theory CSpace1_R

lemma parency_m_n:
  assumes "m \<turnstile> p \<rightarrow> p'"
  shows "n \<turnstile> s_d_swp p \<rightarrow> s_d_swp p'" using assms proof induct case (direct_parent c) thus ?case apply - apply (rule subtree.direct_parent) apply (subst (asm) next_m_n, assumption) apply simp apply (subst (asm) parent_of_m_n, assumption) done next case (trans_parent c c') thus ?case apply - apply (erule subtree.trans_parent) apply (subst (asm) next_m_n, assumption) apply simp apply (subst (asm) parent_of_m_n, assumption) done qed

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

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

goal (1 subgoal):
 1. n \<turnstile> s_d_swp p \<rightarrow> s_d_swp c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p \<rightarrow> s_d_swp c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p \<leadsto> s_d_swp c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> s_d_swp c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p parentOf s_d_swp c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> s_d_swp c \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p parentOf s_d_swp c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p parentOf s_d_swp c proof (prove)
goal:
No subgoals! proof (state)
this:
n \<turnstile> s_d_swp p \<rightarrow> s_d_swp c

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

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

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

goal:
No subgoals!