theory CSpace1_R

lemma parent_m_n:
  assumes "m \<turnstile> p \<rightarrow> p'"
  shows "if p' = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> p' else n \<turnstile> p \<rightarrow> p'" using assms proof induct case (direct_parent c) thus ?case apply (cases "p = src") apply simp apply (rule conjI, clarsimp) apply clarsimp apply (rule subtree.trans_parent [where c'=dest]) apply (rule n_dest_child) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (clarsimp simp: new_src_def src) apply simp apply (subgoal_tac "n \<turnstile> p \<rightarrow> c") prefer 2 apply (rule subtree.direct_parent) apply (clarsimp simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (fastforce simp: new_src_def src) apply clarsimp apply (erule subtree_trans) apply (rule n_dest_child) done next case (trans_parent c d) thus ?case apply - apply (cases "c = dest", simp) apply (cases "d = dest", simp) apply (cases "c = src") apply clarsimp apply (erule subtree.trans_parent [where c'=dest]) apply (clarsimp simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (rule conjI, clarsimp) apply (clarsimp simp: new_src_def src) apply clarsimp apply (subgoal_tac "n \<turnstile> p \<rightarrow> d") apply clarsimp apply (erule subtree_trans, rule n_dest_child) apply (erule subtree.trans_parent) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (fastforce simp: src new_src_def) done qed

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

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

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

goal (1 subgoal):
 1. if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p = src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> src \<rightarrow> dest \<and> n \<turnstile> src \<rightarrow> src) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> src \<rightarrow> c)
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src\<rbrakk> \<Longrightarrow> c \<noteq> src \<longrightarrow> n \<turnstile> src \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto> c
 3. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src parentOf c
 5. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto> c
 2. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src parentOf c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src parentOf c
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; m \<turnstile> src parentOf c; p = src; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src parentOf c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> src \<leadsto> c; c \<noteq> 0; p = src; c \<noteq> src; m c = Some cte; m src = Some cte'; isMDBParentOf cte' cte; c \<noteq> dest\<rbrakk> \<Longrightarrow> isMDBParentOf new_src cte
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c)
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; p \<noteq> src; m c = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> (c = dest \<longrightarrow> (p = dest \<longrightarrow> isMDBParentOf new_dest new_dest) \<and> (p \<noteq> dest \<longrightarrow> isMDBParentOf cte' new_dest)) \<and> (c \<noteq> dest \<longrightarrow> (p = dest \<longrightarrow> (c = src \<longrightarrow> isMDBParentOf new_dest new_src) \<and> (c \<noteq> src \<longrightarrow> isMDBParentOf new_dest cte)) \<and> (p \<noteq> dest \<longrightarrow> c = src \<longrightarrow> isMDBParentOf cte' new_src))
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> src; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src; p \<noteq> src; n \<turnstile> p \<rightarrow> src; c = src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src; p \<noteq> src; c = src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<rightarrow> dest proof (prove)
goal:
No subgoals! proof (state)
this:
if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c

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

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

goal (1 subgoal):
 1. if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c = src\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> dest; c = src; n \<turnstile> p \<rightarrow> dest; n \<turnstile> p \<rightarrow> src; d \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> dest; c = src; n \<turnstile> p \<rightarrow> src; d \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto> d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> dest; c = src; n \<turnstile> p \<rightarrow> src; d \<noteq> src\<rbrakk> \<Longrightarrow> d \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> dest; c = src; n \<turnstile> p \<rightarrow> src; d \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> dest; c = src; n \<turnstile> p \<rightarrow> src; d \<noteq> src\<rbrakk> \<Longrightarrow> d \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> dest; c = src; n \<turnstile> p \<rightarrow> src; d \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> dest; c = src; n \<turnstile> p \<rightarrow> src; d \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> d; d \<noteq> 0; d \<noteq> dest; c = src; m(dest \<mapsto> new_dest, src \<mapsto> new_src) \<turnstile> p \<rightarrow> src; d \<noteq> src; m d = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> isMDBParentOf new_dest cte) \<and> (p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> isMDBParentOf new_src cte)
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> d; d \<noteq> 0; d \<noteq> dest; c = src; m(dest \<mapsto> new_dest, src \<mapsto> new_src) \<turnstile> p \<rightarrow> src; d \<noteq> src; m d = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> isMDBParentOf new_src cte
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> (d = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (d \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> d) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src; n \<turnstile> p \<rightarrow> d\<rbrakk> \<Longrightarrow> (d = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> src) \<and> (d \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> d)
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> src; m \<turnstile> p parentOf src; c \<noteq> dest; c \<noteq> src; n \<turnstile> p \<rightarrow> src; d = src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto> d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> d \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> d \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> dest; d \<noteq> dest; c \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; c \<noteq> dest; d \<noteq> dest; c \<noteq> src; m d = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> (d = src \<longrightarrow> isMDBParentOf new_dest new_src) \<and> (d \<noteq> src \<longrightarrow> isMDBParentOf new_dest cte)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (d = src \<longrightarrow> isMDBParentOf new_src new_src) \<and> (d \<noteq> src \<longrightarrow> isMDBParentOf new_src cte)) \<and> (p \<noteq> src \<longrightarrow> d = src \<longrightarrow> isMDBParentOf cte' new_src)) proof (prove)
goal:
No subgoals! proof (state)
this:
if d = src then n \<turnstile> p \<rightarrow> dest \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d

goal:
No subgoals!