theory CSpace_AI

lemma parent_m_dest:
  "m \<Turnstile> p \<rightarrow> src \<Longrightarrow> n \<Turnstile> p \<rightarrow> dest" apply (erule converse_trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp: n_def cdt_parent_defs) apply (rule trancl_trans) prefer 2 apply assumption apply (rule r_into_trancl) apply (simp add: n_def cdt_parent_defs) apply (rule impI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> src \<Longrightarrow> n \<Turnstile> p \<rightarrow> dest proof (prove)
goal (2 subgoals):
 1. \<And>y. m \<Turnstile> y \<leadsto> src \<Longrightarrow> n \<Turnstile> y \<rightarrow> dest
 2. \<And>y z. \<lbrakk>m \<Turnstile> y \<leadsto> z; m \<Turnstile> z \<rightarrow> src; n \<Turnstile> z \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<Turnstile> y \<rightarrow> dest proof (prove)
goal (2 subgoals):
 1. \<And>y. m \<Turnstile> y \<leadsto> src \<Longrightarrow> n \<Turnstile> y \<leadsto> dest
 2. \<And>y z. \<lbrakk>m \<Turnstile> y \<leadsto> z; m \<Turnstile> z \<rightarrow> src; n \<Turnstile> z \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<Turnstile> y \<rightarrow> dest proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> y \<leadsto> z; m \<Turnstile> z \<rightarrow> src; n \<Turnstile> z \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<Turnstile> y \<rightarrow> dest proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>m \<Turnstile> y \<leadsto> z; m \<Turnstile> z \<rightarrow> src; n \<Turnstile> z \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<Turnstile> y \<rightarrow> ?y5 y z
 2. \<And>y z. \<lbrakk>m \<Turnstile> y \<leadsto> z; m \<Turnstile> z \<rightarrow> src; n \<Turnstile> z \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<Turnstile> ?y5 y z \<rightarrow> dest proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>m \<Turnstile> y \<leadsto> z; m \<Turnstile> z \<rightarrow> src; n \<Turnstile> z \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<Turnstile> ?y5 y z \<rightarrow> dest
 2. \<And>y z. \<lbrakk>m \<Turnstile> y \<leadsto> z; m \<Turnstile> z \<rightarrow> src; n \<Turnstile> z \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<Turnstile> y \<rightarrow> ?y5 y z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> y \<leadsto> z; m \<Turnstile> z \<rightarrow> src; n \<Turnstile> z \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<Turnstile> y \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> y \<leadsto> z; m \<Turnstile> z \<rightarrow> src; n \<Turnstile> z \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<Turnstile> y \<leadsto> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m z = Some y; (z, src) \<in> {(p, c). m c = Some p}\<^sup>+; (z, dest) \<in> {(p, c). (if c = dest then m src else m c) = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z = dest \<longrightarrow> m src = Some y proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m z = Some y; (z, src) \<in> {(p, c). m c = Some p}\<^sup>+; (z, dest) \<in> {(p, c). (if c = dest then m src else m c) = Some p}\<^sup>+; z = dest\<rbrakk> \<Longrightarrow> m src = Some y proof (prove)
goal:
No subgoals!