theory Finalise_R

lemma parency_n:
  assumes "n \<turnstile> p \<rightarrow> p'"
  shows "m \<turnstile> p \<rightarrow> p' \<and> p \<noteq> slot \<and> p' \<noteq> slot" using assms proof induct case (direct_parent c') moreover hence "p \<noteq> slot" by (clarsimp simp: n_next_eq) moreover from direct_parent have "c' \<noteq> slot" by (clarsimp simp add: n_next_eq split: if_split_asm) ultimately show ?case apply simp apply (simp add: n_next_eq split: if_split_asm) prefer 2 apply (erule (1) subtree.direct_parent) apply (erule (2) n_parent_of) apply clarsimp apply (frule n_parent_of, simp, simp) apply (rule subtree.trans_parent[OF _ m_slot_next], simp_all) apply (rule subtree.direct_parent) apply (erule prev_slot_next) apply simp apply (clarsimp simp: parentOf_def slot) apply (case_tac cte'a) apply (case_tac ctea) apply clarsimp apply (frule(2) mdb_chunked2D [OF chunked prev_slot_next m_slot_next]) apply (clarsimp simp: isMDBParentOf_CTE) apply simp apply (simp add: slot) apply (clarsimp simp add: isMDBParentOf_CTE) apply (insert valid_badges) apply (simp add: valid_badges_def2) apply (drule spec[where x=slot]) apply (drule spec[where x="mdbNext s_node"]) apply (simp add: slot m_slot_next) apply (insert valid_badges) apply (simp add: valid_badges_def2) apply (drule spec[where x="mdbPrev s_node"]) apply (drule spec[where x=slot]) apply (simp add: slot prev_slot_next) apply (case_tac cte, case_tac cte') apply (rename_tac cap'' node'') apply (clarsimp simp: isMDBParentOf_CTE) apply (frule n_cap, drule n_badged) apply (frule n_cap, drule n_badged) apply clarsimp apply (case_tac cap'', simp_all add: isCap_simps)[1] apply (clarsimp simp: sameRegionAs_def3 isCap_simps) apply (clarsimp simp: sameRegionAs_def3 isCap_simps) done next case (trans_parent c c') moreover hence "p \<noteq> slot" by (clarsimp simp: n_next_eq) moreover from trans_parent have "c' \<noteq> slot" by (clarsimp simp add: n_next_eq split: if_split_asm) ultimately show ?case apply clarsimp apply (simp add: n_next_eq split: if_split_asm) prefer 2 apply (erule (2) subtree.trans_parent) apply (erule n_parent_of, simp, simp) apply clarsimp apply (rule subtree.trans_parent) apply (rule subtree.trans_parent, assumption) apply (rule prev_slot_next) apply clarsimp apply clarsimp apply (frule n_parent_of, simp, simp) apply (clarsimp simp: parentOf_def slot) apply (case_tac cte'a) apply (rename_tac cap node) apply (case_tac ctea) apply clarsimp apply (subgoal_tac "sameRegionAs cap s_cap") prefer 2 apply (insert chunked)[1] apply (simp add: mdb_chunked_def) apply (erule_tac x="p" in allE) apply (erule_tac x="mdbNext s_node" in allE) apply simp apply (drule isMDBParent_sameRegion)+ apply clarsimp apply (subgoal_tac "m \<turnstile> p \<leadsto>\<^sup>+ slot") prefer 2 apply (rule trancl_trans) apply (erule subtree_mdb_next) apply (rule r_into_trancl) apply (rule prev_slot_next) apply clarsimp apply (subgoal_tac "m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node") prefer 2 apply (erule trancl_trans) apply fastforce apply simp apply (erule impE) apply clarsimp apply clarsimp apply (thin_tac "s \<longrightarrow> t" for s t) apply (simp add: is_chunk_def) apply (erule_tac x=slot in allE) apply (erule impE, fastforce) apply (erule impE, fastforce) apply (clarsimp simp: slot) apply (clarsimp simp: isMDBParentOf_CTE) apply (insert valid_badges, simp add: valid_badges_def2) apply (drule spec[where x=slot], drule spec[where x="mdbNext s_node"]) apply (simp add: slot m_slot_next) apply (case_tac cte, case_tac cte') apply (rename_tac cap'' node'') apply (clarsimp simp: isMDBParentOf_CTE) apply (frule n_cap, drule n_badged) apply (frule n_cap, drule n_badged) apply (clarsimp split: if_split_asm) apply (drule subtree_mdb_next) apply (drule no_loops_tranclE[OF no_loops]) apply (erule notE, rule trancl_into_rtrancl) apply (rule trancl.intros(2)[OF _ m_slot_next]) apply (rule trancl.intros(1), rule prev_slot_next) apply simp apply (case_tac cap'', simp_all add: isCap_simps)[1] apply (clarsimp simp: sameRegionAs_def3 isCap_simps) apply (clarsimp simp: sameRegionAs_def3 isCap_simps) apply (rule m_slot_next) apply simp apply (erule n_parent_of, simp, simp) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> p' \<and> p \<noteq> slot \<and> p' \<noteq> slot proof (prove)
using this:
n \<turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> p' \<and> p \<noteq> slot \<and> p' \<noteq> slot proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (state)
this:
n \<turnstile> p \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (state)
this:
n \<turnstile> p \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (prove)
using this:
n \<turnstile> p \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'

goal (1 subgoal):
 1. p \<noteq> slot proof (state)
this:
p \<noteq> slot

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (state)
this:
p \<noteq> slot

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (chain)
picking this:
n \<turnstile> p \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c' proof (prove)
using this:
n \<turnstile> p \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'

goal (1 subgoal):
 1. c' \<noteq> slot proof (state)
this:
c' \<noteq> slot

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (chain)
picking this:
n \<turnstile> p \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'
p \<noteq> slot
c' \<noteq> slot proof (prove)
using this:
n \<turnstile> p \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'
p \<noteq> slot
c' \<noteq> slot

goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> slot; c' \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node
 2. \<lbrakk>c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> slot; c' \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> slot; c' \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> slot; c' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c'
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<rightarrow> slot proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto> slot
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> slot \<noteq> 0
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node parentOf slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> slot \<noteq> 0
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node parentOf slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbPrev s_node parentOf mdbNext s_node; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node parentOf slot proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte'a cte ctea. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some ctea; n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some cte'a; isMDBParentOf cte'a ctea\<rbrakk> \<Longrightarrow> isMDBParentOf cte'a (CTE s_cap s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte'a cte ctea x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some ctea; n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some cte'a; isMDBParentOf cte'a ctea; cte'a = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte'a (CTE s_cap s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte'a cte ctea x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some ctea; n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some cte'a; isMDBParentOf cte'a ctea; cte'a = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf cte'a (CTE s_cap s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); isMDBParentOf (CTE x1 x2) (CTE x1a x2a)\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE s_cap s_node) proof (prove)
goal (3 subgoals):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); isMDBParentOf (CTE x1 x2) (CTE x1a x2a)\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 x1a
 2. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); isMDBParentOf (CTE x1 x2) (CTE x1a x2a)\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> mdbNext s_node
 3. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); isMDBParentOf (CTE x1 x2) (CTE x1a x2a); \<exists>cap' nd'. m slot = Some (CTE cap' nd') \<and> global.sameRegionAs x1 cap'\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE s_cap s_node) proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); isMDBParentOf (CTE x1 x2) (CTE x1a x2a)\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> mdbNext s_node
 2. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); isMDBParentOf (CTE x1 x2) (CTE x1a x2a); \<exists>cap' nd'. m slot = Some (CTE cap' nd') \<and> global.sameRegionAs x1 cap'\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE s_cap s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); isMDBParentOf (CTE x1 x2) (CTE x1a x2a); \<exists>cap' nd'. m slot = Some (CTE cap' nd') \<and> global.sameRegionAs x1 cap'\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE s_cap s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); isMDBParentOf (CTE x1 x2) (CTE x1a x2a); global.sameRegionAs x1 s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE s_cap s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); valid_badges m\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); \<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); \<forall>p' cap. (\<exists>node. m slot = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> slot \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); \<forall>cap. (\<exists>node. m slot = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; valid_badges m\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; \<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; \<forall>p' cap. (\<exists>node. m (mdbPrev s_node) = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; \<forall>cap. (\<exists>node. m (mdbPrev s_node) = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m slot = Some (CTE cap' node') \<longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto> slot \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capMasterCap x1 = capMasterCap s_cap \<longrightarrow> (\<exists>y. capBadge x1 = Some y) \<longrightarrow> capBadge x1 \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capMasterCap x1 = capMasterCap s_cap \<longrightarrow> (\<exists>y. capBadge x1 = Some y) \<longrightarrow> capBadge x1 \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node; cte = CTE x1b x2b; cte' = CTE x1c x2c\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a x1b x2b cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some cte'; isMDBParentOf cte' cte; m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capMasterCap x1 = capMasterCap s_cap \<longrightarrow> (\<exists>y. capBadge x1 = Some y) \<longrightarrow> capBadge x1 \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node; cte = CTE x1b x2b; cte' = CTE cap'' node''\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some (CTE x1b x2b); m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some (CTE cap'' node''); m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capMasterCap x1 = capMasterCap s_cap \<longrightarrow> (\<exists>y. capBadge x1 = Some y) \<longrightarrow> capBadge x1 \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node; global.sameRegionAs cap'' x1b; mdbRevocable node''; (capBadge cap'', capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2b)\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2a); n (mdbPrev s_node) = Some (CTE cap'' node''); m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capMasterCap x1 = capMasterCap s_cap \<longrightarrow> (\<exists>y. capBadge x1 = Some y) \<longrightarrow> capBadge x1 \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node; global.sameRegionAs cap'' x1b; mdbRevocable node''; (capBadge cap'', capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2b); \<exists>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<and> (if mdbNext s_node = slot then x1b = capability.NullCap else cap' = x1b); \<exists>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<and> (if mdbNext s_node = slot then \<not> mdbFirstBadged x2b else if mdbNext s_node = mdbNext s_node then mdbFirstBadged x2b = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2b = mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2a); m (mdbPrev s_node) = Some (CTE x1 x2); global.sameRegionAs x1 s_cap; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capMasterCap x1 = capMasterCap s_cap \<longrightarrow> (\<exists>y. capBadge x1 = Some y) \<longrightarrow> capBadge x1 \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node; global.sameRegionAs cap'' x1b; mdbRevocable node''; (capBadge cap'', capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2b); \<exists>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<and> (if mdbNext s_node = slot then x1b = capability.NullCap else cap' = x1b); \<exists>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<and> (if mdbNext s_node = slot then \<not> mdbFirstBadged x2b else if mdbNext s_node = mdbNext s_node then mdbFirstBadged x2b = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2b = mdbFirstBadged node'); \<exists>cap' node'. m (mdbPrev s_node) = Some (CTE cap' node') \<and> (if mdbPrev s_node = slot then cap'' = capability.NullCap else cap' = cap''); \<exists>cap' node'. m (mdbPrev s_node) = Some (CTE cap' node') \<and> (if mdbPrev s_node = slot then \<not> mdbFirstBadged node'' else if mdbPrev s_node = mdbNext s_node then mdbFirstBadged node'' = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node'' = mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a x1b x2b cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1b x2a); m (mdbPrev s_node) = Some (CTE cap'' x2); global.sameRegionAs cap'' s_cap; mdbRevocable x2; (capBadge cap'', capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1b \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1b \<longrightarrow> capBadge x1b \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capMasterCap cap'' = capMasterCap s_cap \<longrightarrow> (\<exists>y. capBadge cap'' = Some y) \<longrightarrow> capBadge cap'' \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node; global.sameRegionAs cap'' x1b; mdbRevocable node''; (capBadge cap'', capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2a \<or> mdbFirstBadged s_node); mdbFirstBadged x2b = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node); mdbFirstBadged node'' = mdbFirstBadged x2\<rbrakk> \<Longrightarrow> (capBadge cap'', capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (2 subgoals):
 1. \<And>x2 x2a x1b x2b cap'' node'' x31 x32 x33 x34. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1b x2a); m (mdbPrev s_node) = Some (CTE (capability.NotificationCap x31 x32 x33 x34) x2); global.sameRegionAs (capability.NotificationCap x31 x32 x33 x34) s_cap; mdbRevocable x2; (Some x32, capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1b \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1b \<longrightarrow> capBadge x1b \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capability.NotificationCap x31 0 True True = capMasterCap s_cap \<longrightarrow> Some x32 \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node; global.sameRegionAs (capability.NotificationCap x31 x32 x33 x34) x1b; mdbRevocable node''; (Some x32, capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2a \<or> mdbFirstBadged s_node); mdbFirstBadged x2b = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node); mdbFirstBadged node'' = mdbFirstBadged x2; cap'' = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> (Some x32, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<And>x2 x2a x1b x2b cap'' node'' x51 x52 x53 x54 x55 x56. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1b x2a); m (mdbPrev s_node) = Some (CTE (capability.EndpointCap x51 x52 x53 x54 x55 x56) x2); global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) s_cap; mdbRevocable x2; (Some x52, capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1b \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1b \<longrightarrow> capBadge x1b \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capability.EndpointCap x51 0 True True True True = capMasterCap s_cap \<longrightarrow> Some x52 \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node; global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) x1b; mdbRevocable node''; (Some x52, capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2a \<or> mdbFirstBadged s_node); mdbFirstBadged x2b = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node); mdbFirstBadged node'' = mdbFirstBadged x2; cap'' = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> (Some x52, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a x1b x2b cap'' node'' x51 x52 x53 x54 x55 x56. \<lbrakk>mdbNext s_node \<noteq> 0; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1b x2a); m (mdbPrev s_node) = Some (CTE (capability.EndpointCap x51 x52 x53 x54 x55 x56) x2); global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) s_cap; mdbRevocable x2; (Some x52, capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap s_cap = capMasterCap x1b \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1b \<longrightarrow> capBadge x1b \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2a; capability.EndpointCap x51 0 True True True True = capMasterCap s_cap \<longrightarrow> Some x52 \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node; global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) x1b; mdbRevocable node''; (Some x52, capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2a \<or> mdbFirstBadged s_node); mdbFirstBadged x2b = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node); mdbFirstBadged node'' = mdbFirstBadged x2; cap'' = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> (Some x52, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node) proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (state)
