theory CSpace_R

lemma subtree_m_n:
  assumes p_neq: "p \<noteq> dest" "p \<noteq> src"
  assumes px: "m \<turnstile> p \<rightarrow> x"
  shows "if x = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> x" using px proof induct case (direct_parent c) thus ?case using p_neq apply - apply simp apply (rule conjI) apply clarsimp apply (drule leadsto_is_prev) apply (rule src) apply (rule dlist) apply (rule no_0) apply (clarsimp simp: parentOf_def) apply (rule subtree.direct_parent) apply (simp add: n modify_map_apply mdb_next_update) apply (rule dest_0) apply (clarsimp simp: n modify_map_apply parentOf_def
                           neq [symmetric] src parent_preserved) apply clarsimp 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 (clarsimp simp: mdb_next_update) apply (drule prev_leadstoD) apply (rule src) apply (rule dlist) apply (rule no_0) apply simp apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (clarsimp simp add: parentOf_def) apply (subst modify_map_apply, simp) apply (clarsimp simp add: parentOf_def) apply fastforce done next case (trans_parent c c') thus ?case using p_neq apply - apply (clarsimp split: if_split_asm) apply (erule subtree.trans_parent) apply (clarsimp simp: next_unfold' src n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (clarsimp simp add: neq [symmetric] src split: option.splits) apply (subst modify_map_apply, simp) apply (clarsimp simp add: neq [symmetric] src split: option.splits) apply assumption apply (clarsimp simp: mdb_next_unfold src n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (simp add: parentOf_def) apply (subst modify_map_apply, simp) apply (fastforce simp add: parentOf_def) apply (rule conjI) apply clarsimp apply (cases "m c", simp add: mdb_next_unfold) apply (drule leadsto_is_prev) apply (rule src) apply (rule dlist) apply (rule no_0) apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n modify_map_apply mdb_next_update) apply (rule dest_0) apply (clarsimp simp: n modify_map_apply parentOf_def neq [symmetric] src) apply (rule conjI, clarsimp) apply (clarsimp simp: parent_preserved) apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (clarsimp simp add: mdb_next_update) apply (subst modify_map_apply, simp) apply (clarsimp simp add: mdb_next_update) apply (rule conjI, clarsimp) apply clarsimp apply (drule prev_leadstoD, rule src, rule dlist, rule no_0) apply simp apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (clarsimp simp add: parentOf_def) apply (subst modify_map_apply, simp) apply (fastforce simp add: parentOf_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if x = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> x proof (prove)
using this:
m \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. if x = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> x proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'' proof (state)
this:
m \<turnstile> p \<leadsto> c
c \<noteq> 0
m \<turnstile> p parentOf c

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> p \<leadsto> c
c \<noteq> 0
m \<turnstile> p parentOf c

goal (1 subgoal):
 1. if c = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c proof (prove)
using this:
m \<turnstile> p \<leadsto> c
c \<noteq> 0
m \<turnstile> p parentOf c
p \<noteq> dest
p \<noteq> src

goal (1 subgoal):
 1. if c = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src\<rbrakk> \<Longrightarrow> m src = Some (CTE ?cap17 ?node17)
 2. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src\<rbrakk> \<Longrightarrow> no_0 m
 4. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src; p = mdbPrev ?node17\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 5. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src\<rbrakk> \<Longrightarrow> no_0 m
 3. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src\<rbrakk> \<Longrightarrow> no_0 m
 2. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; c = src; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>c = src; p = mdbPrev src_node; m src = Some cte; m (mdbPrev src_node) = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev src_node \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (4 subgoals):
 1. \<And>cte' cte. \<lbrakk>c = src; p = mdbPrev src_node; m src = Some cte; m (mdbPrev src_node) = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev src_node \<leadsto> dest
 2. \<And>cte' cte. \<lbrakk>c = src; p = mdbPrev src_node; m src = Some cte; m (mdbPrev src_node) = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 3. \<And>cte' cte. \<lbrakk>c = src; p = mdbPrev src_node; m src = Some cte; m (mdbPrev src_node) = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev src_node parentOf dest
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<And>cte' cte. \<lbrakk>c = src; p = mdbPrev src_node; m src = Some cte; m (mdbPrev src_node) = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 2. \<And>cte' cte. \<lbrakk>c = src; p = mdbPrev src_node; m src = Some cte; m (mdbPrev src_node) = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev src_node parentOf dest
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>c = src; p = mdbPrev src_node; m src = Some cte; m (mdbPrev src_node) = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev src_node parentOf dest
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p \<leadsto> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p \<leadsto> c
 2. \<And>a. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p \<leadsto> c
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p \<leadsto> c
 2. \<And>a. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p \<leadsto> c
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p \<leadsto> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p \<leadsto> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> mdbPrev src_node \<leadsto> c; c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> dest = c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (6 subgoals):
 1. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m (?p60 a) = Some (CTE (?cap60 a) src_node)
 2. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> no_0 m
 4. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node; c = ?p60 a\<rbrakk> \<Longrightarrow> dest = c
 5. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 6. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> no_0 m
 3. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node; c = src\<rbrakk> \<Longrightarrow> dest = c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 5. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> no_0 m
 2. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node; c = src\<rbrakk> \<Longrightarrow> dest = c
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>c \<noteq> 0; m \<turnstile> mdbPrev src_node parentOf c; c \<noteq> src; m (mdbPrev src_node) = Some a; p = mdbPrev src_node; c = src\<rbrakk> \<Longrightarrow> dest = c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p parentOf c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p parentOf c
 2. \<And>a. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p parentOf c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; c \<noteq> src; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p parentOf c
 2. \<And>a. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<And>a cte' cte. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; p \<noteq> dest; p \<noteq> src; c \<noteq> src; m (mdbPrev src_node) = Some a; m c = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> (c = dest \<longrightarrow> (p = mdbPrev src_node \<longrightarrow> isMDBParentOf a (CTE cap' src_node)) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> isMDBParentOf cte' (CTE cap' src_node))) \<and> (c \<noteq> dest \<longrightarrow> (p = mdbPrev src_node \<longrightarrow> (c = mdbPrev src_node \<longrightarrow> isMDBParentOf a a) \<and> (c \<noteq> mdbPrev src_node \<longrightarrow> isMDBParentOf a cte)) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> c = mdbPrev src_node \<longrightarrow> isMDBParentOf cte' a)) proof (prove)
goal:
No subgoals! proof (state)
this:
if c = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'' proof (state)
this:
m \<turnstile> p \<rightarrow> c
if c = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c
m \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m \<turnstile> p parentOf c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> p \<rightarrow> c
if c = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c
m \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m \<turnstile> p parentOf c'

goal (1 subgoal):
 1. if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c' proof (prove)
using this:
m \<turnstile> p \<rightarrow> c
if c = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c
m \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m \<turnstile> p parentOf c'
p \<noteq> dest
p \<noteq> src

goal (1 subgoal):
 1. if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; n \<turnstile> p \<rightarrow> dest; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto> c'
 2. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>cte. 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 cte \<and> mdbNext (cteMDBNode cte) = mdbNext src_node
 2. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (5 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' = mdbNext src_node; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> \<exists>cte. 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 cte \<and> mdbNext (cteMDBNode cte) = mdbNext src_node
 2. \<And>a. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' = mdbNext src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> \<exists>cte. 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 cte \<and> mdbNext (cteMDBNode cte) = mdbNext src_node
 3. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 4. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 5. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (5 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' = mdbNext src_node; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> \<exists>cte. (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) dest = Some cte \<and> mdbNext (cteMDBNode cte) = mdbNext src_node
 2. \<And>a. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' = mdbNext src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> \<exists>cte. 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 cte \<and> mdbNext (cteMDBNode cte) = mdbNext src_node
 3. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 4. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 5. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' = mdbNext src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> \<exists>cte. 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 cte \<and> mdbNext (cteMDBNode cte) = mdbNext src_node
 2. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' = mdbNext src_node; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> \<exists>cte. (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 cte \<and> mdbNext (cteMDBNode cte) = mdbNext src_node
 2. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c' = mdbNext src_node; mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = 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> p parentOf mdbNext src_node
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>c' = mdbNext src_node; mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = 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> p parentOf mdbNext src_node
 2. \<And>a. \<lbrakk>c' = mdbNext src_node; mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = 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> p parentOf mdbNext src_node
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>c' = mdbNext src_node; mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = src; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p parentOf mdbNext src_node
 2. \<And>a. \<lbrakk>c' = mdbNext src_node; mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = 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> p parentOf mdbNext src_node
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>c' = mdbNext src_node; mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = 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> p parentOf mdbNext src_node
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>c' = mdbNext src_node; mdbNext src_node \<noteq> 0; m \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> src; c = 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> p parentOf mdbNext src_node
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) \<and> (c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> src; m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> c \<leadsto> src; m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a\<rbrakk> \<Longrightarrow> m src = Some (CTE (?cap84 a) (?node84 a))
 2. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a\<rbrakk> \<Longrightarrow> no_0 m
 4. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a; c = mdbPrev (?node84 a)\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 5. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a\<rbrakk> \<Longrightarrow> no_0 m
 3. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 4. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a\<rbrakk> \<Longrightarrow> no_0 m
 2. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' = src; m c = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' = src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev src_node \<leadsto> dest
 2. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' = src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 3. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' = src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 4. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' = src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 2. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' = src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> p parentOf src; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' = src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>a cte'. \<lbrakk>p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' = src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node; m p = Some cte'; isMDBParentOf cte' (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> isMDBParentOf a (CTE cap' src_node)) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> isMDBParentOf cte' (CTE cap' src_node))
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>a cte'. \<lbrakk>p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' = src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node; m p = Some cte'; isMDBParentOf cte' (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> p \<noteq> mdbPrev src_node \<longrightarrow> isMDBParentOf cte' (CTE cap' src_node)
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; n \<turnstile> p \<rightarrow> c; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto> c'
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 4. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 4. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> (c = dest \<longrightarrow> mdbNext src_node = c') \<and> (c \<noteq> dest \<longrightarrow> c = mdbPrev src_node \<longrightarrow> dest = c')
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> c = mdbPrev src_node \<longrightarrow> dest = c'
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>m \<turnstile> mdbPrev src_node \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' \<noteq> src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> dest = c'
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' \<noteq> src; m (mdbPrev src_node) = Some a; c = mdbPrev src_node; c' = src\<rbrakk> \<Longrightarrow> dest = c'
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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> p parentOf c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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> p parentOf c'
 2. \<And>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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> p parentOf c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; c' \<noteq> src; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p parentOf c'
 2. \<And>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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> p parentOf c' proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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> p parentOf c' proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; m \<turnstile> p \<rightarrow> c; c \<noteq> src; 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> p parentOf c' proof (prove)
goal:
No subgoals! proof (state)
this:
if c' = src then n \<turnstile> p \<rightarrow> dest else n \<turnstile> p \<rightarrow> c'

goal:
No subgoals!