theory CSpace_AI

lemma parency_n_m:
  assumes "n \<Turnstile> p \<rightarrow> p'"
  shows "m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp p'" using assms proof induct case (base y) thus ?case apply (simp add: s_d_swap_def) apply safe apply (rule r_into_trancl|
                   simp add: n_def n'_def cdt_parent_defs split: if_split_asm)+ done next case (step x y) thus ?case apply - apply (erule trancl_trans) apply (simp add: s_d_swap_def split: if_split_asm) apply safe apply (simp add: n_def n'_def cdt_parent_defs split: if_split_asm) apply (rule r_into_trancl,
                  simp add: n_def n'_def cdt_parent_defs split: if_split_asm) apply (rule r_into_trancl,
                 simp add: n_def n'_def cdt_parent_defs split: if_split_asm) apply (rule r_into_trancl,
                simp add: n_def n'_def cdt_parent_defs split: if_split_asm) apply (simp add: n_def n'_def cdt_parent_defs split: if_split_asm) apply (rule r_into_trancl,
              simp add: n_def n'_def cdt_parent_defs split: if_split_asm) apply (rule r_into_trancl,
             simp add: n_def n'_def cdt_parent_defs split: if_split_asm) apply (rule r_into_trancl,
            simp add: n_def n'_def cdt_parent_defs split: if_split_asm) apply (rule r_into_trancl,
           simp add: n_def n'_def cdt_parent_defs split: if_split_asm) done qed

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

goal (1 subgoal):
 1. m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp p' proof (state)
goal (2 subgoals):
 1. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y\<rbrakk> \<Longrightarrow> m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp z proof (state)
this:
n \<Turnstile> p \<leadsto> y

goal (2 subgoals):
 1. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y\<rbrakk> \<Longrightarrow> m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp z proof (prove)
using this:
n \<Turnstile> p \<leadsto> y

goal (1 subgoal):
 1. m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y proof (prove)
goal (1 subgoal):
 1. n \<Turnstile> p \<leadsto> y \<Longrightarrow> (p = dest \<longrightarrow> y \<noteq> dest \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> m \<Turnstile> src \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> m \<Turnstile> src \<rightarrow> y))) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (y = dest \<longrightarrow> m \<Turnstile> dest \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> y \<noteq> src \<and> (y \<noteq> src \<longrightarrow> m \<Turnstile> dest \<rightarrow> y))) \<and> (p \<noteq> src \<longrightarrow> (y = dest \<longrightarrow> m \<Turnstile> p \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> m \<Turnstile> p \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> m \<Turnstile> p \<rightarrow> y)))) proof (prove)
goal (9 subgoals):
 1. \<lbrakk>n \<Turnstile> dest \<leadsto> dest; p = dest; y = dest\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<Turnstile> dest \<leadsto> src; p = dest; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> dest
 3. \<lbrakk>n \<Turnstile> dest \<leadsto> y; p = dest; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> y
 4. \<lbrakk>n \<Turnstile> src \<leadsto> dest; src \<noteq> dest; p = src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> src
 5. \<lbrakk>n \<Turnstile> src \<leadsto> src; src \<noteq> dest; p = src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>n \<Turnstile> src \<leadsto> y; src \<noteq> dest; p = src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> y
 7. \<lbrakk>n \<Turnstile> p \<leadsto> dest; p \<noteq> dest; p \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> src
 8. \<lbrakk>n \<Turnstile> p \<leadsto> src; p \<noteq> dest; p \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> dest
 9. \<lbrakk>n \<Turnstile> p \<leadsto> y; p \<noteq> dest; p \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> y proof (prove)
goal:
No subgoals! proof (state)
this:
m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y\<rbrakk> \<Longrightarrow> m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp z proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y\<rbrakk> \<Longrightarrow> m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp z proof (state)
this:
n \<Turnstile> p \<rightarrow> x
n \<Turnstile> x \<leadsto> y
m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y\<rbrakk> \<Longrightarrow> m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp z proof (prove)
using this:
n \<Turnstile> p \<rightarrow> x
n \<Turnstile> x \<leadsto> y
m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp x

