theory CSpace_R

lemma subtree_n_m:
  assumes p_neq: "p \<noteq> dest" "p \<noteq> src"
  assumes px: "n \<turnstile> p \<rightarrow> x"
  shows "if x = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> x" using px proof induct case (direct_parent c) thus ?case using p_neq apply clarsimp apply (rule conjI) apply clarsimp apply (subgoal_tac "p = mdbPrev src_node") prefer 2 apply (drule mdb_next_modify_prev [where x="mdbNext src_node" and f="\<lambda>_. dest", THEN iffD2]) apply (fold m'_def) apply (drule leadsto_is_prev) apply (fastforce simp: n m'_def modify_map_def) apply (rule dlist') apply (rule no_0') apply simp apply clarsimp apply (rule subtree.direct_parent) apply (rule prev_leadstoI) apply (rule src) apply (insert no_0)[1] apply (clarsimp simp add: next_unfold' n modify_map_def no_0_def split: if_split_asm) apply (rule dlist) apply (rule src_0) apply (clarsimp simp: parentOf_def n modify_map_def src parent_preserved) apply clarsimp 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: next_unfold' mdb_next_unfold) apply (subst (asm) modify_map_apply, simp)+ apply (simp add: mdb_next_update split: if_split_asm) apply assumption apply (simp add: n) apply (clarsimp simp add: parentOf_def modify_map_def split: if_split_asm) done next case (trans_parent c c') thus ?case using p_neq apply - apply (simp split: if_split_asm) apply clarsimp apply (subgoal_tac "c' = mdbNext src_node") prefer 2 apply (clarsimp simp add: mdb_next_unfold n modify_map_def) apply clarsimp apply (erule subtree.trans_parent) apply (simp add: mdb_next_unfold src) apply assumption apply (clarsimp simp add: parentOf_def modify_map_def n split: if_split_asm) apply (rule conjI) apply clarsimp apply (subgoal_tac "c = mdbPrev src_node") prefer 2 apply (drule mdb_next_modify_prev [where x="mdbNext src_node" and f="\<lambda>_. dest", THEN iffD2]) apply (fold m'_def) apply (drule leadsto_is_prev) apply (fastforce simp: n m'_def modify_map_def) apply (rule dlist') apply (rule no_0') apply simp apply clarsimp apply (erule subtree.trans_parent) apply (rule prev_leadstoI) apply (rule src) apply (insert no_0)[1] apply (clarsimp simp: next_unfold' no_0_def n modify_map_def) apply (rule dlist) apply (rule src_0) apply (clarsimp simp: parentOf_def n modify_map_def src
                           parent_preserved split: if_split_asm) apply clarsimp apply (erule subtree.trans_parent) apply (clarsimp simp add: n modify_map_def mdb_next_unfold nullPointer_def split: if_split_asm) apply assumption apply (clarsimp simp add: n modify_map_def parentOf_def split: if_split_asm) done qed

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

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