this:
n \<turnstile> p \<rightarrow> c
m \<turnstile> p \<rightarrow> c \<and> p \<noteq> slot \<and> c \<noteq> slot
n \<turnstile> c \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (state)
this:
n \<turnstile> p \<rightarrow> c
m \<turnstile> p \<rightarrow> c \<and> p \<noteq> slot \<and> c \<noteq> slot
n \<turnstile> c \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (prove)
using this:
n \<turnstile> p \<rightarrow> c
m \<turnstile> p \<rightarrow> c \<and> p \<noteq> slot \<and> c \<noteq> slot
n \<turnstile> c \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'

goal (1 subgoal):
 1. p \<noteq> slot proof (state)
this:
p \<noteq> slot

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (state)
this:
p \<noteq> slot

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (chain)
picking this:
n \<turnstile> p \<rightarrow> c
m \<turnstile> p \<rightarrow> c \<and> p \<noteq> slot \<and> c \<noteq> slot
n \<turnstile> c \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c' proof (prove)
using this:
n \<turnstile> p \<rightarrow> c
m \<turnstile> p \<rightarrow> c \<and> p \<noteq> slot \<and> c \<noteq> slot
n \<turnstile> c \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'

goal (1 subgoal):
 1. c' \<noteq> slot proof (state)