goal (1 subgoal):
 1. m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp x\<rbrakk> \<Longrightarrow> m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y\<rbrakk> \<Longrightarrow> m \<Turnstile> s_d_swp x \<rightarrow> s_d_swp y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y\<rbrakk> \<Longrightarrow> (x = dest \<longrightarrow> y \<noteq> dest \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> m \<Turnstile> src \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> m \<Turnstile> src \<rightarrow> y))) \<and> (x \<noteq> dest \<longrightarrow> (x = src \<longrightarrow> (y = dest \<longrightarrow> m \<Turnstile> dest \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> y \<noteq> src \<and> (y \<noteq> src \<longrightarrow> m \<Turnstile> dest \<rightarrow> y))) \<and> (x \<noteq> src \<longrightarrow> (y = dest \<longrightarrow> m \<Turnstile> x \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> m \<Turnstile> x \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> m \<Turnstile> x \<rightarrow> y)))) proof (prove)
goal (9 subgoals):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> dest; n \<Turnstile> dest \<leadsto> dest; x = dest; y = dest\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<Turnstile> p \<rightarrow> dest; n \<Turnstile> dest \<leadsto> src; x = dest; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> dest
 3. \<lbrakk>n \<Turnstile> p \<rightarrow> dest; n \<Turnstile> dest \<leadsto> y; x = dest; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> y
 4. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> dest; src \<noteq> dest; x = src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> src
 5. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> src; src \<noteq> dest; x = src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> y; src \<noteq> dest; x = src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> y
 7. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> dest; x \<noteq> dest; x \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> src
 8. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> src; x \<noteq> dest; x \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> dest
 9. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> y proof (prove)
goal (8 subgoals):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> dest; n \<Turnstile> dest \<leadsto> src; x = dest; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> dest
 2. \<lbrakk>n \<Turnstile> p \<rightarrow> dest; n \<Turnstile> dest \<leadsto> y; x = dest; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> y
 3. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> dest; src \<noteq> dest; x = src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> src
 4. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> src; src \<noteq> dest; x = src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> y; src \<noteq> dest; x = src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> y
 6. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> dest; x \<noteq> dest; x \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> src
 7. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> src; x \<noteq> dest; x \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> dest
 8. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> y proof (prove)
goal (7 subgoals):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> dest; n \<Turnstile> dest \<leadsto> y; x = dest; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> src \<rightarrow> y
 2. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> dest; src \<noteq> dest; x = src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> src
 3. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> src; src \<noteq> dest; x = src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> y; src \<noteq> dest; x = src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> y
 5. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> dest; x \<noteq> dest; x \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> src
 6. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> src; x \<noteq> dest; x \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> dest
 7. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> y proof (prove)
goal (6 subgoals):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> dest; src \<noteq> dest; x = src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> src
 2. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> src; src \<noteq> dest; x = src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> y; src \<noteq> dest; x = src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> y
 4. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> dest; x \<noteq> dest; x \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> src
 5. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> src; x \<noteq> dest; x \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> dest
 6. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> y proof (prove)
goal (5 subgoals):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> src; src \<noteq> dest; x = src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> y; src \<noteq> dest; x = src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> y
 3. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> dest; x \<noteq> dest; x \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> src
 4. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> src; x \<noteq> dest; x \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> dest
 5. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> y proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> src; n \<Turnstile> src \<leadsto> y; src \<noteq> dest; x = src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> dest \<rightarrow> y
 2. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> dest; x \<noteq> dest; x \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> src
 3. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> src; x \<noteq> dest; x \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> dest
 4. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> dest; x \<noteq> dest; x \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> src
 2. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> src; x \<noteq> dest; x \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> dest
 3. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> src; x \<noteq> dest; x \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> dest
 2. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<Turnstile> p \<rightarrow> x; n \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> m \<Turnstile> x \<rightarrow> y proof (prove)
goal:
No subgoals! proof (state)
this:
m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y

goal:
No subgoals!