goal (1 subgoal):
 1. if c = dest then m \<turnstile> p \<rightarrow> src else 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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (c = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> dest \<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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; modify_map n (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) \<turnstile> p \<leadsto> dest\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; m' \<turnstile> p \<leadsto> dest\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (6 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest\<rbrakk> \<Longrightarrow> m' dest = Some (CTE ?cap20 ?node20)
 2. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest\<rbrakk> \<Longrightarrow> valid_dlist m'
 3. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest\<rbrakk> \<Longrightarrow> no_0 m'
 4. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev ?node20\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 5. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 6. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (5 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest\<rbrakk> \<Longrightarrow> valid_dlist m'
 2. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest\<rbrakk> \<Longrightarrow> no_0 m'
 3. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 4. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 5. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest\<rbrakk> \<Longrightarrow> no_0 m'
 2. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 3. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 4. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> src
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (6 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m src = Some (CTE ?cap43 src_node)
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 4. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 5. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (5 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 4. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (5 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node; no_0 m\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 4. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> mdbPrev src_node parentOf dest; c = dest; p = mdbPrev src_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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<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; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> dest \<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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; 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; p \<noteq> dest; p \<noteq> src; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal:
No subgoals! proof (state)
this:
if c = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c

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

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

goal (1 subgoal):
 1. if c' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<rightarrow> c; if c = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c; n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> if c' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; m \<turnstile> p \<rightarrow> src\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; m \<turnstile> p \<rightarrow> src; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; m \<turnstile> p \<rightarrow> src; c' \<noteq> dest; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>n \<turnstile> dest \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; m \<turnstile> p \<rightarrow> src; c' \<noteq> dest\<rbrakk> \<Longrightarrow> c' = mdbNext src_node
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; m \<turnstile> p \<rightarrow> src; c' \<noteq> dest\<rbrakk> \<Longrightarrow> c' = mdbNext src_node
 2. \<lbrakk>n \<turnstile> dest \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; m \<turnstile> p \<rightarrow> src; c' \<noteq> dest; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; m \<turnstile> p \<rightarrow> src; c' \<noteq> dest; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> mdbNext src_node; mdbNext src_node \<noteq> 0; n \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; m \<turnstile> p \<rightarrow> src; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> mdbNext src_node
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> mdbNext src_node; mdbNext src_node \<noteq> 0; n \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 2. \<lbrakk>n \<turnstile> dest \<leadsto> mdbNext src_node; mdbNext src_node \<noteq> 0; n \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 3. \<lbrakk>n \<turnstile> dest \<leadsto> mdbNext src_node; mdbNext src_node \<noteq> 0; n \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext src_node
 4. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> mdbNext src_node; mdbNext src_node \<noteq> 0; n \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 2. \<lbrakk>n \<turnstile> dest \<leadsto> mdbNext src_node; mdbNext src_node \<noteq> 0; n \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext src_node
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> mdbNext src_node; mdbNext src_node \<noteq> 0; n \<turnstile> p parentOf mdbNext src_node; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c = dest; c' = mdbNext src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext src_node
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest\<rbrakk> \<Longrightarrow> c = mdbPrev src_node
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest\<rbrakk> \<Longrightarrow> c = mdbPrev src_node
 2. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; modify_map n (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) \<turnstile> c \<leadsto> dest\<rbrakk> \<Longrightarrow> c = mdbPrev src_node
 2. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; m' \<turnstile> c \<leadsto> dest\<rbrakk> \<Longrightarrow> c = mdbPrev src_node
 2. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest\<rbrakk> \<Longrightarrow> m' dest = Some (CTE ?cap63 ?node63)
 2. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest\<rbrakk> \<Longrightarrow> valid_dlist m'
 3. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest\<rbrakk> \<Longrightarrow> no_0 m'
 4. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev ?node63\<rbrakk> \<Longrightarrow> c = mdbPrev src_node
 5. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 6. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest\<rbrakk> \<Longrightarrow> valid_dlist m'
 2. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest\<rbrakk> \<Longrightarrow> no_0 m'
 3. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> c = mdbPrev src_node
 4. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 5. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest\<rbrakk> \<Longrightarrow> no_0 m'
 2. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> c = mdbPrev src_node
 3. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 4. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> c = mdbPrev src_node
 2. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> c \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; m \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> src
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf src
 4. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m src = Some (CTE ?cap86 src_node)
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 4. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 5. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf src
 6. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 4. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf src
 5. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node; no_0 m\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 4. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf src
 5. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf src
 4. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> src \<noteq> 0
 2. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf src
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> mdbPrev src_node \<leadsto> dest; dest \<noteq> 0; n \<turnstile> p parentOf dest; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> mdbPrev src_node; c' = dest; c = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf src
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c'
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; c' \<noteq> dest\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; c' \<noteq> dest\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> c \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c' proof (prove)
goal:
No subgoals! proof (state)
this:
if c' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'

goal:
No subgoals!