theory CSpace_R

lemma no_src_subtree_n_m:
  assumes no_src: "\<not> m \<turnstile> p \<rightarrow> src" "p \<noteq> src" "p \<noteq> dest"
  assumes px: "n \<turnstile> p \<rightarrow> x"
  shows "m \<turnstile> p \<rightarrow> x" using px proof induct case (direct_parent c) thus ?case using neq no_src no_loops apply - apply (case_tac "c=dest") apply (cases "m (mdbPrev src_node)") apply (unfold n)[1] apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp: mdb_next_update) apply (rename_tac cte') apply clarsimp apply (subgoal_tac "p = mdbPrev src_node") prefer 2 apply (simp add: n) apply (subst (asm) modify_map_apply, simp) apply (clarsimp simp:_mdb_next_update split: if_split_asm) apply clarsimp apply (simp add: n) apply (subst (asm) modify_map_apply, simp)+ apply (insert dest)[1] apply (clarsimp simp add: parentOf_def mdb_next_unfold) apply (subgoal_tac "m \<turnstile> mdbPrev src_node \<rightarrow> src") apply simp apply (rule subtree.direct_parent) apply (rule prev_leadstoI) apply (rule src) apply (insert no_0, clarsimp simp: no_0_def)[1] apply (rule dlist) apply (rule src_0) apply (simp add: parentOf_def src parent_preserved) apply (rule subtree.direct_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (simp add: mdb_next_update) apply (subst (asm) modify_map_apply, simp)+ apply (simp add: mdb_next_update split: if_split_asm) apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp add: parentOf_def split: if_split_asm) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp add: parentOf_def split: if_split_asm) done next case (trans_parent c c') thus ?case using neq no_src apply - apply (case_tac "c' = dest") apply clarsimp apply (subgoal_tac "c = mdbPrev src_node") prefer 2 apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp: mdb_next_update split: if_split_asm) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp: mdb_next_update split: if_split_asm) apply clarsimp apply (cases "m (mdbPrev src_node)") apply (unfold n)[1] apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp: mdb_next_update) apply (subgoal_tac "m \<turnstile> p \<rightarrow> src") apply simp apply (rule subtree.trans_parent, assumption) apply (rule prev_leadstoI) apply (rule src) apply (insert no_0, clarsimp simp: no_0_def)[1] apply (rule dlist) apply (rule src_0) apply (clarsimp simp: n) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp: parentOf_def src parent_preserved
                     split: if_split_asm) apply (rule subtree.trans_parent, assumption) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (simp add: mdb_next_update split: if_split_asm) apply (subst (asm) modify_map_apply, simp)+ apply (simp add: mdb_next_update split: if_split_asm) apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp: parentOf_def split: if_split_asm) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp: parentOf_def split: if_split_asm) done qed

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

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

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

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

goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c
 2. \<And>a. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c
 2. \<And>a. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p \<leadsto> c; c \<noteq> 0; m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c
 2. \<And>a. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<And>cte'. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> False
 2. \<And>cte'. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<And>cte'. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<And>cte'. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<And>cte'. \<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> p \<leadsto> dest; dest \<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> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<And>cte'. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<And>cte'. \<lbrakk>m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode, mdbPrev src_node \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. dest)) cte') \<turnstile> p \<leadsto> dest; dest \<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> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<And>cte'. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<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> mdbPrev src_node \<leadsto> dest; dest \<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> mdbPrev src_node parentOf dest; src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode, mdbPrev src_node \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. dest)) cte') \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<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)) cte') \<turnstile> mdbPrev src_node parentOf dest; src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode, mdbPrev src_node \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. dest)) cte') \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<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)) cte') \<turnstile> mdbPrev src_node parentOf dest; src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node); m \<turnstile> mdbPrev src_node \<rightarrow> src\<rbrakk> \<Longrightarrow> False
 2. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<rightarrow> src
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<rightarrow> src
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (4 subgoals):
 1. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> src
 2. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node parentOf src
 4. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (6 subgoals):
 1. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m src = Some (CTE (?cap61 cte') src_node)
 2. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0
 3. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> valid_dlist m
 4. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> src \<noteq> 0
 5. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node parentOf src
 6. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (5 subgoals):
 1. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0
 2. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> src \<noteq> 0
 4. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node parentOf src
 5. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (4 subgoals):
 1. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node parentOf src
 4. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> src \<noteq> 0
 2. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node parentOf src
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>dest \<noteq> 0; isMDBParentOf cte' (CTE cap' src_node); src \<noteq> dest; \<not> m \<turnstile> mdbPrev src_node \<rightarrow> src; no_loops m; c = dest; m (mdbPrev src_node) = Some cte'; p = mdbPrev src_node; m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node parentOf src
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (3 subgoals):
 1. \<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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (4 subgoals):
 1. \<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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 2. \<And>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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p \<leadsto> c; c \<noteq> 0; m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 2. \<And>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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (3 subgoals):
 1. \<And>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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (3 subgoals):
 1. \<And>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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (2 subgoals):
 1. \<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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c
 2. \<And>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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p \<leadsto> c; c \<noteq> 0; m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode) \<turnstile> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = None\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c
 2. \<And>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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<And>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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<And>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> p \<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> p parentOf c; src \<noteq> dest; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; p \<noteq> dest; no_loops m; c \<noteq> dest; m (mdbPrev src_node) = Some a\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> p \<rightarrow> c

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

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

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

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

goal:
No subgoals!