theory CSpace_R

lemma m_tranclD:
  "m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> p' \<noteq> dest \<and> (p = dest \<longrightarrow> p' = 0) \<and> n \<turnstile> p \<leadsto>\<^sup>+ p'" apply (erule trancl_induct) apply (rule context_conjI, clarsimp) apply (rule context_conjI, clarsimp) apply (cases "p = src") apply simp apply (rule trancl_trans) apply (rule r_into_trancl) apply (rule n_src_dest) apply (rule r_into_trancl) apply (simp add: n_direct_eq) apply (cases "p = dest", simp) apply (rule r_into_trancl) apply (simp add: n_direct_eq) apply clarsimp apply (rule context_conjI, clarsimp) apply (rule context_conjI, clarsimp simp: mdb_next_unfold) apply (case_tac "y = src") apply clarsimp apply (erule trancl_trans) apply (rule trancl_trans) apply (rule r_into_trancl) apply (rule n_src_dest) apply (rule r_into_trancl) apply (simp add: n_direct_eq) apply (case_tac "y = dest", simp) apply (erule trancl_trans) apply (rule r_into_trancl) apply (simp add: n_direct_eq) done

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