theory Untyped_R

lemma m_tranclD:
  assumes m: "m \<turnstile> p \<leadsto>\<^sup>+ p'"
  shows "p' \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ p'" proof - from m have "p = site \<longrightarrow> p' = 0" by clarsimp with mdb_chain_0_n' m show ?thesis apply - apply (erule trancl_induct) apply (rule context_conjI) apply clarsimp apply (cases "p = site") apply (simp add: mdb_chain_0_def site_in_dom) apply (cases "p = parent") apply simp apply (rule trancl_trans) apply (rule r_into_trancl) apply (simp add: n'_direct_eq) apply (rule r_into_trancl) apply (simp add: n'_direct_eq) apply (rule r_into_trancl) apply (simp add: n'_direct_eq) apply (rule context_conjI) apply clarsimp apply clarsimp apply (erule trancl_trans) apply (case_tac "y = parent") apply simp apply (rule trancl_trans) apply (rule r_into_trancl) apply (simp add: n'_direct_eq) apply (rule r_into_trancl) apply (simp add: n'_direct_eq) apply (rule r_into_trancl) apply (simp add: n'_direct_eq) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p' \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (state)
goal (1 subgoal):
 1. p' \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (chain)
picking this:
m \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ p'

goal (1 subgoal):
 1. p = site \<longrightarrow> p' = 0 proof (state)
this:
p = site \<longrightarrow> p' = 0

goal (1 subgoal):
 1. p' \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (chain)
picking this:
mdb_chain_0 n'
m \<turnstile> p \<leadsto>\<^sup>+ p'
p = site \<longrightarrow> p' = 0 proof (prove)
using this:
mdb_chain_0 n'
m \<turnstile> p \<leadsto>\<^sup>+ p'
p = site \<longrightarrow> p' = 0

goal (1 subgoal):
 1. p' \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_chain_0 n'; m \<turnstile> p \<leadsto>\<^sup>+ p'; p = site \<longrightarrow> p' = 0\<rbrakk> \<Longrightarrow> p' \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> y \<noteq> site
 2. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 3. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 3. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 3. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>m \<turnstile> parent \<leadsto> y; y \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ y
 2. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 3. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>m \<turnstile> parent \<leadsto> y; y \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ ?y16 y
 2. \<And>y. \<lbrakk>m \<turnstile> parent \<leadsto> y; y \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> ?y16 y \<leadsto>\<^sup>+ y
 3. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 4. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>m \<turnstile> parent \<leadsto> y; y \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto> ?y16 y
 2. \<And>y. \<lbrakk>m \<turnstile> parent \<leadsto> y; y \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> ?y16 y \<leadsto>\<^sup>+ y
 3. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 4. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>m \<turnstile> parent \<leadsto> y; y \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ y
 2. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 3. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>m \<turnstile> parent \<leadsto> y; y \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto> y
 2. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 3. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto> y; y \<noteq> site; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto> y
 2. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> site
 2. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>mdb_chain_0 n'; p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; y = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto>\<^sup>+ z
 2. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; y \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ parent; m \<turnstile> parent \<leadsto> z; z \<noteq> site; y = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ z
 2. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; y \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ parent; m \<turnstile> parent \<leadsto> z; z \<noteq> site; y = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ ?y39 y z
 2. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ parent; m \<turnstile> parent \<leadsto> z; z \<noteq> site; y = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> ?y39 y z \<leadsto>\<^sup>+ z
 3. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; y \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ parent; m \<turnstile> parent \<leadsto> z; z \<noteq> site; y = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto> ?y39 y z
 2. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ parent; m \<turnstile> parent \<leadsto> z; z \<noteq> site; y = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> ?y39 y z \<leadsto>\<^sup>+ z
 3. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; y \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ parent; m \<turnstile> parent \<leadsto> z; z \<noteq> site; y = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ z
 2. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; y \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ parent; m \<turnstile> parent \<leadsto> z; z \<noteq> site; y = parent\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto> z
 2. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; y \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; y \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>p = site \<longrightarrow> p' = 0; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> site; y \<noteq> site; y \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> y \<leadsto> z proof (prove)
goal:
No subgoals! proof (state)
this:
p' \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ p'

goal:
No subgoals!