theory Untyped_R

lemma n'_trancl_eq:
  "n' \<turnstile> p \<leadsto>\<^sup>+ p' =
  (if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ p'
   else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent  then m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site
   else m \<turnstile> p \<leadsto>\<^sup>+ p')" apply simp apply (intro conjI impI iffI) apply (drule n'_tranclD) apply simp apply simp apply (drule n'_tranclD) apply simp apply (erule disjE) apply (drule m_tranclD)+ apply simp apply (drule m_tranclD) apply simp apply (erule trancl_trans) apply (rule r_into_trancl) apply (simp add: n'_direct_eq) apply (drule n'_tranclD, simp) apply (erule disjE) apply (drule m_tranclD) apply simp apply simp apply (rule r_into_trancl) apply (simp add: n'_direct_eq) apply (drule n'_tranclD, simp) apply simp apply (cases "p' = site", simp) apply (drule m_tranclD) apply clarsimp apply (drule tranclD) apply (clarsimp simp: n'_direct_eq) apply (simp add: rtrancl_eq_or_trancl) apply (drule n'_tranclD, simp) apply clarsimp apply (drule m_tranclD, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' \<turnstile> p \<leadsto>\<^sup>+ p' = (if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ p' else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent then m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site else m \<turnstile> p \<leadsto>\<^sup>+ p') proof (prove)
goal (1 subgoal):
 1. (m \<turnstile> p \<leadsto>\<^sup>+ parent \<longrightarrow> (p = site \<longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p' = m \<turnstile> parent \<leadsto>\<^sup>+ p') \<and> (p \<noteq> site \<longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' = (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site))) \<and> (p = parent \<longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p' = (m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site)) \<and> ((p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent \<longrightarrow> (p = site \<longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p' = m \<turnstile> parent \<leadsto>\<^sup>+ p') \<and> (p \<noteq> site \<longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' = m \<turnstile> p \<leadsto>\<^sup>+ p')) proof (prove)
goal (10 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 2. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 3. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site
 4. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 6. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 8. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 9. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 10. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (10 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p = site; if site = site then m \<turnstile> parent \<leadsto>\<^sup>+ p' else if m \<turnstile> site \<leadsto>\<^sup>+ parent \<or> site = parent then m \<turnstile> site \<leadsto>\<^sup>+ p' \<or> p' = site else m \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 2. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 3. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site
 4. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 6. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 8. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 9. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 10. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (9 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 2. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site
 3. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 4. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 5. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 8. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 9. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (8 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site
 2. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 4. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 8. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (8 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ p' else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent then m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site else m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site
 2. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 4. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 8. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 3. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (8 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 4. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 8. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (8 subgoals):
 1. \<lbrakk>p \<noteq> site; parent \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ parent; p' \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 4. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 8. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ parent; p \<noteq> site; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 3. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p \<noteq> site; p' = site; parent \<noteq> site \<and> n' \<turnstile> p \<leadsto>\<^sup>+ parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 3. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p \<noteq> site; p' = site; n' \<turnstile> p \<leadsto>\<^sup>+ parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ site
 2. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 3. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p \<noteq> site; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ site
 2. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 3. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p \<noteq> site; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto> site
 2. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 3. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 7. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>p = parent; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
 2. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>p = parent; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p = parent; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>p = parent; p' \<noteq> site \<and> n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p = parent; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 6. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p = parent; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p = parent; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto>\<^sup>+ site
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p = parent; p' = site\<rbrakk> \<Longrightarrow> n' \<turnstile> parent \<leadsto> site
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; n' \<turnstile> site \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 4. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = site; m \<turnstile> parent \<leadsto>\<^sup>+ p'; p' \<noteq> site\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = site; p' \<noteq> site; p' \<noteq> site \<and> n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = site; p' \<noteq> site; n' \<turnstile> parent \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = site; p' \<noteq> site; \<exists>z. n' \<turnstile> parent \<leadsto> z \<and> n' \<turnstile> z \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = site; p' \<noteq> site; n' \<turnstile> site \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> n' \<turnstile> site \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; n' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p, parent) \<notin> (mdb_next_rel m)\<^sup>+ \<and> p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> site; m \<turnstile> p \<leadsto>\<^sup>+ p'; (p, parent) \<notin> (mdb_next_rel m)\<^sup>+; p \<noteq> parent\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal:
No subgoals!