theory CSpace1_R

lemma parent_n:
  "n \<turnstile> p \<rightarrow> p' \<Longrightarrow> if p' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p'" apply (cases "p=dest", simp add: dest_no_parent_n) apply (cases "p=src", simp) apply (erule subtree.induct) apply simp apply (rule conjI) apply (clarsimp simp: n_direct_eq) apply clarsimp apply (rule direct_parent) apply (simp add: n_direct_eq) apply assumption apply (clarsimp simp: parentOf_def n src new_src_def split: if_split_asm) apply simp apply (rule conjI) apply (clarsimp simp: n_direct_eq split: if_split_asm) apply (clarsimp simp: n_direct_eq split: if_split_asm) apply (erule trans_parent, assumption, assumption) apply (clarsimp simp: parentOf_def n src new_src_def split: if_split_asm) apply (erule trans_parent, assumption, assumption) apply (clarsimp simp: parentOf_def n src new_src_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<rightarrow> p' \<Longrightarrow> if p' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<rightarrow> p'; p \<noteq> dest\<rbrakk> \<Longrightarrow> if p' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<rightarrow> p'; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> if p' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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>p \<noteq> dest; p \<noteq> src; 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)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> (c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c')
 2. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c'
 3. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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)
goal (4 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c'
 2. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; c' \<noteq> dest\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c'
 4. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; c' \<noteq> dest\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c'
 3. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'; c' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c'
 2. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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> (c'' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c'') proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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> c'' = dest \<longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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> c'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>p \<noteq> dest; p \<noteq> src; 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> c'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c''. \<lbrakk>m \<turnstile> src \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; m \<turnstile> p \<rightarrow> src; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c''
 2. \<And>c' c''. \<lbrakk>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> src; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c''. \<lbrakk>m \<turnstile> src \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> dest; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c''
 2. \<And>c' c''. \<lbrakk>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> src; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>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> src; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>c'' \<noteq> 0; n \<turnstile> p parentOf c''; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> dest; c' \<noteq> src; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c'' proof (prove)
goal:
No subgoals!