theory Untyped_R

lemma parent_m_n:
  assumes "m \<turnstile> p \<rightarrow> p'"
  shows "if p' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> p' else n \<turnstile> p \<rightarrow> p'" using assms proof induct case (direct_parent c) thus ?case apply (cases "p = parent") apply simp apply (rule conjI, clarsimp) apply clarsimp apply (rule subtree.trans_parent [where c'=site]) apply (rule n_site_child) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (clarsimp simp: new_parent_def parent) apply simp apply (subgoal_tac "n \<turnstile> p \<rightarrow> c") prefer 2 apply (rule subtree.direct_parent) apply (clarsimp simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (fastforce simp: new_parent_def parent) apply clarsimp apply (erule subtree_trans) apply (rule n_site_child) done next case (trans_parent c d) thus ?case apply - apply (cases "c = site", simp) apply (cases "d = site", simp) apply (cases "c = parent") apply clarsimp apply (erule subtree.trans_parent [where c'=site]) apply (clarsimp simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (rule conjI, clarsimp) apply (clarsimp simp: new_parent_def parent) apply clarsimp apply (subgoal_tac "n \<turnstile> p \<rightarrow> d") apply clarsimp apply (erule subtree_trans, rule n_site_child) apply (erule subtree.trans_parent) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (fastforce simp: parent new_parent_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if p' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> p' else n \<turnstile> p \<rightarrow> p' proof (prove)
using this:
m \<turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. if p' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> p' else n \<turnstile> p \<rightarrow> p' proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> if c' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c' else n \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c' else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c'' else n \<turnstile> p \<rightarrow> c'' proof (state)
this:
m \<turnstile> p \<leadsto> c
c \<noteq> 0
m \<turnstile> p parentOf c

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> if c' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c' else n \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c' else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c'' else n \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> p \<leadsto> c
c \<noteq> 0
m \<turnstile> p parentOf c

goal (1 subgoal):
 1. if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p = parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent\<rbrakk> \<Longrightarrow> (c = parent \<longrightarrow> n \<turnstile> parent \<rightarrow> site \<and> n \<turnstile> parent \<rightarrow> parent) \<and> (c \<noteq> parent \<longrightarrow> n \<turnstile> parent \<rightarrow> c)
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent\<rbrakk> \<Longrightarrow> c \<noteq> parent \<longrightarrow> n \<turnstile> parent \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> parent \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> parent \<rightarrow> site
 2. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> site \<leadsto> c
 3. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> parent parentOf c
 5. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> site \<leadsto> c
 2. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> parent parentOf c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> parent parentOf c
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; m \<turnstile> parent parentOf c; p = parent; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> parent parentOf c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> parent \<leadsto> c; c \<noteq> 0; p = parent; c \<noteq> parent; m c = Some cte; m parent = Some cte'; isMDBParentOf cte' cte; c \<noteq> site\<rbrakk> \<Longrightarrow> isMDBParentOf new_parent cte
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> (c = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (c \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (c \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> c)
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (c \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (c \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (c \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (c \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; p \<noteq> parent; m c = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> (c = site \<longrightarrow> (p = site \<longrightarrow> isMDBParentOf new_site new_site) \<and> (p \<noteq> site \<longrightarrow> isMDBParentOf cte' new_site)) \<and> (c \<noteq> site \<longrightarrow> (p = site \<longrightarrow> (c = parent \<longrightarrow> isMDBParentOf new_site new_parent) \<and> (c \<noteq> parent \<longrightarrow> isMDBParentOf new_site cte)) \<and> (p \<noteq> site \<longrightarrow> c = parent \<longrightarrow> isMDBParentOf cte' new_parent))
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (c \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; p \<noteq> parent; n \<turnstile> p \<rightarrow> c\<rbrakk> \<Longrightarrow> (c = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (c \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> parent; m \<turnstile> p parentOf parent; p \<noteq> parent; n \<turnstile> p \<rightarrow> parent; c = parent\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> site proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> parent; m \<turnstile> p parentOf parent; p \<noteq> parent; c = parent\<rbrakk> \<Longrightarrow> n \<turnstile> parent \<rightarrow> site proof (prove)
goal:
No subgoals! proof (state)
this:
if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c' else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c'' else n \<turnstile> p \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c' else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c'' else n \<turnstile> p \<rightarrow> c'' proof (state)
this:
m \<turnstile> p \<rightarrow> c
if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c
m \<turnstile> c \<leadsto> d
d \<noteq> 0
m \<turnstile> p parentOf d

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; if c' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c' else n \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c'' else n \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> p \<rightarrow> c
if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c
m \<turnstile> c \<leadsto> d
d \<noteq> 0
m \<turnstile> p parentOf d

goal (1 subgoal):
 1. if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c = parent\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> parent; m \<turnstile> parent \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> site; c = parent; n \<turnstile> p \<rightarrow> site; n \<turnstile> p \<rightarrow> parent; d \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> parent; m \<turnstile> parent \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> site; c = parent; n \<turnstile> p \<rightarrow> parent; d \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> site \<leadsto> d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> parent; m \<turnstile> parent \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> site; c = parent; n \<turnstile> p \<rightarrow> parent; d \<noteq> parent\<rbrakk> \<Longrightarrow> d \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> parent; m \<turnstile> parent \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> site; c = parent; n \<turnstile> p \<rightarrow> parent; d \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> parent; m \<turnstile> parent \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> site; c = parent; n \<turnstile> p \<rightarrow> parent; d \<noteq> parent\<rbrakk> \<Longrightarrow> d \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<rightarrow> parent; m \<turnstile> parent \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> site; c = parent; n \<turnstile> p \<rightarrow> parent; d \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> parent; m \<turnstile> parent \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; d \<noteq> site; c = parent; n \<turnstile> p \<rightarrow> parent; d \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> p \<rightarrow> parent; m \<turnstile> parent \<leadsto> d; d \<noteq> 0; d \<noteq> site; c = parent; m(site \<mapsto> new_site, parent \<mapsto> new_parent) \<turnstile> p \<rightarrow> parent; d \<noteq> parent; m d = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> (p = site \<longrightarrow> isMDBParentOf new_site cte) \<and> (p \<noteq> site \<longrightarrow> p = parent \<longrightarrow> isMDBParentOf new_parent cte)
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> p \<rightarrow> parent; m \<turnstile> parent \<leadsto> d; d \<noteq> 0; d \<noteq> site; c = parent; m(site \<mapsto> new_site, parent \<mapsto> new_parent) \<turnstile> p \<rightarrow> parent; d \<noteq> parent; m d = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> p \<noteq> site \<longrightarrow> p = parent \<longrightarrow> isMDBParentOf new_parent cte
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; if c = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> c else n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> (d = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (d \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> d) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent; n \<turnstile> p \<rightarrow> d\<rbrakk> \<Longrightarrow> (d = parent \<longrightarrow> n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> parent) \<and> (d \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> d)
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> parent; m \<turnstile> p parentOf parent; c \<noteq> site; c \<noteq> parent; n \<turnstile> p \<rightarrow> parent; d = parent\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> site
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; n \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto> d
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> d \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> d \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; m \<turnstile> p parentOf d; c \<noteq> site; d \<noteq> site; c \<noteq> parent\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf d proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> d; d \<noteq> 0; c \<noteq> site; d \<noteq> site; c \<noteq> parent; m d = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> (p = site \<longrightarrow> (d = parent \<longrightarrow> isMDBParentOf new_site new_parent) \<and> (d \<noteq> parent \<longrightarrow> isMDBParentOf new_site cte)) \<and> (p \<noteq> site \<longrightarrow> (p = parent \<longrightarrow> (d = parent \<longrightarrow> isMDBParentOf new_parent new_parent) \<and> (d \<noteq> parent \<longrightarrow> isMDBParentOf new_parent cte)) \<and> (p \<noteq> parent \<longrightarrow> d = parent \<longrightarrow> isMDBParentOf cte' new_parent)) proof (prove)
goal:
No subgoals! proof (state)
this:
if d = parent then n \<turnstile> p \<rightarrow> site \<and> n \<turnstile> p \<rightarrow> d else n \<turnstile> p \<rightarrow> d

goal:
No subgoals!