this:
c' \<noteq> slot

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' \<and> p \<noteq> slot \<and> c'' \<noteq> slot proof (chain)
picking this:
n \<turnstile> p \<rightarrow> c
m \<turnstile> p \<rightarrow> c \<and> p \<noteq> slot \<and> c \<noteq> slot
n \<turnstile> c \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'
p \<noteq> slot
c' \<noteq> slot proof (prove)
using this:
n \<turnstile> p \<rightarrow> c
m \<turnstile> p \<rightarrow> c \<and> p \<noteq> slot \<and> c \<noteq> slot
n \<turnstile> c \<leadsto> c'
c' \<noteq> 0
n \<turnstile> p parentOf c'
p \<noteq> slot
c' \<noteq> slot

goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<rightarrow> c; n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> slot; c' \<noteq> slot; m \<turnstile> p \<rightarrow> c; c \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node
 2. \<lbrakk>c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> slot; c' \<noteq> slot; m \<turnstile> p \<rightarrow> c; c \<noteq> slot; n \<turnstile> p \<rightarrow> c; c \<noteq> mdbPrev s_node; m \<turnstile> c \<leadsto> c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> slot; c' \<noteq> slot; m \<turnstile> p \<rightarrow> c; c \<noteq> slot; n \<turnstile> p \<rightarrow> c; c \<noteq> mdbPrev s_node; m \<turnstile> c \<leadsto> c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> slot; c' \<noteq> slot; c \<noteq> slot; n \<turnstile> p \<rightarrow> c; c \<noteq> mdbPrev s_node; m \<turnstile> c \<leadsto> c'\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c'
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> ?c'27
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> ?c'27 \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto> ?c'27
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> ?c'27 \<noteq> 0
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf ?c'27
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> ?c'27 \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> slot \<noteq> 0
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf slot
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> slot \<noteq> 0
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf slot
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf slot
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m \<turnstile> p parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf slot
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte'a cte ctea. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some ctea; n p = Some cte'; isMDBParentOf cte' cte; m p = Some cte'a; isMDBParentOf cte'a ctea\<rbrakk> \<Longrightarrow> isMDBParentOf cte'a (CTE s_cap s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte'a cte ctea x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some ctea; n p = Some cte'; isMDBParentOf cte' cte; m p = Some cte'a; isMDBParentOf cte'a ctea; cte'a = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte'a (CTE s_cap s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte'a cte ctea cap node. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some ctea; n p = Some cte'; isMDBParentOf cte' cte; m p = Some cte'a; isMDBParentOf cte'a ctea; cte'a = CTE cap node\<rbrakk> \<Longrightarrow> isMDBParentOf cte'a (CTE s_cap s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte'a cte ctea cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some ctea; n p = Some cte'; isMDBParentOf cte' cte; m p = Some cte'a; isMDBParentOf cte'a ctea; cte'a = CTE cap node; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte'a (CTE s_cap s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2)\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); mdb_chunked m\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p))\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); \<forall>p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p))\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); \<forall>cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m (mdbNext s_node) = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' (mdbNext s_node) p))\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap x1 \<longrightarrow> p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs cap x1 \<longrightarrow> p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs (cteCap (CTE cap node)) (cteCap (CTE x1 x2))\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ slot
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ slot
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (7 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ ?y71 cte' cte cap node x1 x2
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1\<rbrakk> \<Longrightarrow> m \<turnstile> ?y71 cte' cte cap node x1 x2 \<leadsto>\<^sup>+ slot
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 4. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 7. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ slot
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto> slot
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<or> m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node)) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); p \<noteq> mdbNext s_node \<longrightarrow> is_chunk m cap p (mdbNext s_node) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node\<rbrakk> \<Longrightarrow> p \<noteq> mdbNext s_node
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node; is_chunk m cap p (mdbNext s_node) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 3. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 6. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node; is_chunk m cap p (mdbNext s_node) \<and> (m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node; is_chunk m cap p (mdbNext s_node); m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 (mdbNext s_node) p\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node; is_chunk m cap p (mdbNext s_node)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node; \<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* mdbNext s_node \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node; m \<turnstile> p \<leadsto>\<^sup>+ slot \<longrightarrow> m \<turnstile> slot \<leadsto>\<^sup>* mdbNext s_node \<longrightarrow> (\<exists>cap''. (\<exists>n''. m slot = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node; m \<turnstile> slot \<leadsto>\<^sup>* mdbNext s_node \<longrightarrow> (\<exists>cap''. (\<exists>n''. m slot = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; m p = Some (CTE cap node); global.sameRegionAs (cteCap cte') (cteCap cte); global.sameRegionAs cap x1; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node; \<exists>cap''. (\<exists>n''. m slot = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''\<rbrakk> \<Longrightarrow> global.sameRegionAs cap s_cap
 2. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); isMDBParentOf (CTE cap node) (CTE x1 x2); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap node) (CTE s_cap s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); global.sameRegionAs cap s_cap; global.sameRegionAs cap x1; mdbRevocable node; (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2)\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); global.sameRegionAs cap s_cap; global.sameRegionAs cap x1; mdbRevocable node; (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); global.sameRegionAs cap s_cap; global.sameRegionAs cap x1; mdbRevocable node; (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<forall>cap. (\<exists>node. m slot = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte cap node x1 x2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); global.sameRegionAs cap s_cap; global.sameRegionAs cap x1; mdbRevocable node; (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1 \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1 \<longrightarrow> capBadge x1 \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte cap node x1 x2 x1a x2a x1b x2b. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); global.sameRegionAs cap s_cap; global.sameRegionAs cap x1; mdbRevocable node; (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1 \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1 \<longrightarrow> capBadge x1 \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; cte = CTE x1a x2a; cte' = CTE x1b x2b\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte cap node x1 x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some cte; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some cte'; isMDBParentOf cte' cte; m p = Some (CTE cap node); global.sameRegionAs cap s_cap; global.sameRegionAs cap x1; mdbRevocable node; (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1 \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1 \<longrightarrow> capBadge x1 \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; cte = CTE x1a x2a; cte' = CTE cap'' node''\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cap node x1 x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; n (mdbNext s_node) = Some (CTE x1a x2a); m (mdbNext s_node) = Some (CTE x1 x2); n p = Some (CTE cap'' node''); m p = Some (CTE cap node); global.sameRegionAs cap s_cap; global.sameRegionAs cap x1; mdbRevocable node; (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1 \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1 \<longrightarrow> capBadge x1 \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cap node x1 x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1 x2); n p = Some (CTE cap'' node''); m p = Some (CTE cap node); global.sameRegionAs cap s_cap; global.sameRegionAs cap x1; mdbRevocable node; (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1 \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1 \<longrightarrow> capBadge x1 \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); \<exists>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<and> (if mdbNext s_node = slot then x1a = capability.NullCap else cap' = x1a); \<exists>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<and> (if mdbNext s_node = slot then \<not> mdbFirstBadged x2a else if mdbNext s_node = mdbNext s_node then mdbFirstBadged x2a = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2a = mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>cap node x1 x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1 x2); m p = Some (CTE cap node); global.sameRegionAs cap s_cap; global.sameRegionAs cap x1; mdbRevocable node; (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1 \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1 \<longrightarrow> capBadge x1 \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); \<exists>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<and> (if mdbNext s_node = slot then x1a = capability.NullCap else cap' = x1a); \<exists>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<and> (if mdbNext s_node = slot then \<not> mdbFirstBadged x2a else if mdbNext s_node = mdbNext s_node then mdbFirstBadged x2a = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2a = mdbFirstBadged node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then cap'' = capability.NullCap else cap' = cap''); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node'' else if p = mdbNext s_node then mdbFirstBadged node'' = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node'' = mdbFirstBadged node')\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>node x1a x2a node''. \<lbrakk>mdbNext s_node \<noteq> 0; m \<turnstile> mdbNext s_node \<rightarrow> mdbPrev s_node; n \<turnstile> mdbNext s_node \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a node); global.sameRegionAs x1a s_cap; mdbRevocable node; mdbFirstBadged node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node; global.sameRegionAs x1a x1a; mdbRevocable node''; mdbFirstBadged s_node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; mdbFirstBadged x2a = (mdbFirstBadged node \<or> mdbFirstBadged s_node); p = mdbNext s_node; mdbFirstBadged node'' = (mdbFirstBadged node \<or> mdbFirstBadged s_node)\<rbrakk> \<Longrightarrow> (capBadge x1a, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<And>node x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE cap'' node); global.sameRegionAs cap'' s_cap; mdbRevocable node; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node\<rbrakk> \<Longrightarrow> (capBadge cap'', capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>node x1a x2a node''. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbNext s_node \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a node); global.sameRegionAs x1a s_cap; mdbRevocable node; mdbFirstBadged node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node; global.sameRegionAs x1a x1a; mdbRevocable node''; mdbFirstBadged s_node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; mdbFirstBadged x2a = (mdbFirstBadged node \<or> mdbFirstBadged s_node); p = mdbNext s_node; mdbFirstBadged node'' = (mdbFirstBadged node \<or> mdbFirstBadged s_node); m \<turnstile> mdbNext s_node \<leadsto>\<^sup>+ mdbPrev s_node\<rbrakk> \<Longrightarrow> (capBadge x1a, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<And>node x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE cap'' node); global.sameRegionAs cap'' s_cap; mdbRevocable node; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node\<rbrakk> \<Longrightarrow> (capBadge cap'', capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>node x1a x2a node''. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbNext s_node \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a node); global.sameRegionAs x1a s_cap; mdbRevocable node; mdbFirstBadged node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node; global.sameRegionAs x1a x1a; mdbRevocable node''; mdbFirstBadged s_node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; mdbFirstBadged x2a = (mdbFirstBadged node \<or> mdbFirstBadged s_node); p = mdbNext s_node; mdbFirstBadged node'' = (mdbFirstBadged node \<or> mdbFirstBadged s_node); (mdbPrev s_node, mdbNext s_node) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> (capBadge x1a, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<And>node x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE cap'' node); global.sameRegionAs cap'' s_cap; mdbRevocable node; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node\<rbrakk> \<Longrightarrow> (capBadge cap'', capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>node x1a x2a node''. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbNext s_node \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a node); global.sameRegionAs x1a s_cap; mdbRevocable node; mdbFirstBadged node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node; global.sameRegionAs x1a x1a; mdbRevocable node''; mdbFirstBadged s_node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; mdbFirstBadged x2a = (mdbFirstBadged node \<or> mdbFirstBadged s_node); p = mdbNext s_node; mdbFirstBadged node'' = (mdbFirstBadged node \<or> mdbFirstBadged s_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>node x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE cap'' node); global.sameRegionAs cap'' s_cap; mdbRevocable node; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node\<rbrakk> \<Longrightarrow> (capBadge cap'', capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>node x1a x2a node''. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbNext s_node \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a node); global.sameRegionAs x1a s_cap; mdbRevocable node; mdbFirstBadged node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node; global.sameRegionAs x1a x1a; mdbRevocable node''; mdbFirstBadged s_node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; mdbFirstBadged x2a = (mdbFirstBadged node \<or> mdbFirstBadged s_node); p = mdbNext s_node; mdbFirstBadged node'' = (mdbFirstBadged node \<or> mdbFirstBadged s_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ slot
 2. \<And>node x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE cap'' node); global.sameRegionAs cap'' s_cap; mdbRevocable node; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node\<rbrakk> \<Longrightarrow> (capBadge cap'', capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>node x1a x2a node''. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> mdbNext s_node \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a node); global.sameRegionAs x1a s_cap; mdbRevocable node; mdbFirstBadged node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node; global.sameRegionAs x1a x1a; mdbRevocable node''; mdbFirstBadged s_node \<longrightarrow> capBadge x1a = None \<or> capBadge x1a = Some 0; mdbFirstBadged x2a = (mdbFirstBadged node \<or> mdbFirstBadged s_node); p = mdbNext s_node; mdbFirstBadged node'' = (mdbFirstBadged node \<or> mdbFirstBadged s_node)\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 2. \<And>node x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE cap'' node); global.sameRegionAs cap'' s_cap; mdbRevocable node; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node\<rbrakk> \<Longrightarrow> (capBadge cap'', capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>node x2 x1a x2a cap'' node''. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE cap'' node); global.sameRegionAs cap'' s_cap; mdbRevocable node; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs cap'' x1a; mdbRevocable node''; (capBadge cap'', capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node\<rbrakk> \<Longrightarrow> (capBadge cap'', capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<And>node x2 x1a x2a cap'' node'' x31 x32 x33 x34. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE (capability.NotificationCap x31 x32 x33 x34) node); global.sameRegionAs (capability.NotificationCap x31 x32 x33 x34) s_cap; mdbRevocable node; (Some x32, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs (capability.NotificationCap x31 x32 x33 x34) x1a; mdbRevocable node''; (Some x32, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node; cap'' = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> (Some x32, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<And>node x2 x1a x2a cap'' node'' x51 x52 x53 x54 x55 x56. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE (capability.EndpointCap x51 x52 x53 x54 x55 x56) node); global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) s_cap; mdbRevocable node; (Some x52, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) x1a; mdbRevocable node''; (Some x52, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node; cap'' = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> (Some x52, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 5. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<And>node x2 x1a x2a cap'' node'' x51 x52 x53 x54 x55 x56. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; m (mdbNext s_node) = Some (CTE x1a x2); m p = Some (CTE (capability.EndpointCap x51 x52 x53 x54 x55 x56) node); global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) s_cap; mdbRevocable node; (Some x52, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capMasterCap s_cap = capMasterCap x1a \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap \<noteq> capBadge x1a \<longrightarrow> capBadge x1a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged x2; global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) x1a; mdbRevocable node''; (Some x52, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); mdbFirstBadged x2a = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node); p \<noteq> mdbNext s_node; mdbFirstBadged node'' = mdbFirstBadged node; cap'' = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> (Some x52, capBadge s_cap) \<in> capBadge_ordering (mdbFirstBadged s_node)
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 4. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 3. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 2. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; n \<turnstile> p parentOf mdbNext s_node; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbPrev s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0; c' = mdbNext s_node; valid_badges m\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> p \<rightarrow> c' \<and> p \<noteq> slot \<and> c' \<noteq> slot

goal:
No subgoals!