theory CSpace_R

lemma subtree_src_dest:
  "m \<turnstile> src \<rightarrow> x \<Longrightarrow> n \<turnstile> dest \<rightarrow> x" apply (erule subtree.induct) apply (clarsimp simp: mdb_next_unfold src) apply (rule subtree.direct_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (simp add: mdb_next_update) apply (subst modify_map_apply, simp) apply (simp add: mdb_next_update) apply assumption apply (simp add: n) apply (clarsimp simp add: modify_map_def parentOf_def src children_preserved) apply (subgoal_tac "c'' \<noteq> src") prefer 2 apply (drule (3) subtree.trans_parent) apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (simp add: mdb_next_update) apply fastforce apply (subst modify_map_apply, simp) apply (simp add: mdb_next_update) apply fastforce apply assumption apply (fastforce simp: n modify_map_def parentOf_def src children_preserved) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<rightarrow> x \<Longrightarrow> n \<turnstile> dest \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> src parentOf c'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> mdbNext src_node
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto> mdbNext src_node
 2. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 3. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf mdbNext src_node
 4. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> dest \<leadsto> mdbNext src_node
 2. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 3. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf mdbNext src_node
 4. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> dest \<leadsto> mdbNext src_node
 2. \<And>a. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> dest \<leadsto> mdbNext src_node
 3. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 4. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf mdbNext src_node
 5. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> dest \<leadsto> mdbNext src_node
 2. \<And>a. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> dest \<leadsto> mdbNext src_node
 3. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 4. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf mdbNext src_node
 5. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> dest \<leadsto> mdbNext src_node
 2. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 3. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf mdbNext src_node
 4. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode, mdbPrev src_node \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. dest)) a) \<turnstile> dest \<leadsto> mdbNext src_node
 2. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 3. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf mdbNext src_node
 4. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 2. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf mdbNext src_node
 3. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf mdbNext src_node
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> src parentOf mdbNext src_node\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> dest parentOf mdbNext src_node
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c''
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> c'' \<noteq> src proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> c'' \<noteq> src
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; m \<turnstile> src \<rightarrow> c''\<rbrakk> \<Longrightarrow> c'' \<noteq> src
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> dest \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal (4 subgoals):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> c' \<leadsto> c''
 2. \<And>c' c'' a. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> c' \<leadsto> c''
 3. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 4. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal (4 subgoals):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> c' \<leadsto> c''
 2. \<And>c' c'' a. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> c' \<leadsto> c''
 3. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 4. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal (4 subgoals):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> mdbNext src_node = c'') \<and> (c' \<noteq> dest \<longrightarrow> c' = src \<longrightarrow> nullPointer = c'')
 2. \<And>c' c'' a. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> c' \<leadsto> c''
 3. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 4. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c'' a. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c'' a. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode, mdbPrev src_node \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. dest)) a) \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c'' a. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> mdbNext src_node = c'') \<and> (c' \<noteq> dest \<longrightarrow> (c' = src \<longrightarrow> nullPointer = c'') \<and> (c' \<noteq> src \<longrightarrow> c' = mdbPrev src_node \<longrightarrow> dest = c''))
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> src \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> src parentOf c''; c'' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest parentOf c'' proof (prove)
goal:
No subgoals!