theory CSpace_R

lemma n_trancl_eq':
  "n \<turnstile> p \<leadsto>\<^sup>+ p' =
  (if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src
   else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p'
   else m \<turnstile> p \<leadsto>\<^sup>+ p')" apply (rule iffI) apply (erule trancl_induct) apply (clarsimp simp: n_direct_eq) apply (fastforce split: if_split_asm) apply (clarsimp simp: n_direct_eq split: if_split_asm) apply fastforce apply fastforce apply (fastforce intro: trancl_trans) apply (fastforce intro: trancl_trans) apply (simp split: if_split_asm) apply (drule rtranclD) apply (erule disjE) apply (fastforce intro: n_src_dest) apply (clarsimp dest!: m_tranclD) apply (erule trancl_trans) apply (fastforce intro: n_src_dest) apply (drule m_tranclD, clarsimp) apply (drule tranclD) apply clarsimp apply (insert n_src_dest)[1] apply (drule (1) next_single_value) apply (clarsimp simp: rtrancl_eq_or_trancl) apply (drule m_tranclD) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' = (if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p') proof (prove)
goal (2 subgoals):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p'
 2. if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<And>y. n \<turnstile> p \<leadsto> y \<Longrightarrow> if y = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ y else m \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; if y = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ y else m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if z = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ z else m \<turnstile> p \<leadsto>\<^sup>+ z
 3. if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<And>y. if p = src then y = dest else if p = dest then m \<turnstile> src \<leadsto> y else m \<turnstile> p \<leadsto> y \<Longrightarrow> (p = dest \<longrightarrow> (y = dest \<longrightarrow> m \<turnstile> dest \<leadsto>\<^sup>* src) \<and> (y \<noteq> dest \<longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ y)) \<and> (p \<noteq> dest \<longrightarrow> (y = dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* src) \<and> (y \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ y))
 2. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; if y = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ y else m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if z = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ z else m \<turnstile> p \<leadsto>\<^sup>+ z
 3. if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; if y = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ y else m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if z = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ z else m \<turnstile> p \<leadsto>\<^sup>+ z
 2. if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ src; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* src
 2. \<And>z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ dest; m \<turnstile> src \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> (z = dest \<longrightarrow> m \<turnstile> dest \<leadsto>\<^sup>* src) \<and> (z \<noteq> dest \<longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ z)) \<and> (p \<noteq> dest \<longrightarrow> z \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z)
 3. \<And>y z. \<lbrakk>n \<turnstile> dest \<leadsto>\<^sup>+ y; y \<noteq> src; m \<turnstile> y \<leadsto> z; y \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> (z = dest \<longrightarrow> m \<turnstile> dest \<leadsto>\<^sup>* src) \<and> (z \<noteq> dest \<longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ z)
 4. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> src; m \<turnstile> y \<leadsto> z; y \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> (z = dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* src) \<and> (z \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z)
 5. if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ dest; m \<turnstile> src \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> (z = dest \<longrightarrow> m \<turnstile> dest \<leadsto>\<^sup>* src) \<and> (z \<noteq> dest \<longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ z)) \<and> (p \<noteq> dest \<longrightarrow> z \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z)
 2. \<And>y z. \<lbrakk>n \<turnstile> dest \<leadsto>\<^sup>+ y; y \<noteq> src; m \<turnstile> y \<leadsto> z; y \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> (z = dest \<longrightarrow> m \<turnstile> dest \<leadsto>\<^sup>* src) \<and> (z \<noteq> dest \<longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ z)
 3. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> src; m \<turnstile> y \<leadsto> z; y \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> (z = dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* src) \<and> (z \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z)
 4. if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<And>y z. \<lbrakk>n \<turnstile> dest \<leadsto>\<^sup>+ y; y \<noteq> src; m \<turnstile> y \<leadsto> z; y \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> (z = dest \<longrightarrow> m \<turnstile> dest \<leadsto>\<^sup>* src) \<and> (z \<noteq> dest \<longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ z)
 2. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> src; m \<turnstile> y \<leadsto> z; y \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> (z = dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* src) \<and> (z \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z)
 3. if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> src; m \<turnstile> y \<leadsto> z; y \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> (z = dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* src) \<and> (z \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z)
 2. if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. if p' = dest then m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p' = dest; m \<turnstile> p \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ dest
 2. \<lbrakk>p' \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p' = dest; p = src \<or> p \<noteq> src \<and> m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ dest
 2. \<lbrakk>p' \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p' = dest; p = src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ dest
 2. \<lbrakk>p' = dest; p \<noteq> src \<and> m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ dest
 3. \<lbrakk>p' \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 4. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p' = dest; p \<noteq> src \<and> m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ dest
 2. \<lbrakk>p' \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p' = dest; p \<noteq> src; p \<noteq> dest; n \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ dest
 2. \<lbrakk>p' \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p' = dest; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto>\<^sup>+ dest
 2. \<lbrakk>p' \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' \<noteq> dest; p = dest; m \<turnstile> src \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p = dest; p' \<noteq> dest; n \<turnstile> src \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p = dest; p' \<noteq> dest; \<exists>z. n \<turnstile> src \<leadsto> z \<and> n \<turnstile> z \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p = dest; p' \<noteq> dest; n \<turnstile> src \<leadsto> z; n \<turnstile> z \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p = dest; p' \<noteq> dest; n \<turnstile> src \<leadsto> z; n \<turnstile> z \<leadsto>\<^sup>* p'; n \<turnstile> src \<leadsto> dest\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p = dest; p' \<noteq> dest; n \<turnstile> z \<leadsto>\<^sup>* p'; n \<turnstile> src \<leadsto> dest; z = dest\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<noteq> dest; p \<noteq> dest; p' \<noteq> dest \<and> (p = dest \<longrightarrow> p' = 0) \<and> n \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal:
No subgoals!