theory CSpace_R

lemma subtree_dest_src:
  "n \<turnstile> dest \<rightarrow> x \<Longrightarrow> m \<turnstile> src \<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 (asm) modify_map_None, simp)+ apply (clarsimp simp add: mdb_next_update next_unfold src) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp add: mdb_next_update  next_unfold src) apply assumption apply (simp add: n) apply (simp add: modify_map_def parentOf_def) apply (clarsimp simp: src children_preserved) apply (subgoal_tac "c' \<noteq> dest") prefer 2 apply clarsimp apply (subgoal_tac "c'' \<noteq> dest") prefer 2 apply clarsimp apply (drule (3) trans_parent) apply (simp add: dest_loop) apply (subgoal_tac "c' \<noteq> mdbPrev src_node") prefer 2 apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (simp add: mdb_next_update nullPointer_def split: if_split_asm) apply (subst (asm) modify_map_apply, simp)+ apply (simp add: mdb_next_update nullPointer_def split: if_split_asm) apply assumption apply (clarsimp simp add: n modify_map_def parentOf_def src children_preserved
                  split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> dest \<rightarrow> x \<Longrightarrow> m \<turnstile> src \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> dest \<leadsto> c'; c' \<noteq> 0; n \<turnstile> dest parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> mdbNext (cteMDBNode z)
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext (cteMDBNode z)
 2. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 3. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext (cteMDBNode z)
 4. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; 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 (cteMDBNode z); modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext (cteMDBNode z)
 2. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 3. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext (cteMDBNode z)
 4. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (5 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; 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 (cteMDBNode z); modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) dest = Some z; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext (cteMDBNode z)
 2. \<And>z a. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; 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 (cteMDBNode z); modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) dest = Some z; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext (cteMDBNode z)
 3. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 4. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext (cteMDBNode z)
 5. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (5 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> dest parentOf mdbNext (cteMDBNode z); (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) dest = Some z; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext (cteMDBNode z)
 2. \<And>z a. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; 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 (cteMDBNode z); modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) dest = Some z; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext (cteMDBNode z)
 3. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 4. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext (cteMDBNode z)
 5. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>z a. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; 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 (cteMDBNode z); modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) dest = Some z; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext (cteMDBNode z)
 2. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 3. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext (cteMDBNode z)
 4. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>z a. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; 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 parentOf mdbNext (cteMDBNode z); (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode, mdbPrev src_node \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. dest)) a)) dest = Some z; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext (cteMDBNode z)
 2. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 3. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext (cteMDBNode z)
 4. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 2. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext (cteMDBNode z)
 3. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; n \<turnstile> dest parentOf mdbNext (cteMDBNode z); n dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext (cteMDBNode z)
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; 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 (cteMDBNode z); modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) dest = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext (cteMDBNode z)
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; \<exists>cte. (if mdbNext (cteMDBNode z) = mdbPrev src_node then map_option (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) (m (mdbPrev src_node)) else if mdbNext (cteMDBNode z) = src then Some (CTE capability.NullCap nullMDBNode) else if mdbNext (cteMDBNode z) = dest then Some z else m (mdbNext (cteMDBNode z))) = Some cte \<and> isMDBParentOf z cte; CTE cap' src_node = z\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m (mdbNext (cteMDBNode z)) = Some cte \<and> m src = Some cte' \<and> isMDBParentOf cte' cte
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c''
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> c' \<noteq> dest proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> c' \<noteq> dest
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c''
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest\<rbrakk> \<Longrightarrow> c'' \<noteq> dest proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest\<rbrakk> \<Longrightarrow> c'' \<noteq> dest
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> dest; dest \<noteq> 0; n \<turnstile> dest parentOf dest; c' \<noteq> dest\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> dest; dest \<noteq> 0; n \<turnstile> dest parentOf dest; c' \<noteq> dest; n \<turnstile> dest \<rightarrow> dest\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c''
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> c' \<noteq> mdbPrev src_node proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> c' \<noteq> mdbPrev src_node
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; m \<turnstile> src \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c''. \<lbrakk>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 \<rightarrow> c'; 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''; c'' \<noteq> 0; 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 c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf c'' proof (prove)
goal (4 subgoals):
 1. \<And>c' c''. \<lbrakk>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 \<rightarrow> c'; 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''; c'' \<noteq> 0; 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 c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 2. \<And>c' c'' a. \<lbrakk>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 \<rightarrow> c'; 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''; c'' \<noteq> 0; 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 c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 3. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 4. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf c'' proof (prove)
goal (4 subgoals):
 1. \<And>c' c''. \<lbrakk>m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> dest \<rightarrow> c'; m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 2. \<And>c' c'' a. \<lbrakk>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 \<rightarrow> c'; 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''; c'' \<noteq> 0; 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 c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 3. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 4. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c'' a. \<lbrakk>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 \<rightarrow> c'; 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''; c'' \<noteq> 0; 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 c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c'' a. \<lbrakk>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 \<rightarrow> c'; 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''; c'' \<noteq> 0; 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 parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf c'' proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> dest \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''; c' \<noteq> dest; c'' \<noteq> dest; c' \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf c'' proof (prove)
goal:
No subgoals!