theory CNode_IF

lemma all_children_descendants_equal:
  "\<lbrakk> equiv_for P id s t; all_children P s; all_children P t; P slot \<rbrakk>
     \<Longrightarrow> descendants_of slot s = descendants_of slot t" apply (clarsimp | rule equalityI)+ apply (frule_tac p="(a, b)" and q="slot" and m=s in all_children_descendants_of) apply (simp)+ apply (simp add: descendants_of_def cdt_parent_rel_def is_cdt_parent_def) apply (rule_tac r'="{(p, c). s c = Some p}" and Q="P" in trancl_subset_equivalence) apply (clarsimp)+ apply (frule_tac p="(aa, ba)" and q="slot" in all_children_descendants_of) apply (fastforce simp: descendants_of_def cdt_parent_rel_def is_cdt_parent_def)+ apply (fastforce simp: equiv_for_def) apply (clarsimp) apply (frule_tac p="(a, b)" and q="slot" and m=t in all_children_descendants_of) apply (simp)+ apply (simp add: descendants_of_def cdt_parent_rel_def is_cdt_parent_def) apply (rule_tac r'="{(p, c). t c = Some p}" and Q="P" in trancl_subset_equivalence) apply (clarsimp)+ apply (frule_tac p="(aa, ba)" and q="slot" and m=t in all_children_descendants_of) apply (fastforce simp: equiv_for_def descendants_of_def cdt_parent_rel_def is_cdt_parent_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot s = descendants_of slot t proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot s\<rbrakk> \<Longrightarrow> (a, b) \<in> descendants_of slot t
 2. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot t \<subseteq> descendants_of slot s proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot s\<rbrakk> \<Longrightarrow> (a, b) \<in> descendants_of slot s
 2. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot s\<rbrakk> \<Longrightarrow> P slot
 3. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot s; P (a, b)\<rbrakk> \<Longrightarrow> (a, b) \<in> descendants_of slot t
 4. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot t \<subseteq> descendants_of slot s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot s; P (a, b)\<rbrakk> \<Longrightarrow> (a, b) \<in> descendants_of slot t
 2. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot t \<subseteq> descendants_of slot s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+
 2. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot t \<subseteq> descendants_of slot s proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+
 2. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> \<forall>x. (slot, x) \<in> {(p, c). s c = Some p}\<^sup>+ \<longrightarrow> P x
 3. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> \<forall>x y. P x \<longrightarrow> ((y, x) \<in> {(p, c). t c = Some p}) = ((y, x) \<in> {(p, c). s c = Some p})
 4. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot t \<subseteq> descendants_of slot s proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b); (slot, aa, ba) \<in> {(p, c). s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> P (aa, ba)
 2. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> \<forall>x y. P x \<longrightarrow> ((y, x) \<in> {(p, c). t c = Some p}) = ((y, x) \<in> {(p, c). s c = Some p})
 3. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot t \<subseteq> descendants_of slot s proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b); (slot, aa, ba) \<in> {(p, c). s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of slot s
 2. \<And>a b aa ba. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b); (slot, aa, ba) \<in> {(p, c). s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> P slot
 3. \<And>a b aa ba. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b); (slot, aa, ba) \<in> {(p, c). s c = Some p}\<^sup>+; P (aa, ba)\<rbrakk> \<Longrightarrow> P (aa, ba)
 4. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> \<forall>x y. P x \<longrightarrow> ((y, x) \<in> {(p, c). t c = Some p}) = ((y, x) \<in> {(p, c). s c = Some p})
 5. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot t \<subseteq> descendants_of slot s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> \<forall>x y. P x \<longrightarrow> ((y, x) \<in> {(p, c). t c = Some p}) = ((y, x) \<in> {(p, c). s c = Some p})
 2. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot t \<subseteq> descendants_of slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot\<rbrakk> \<Longrightarrow> descendants_of slot t \<subseteq> descendants_of slot s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot t\<rbrakk> \<Longrightarrow> (a, b) \<in> descendants_of slot s proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot t\<rbrakk> \<Longrightarrow> (a, b) \<in> descendants_of slot t
 2. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot t\<rbrakk> \<Longrightarrow> P slot
 3. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot t; P (a, b)\<rbrakk> \<Longrightarrow> (a, b) \<in> descendants_of slot s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (a, b) \<in> descendants_of slot t; P (a, b)\<rbrakk> \<Longrightarrow> (a, b) \<in> descendants_of slot s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> (slot, a, b) \<in> {(p, c). s c = Some p}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+
 2. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> \<forall>x. (slot, x) \<in> {(p, c). t c = Some p}\<^sup>+ \<longrightarrow> P x
 3. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> \<forall>x y. P x \<longrightarrow> ((y, x) \<in> {(p, c). s c = Some p}) = ((y, x) \<in> {(p, c). t c = Some p}) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b); (slot, aa, ba) \<in> {(p, c). t c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> P (aa, ba)
 2. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> \<forall>x y. P x \<longrightarrow> ((y, x) \<in> {(p, c). s c = Some p}) = ((y, x) \<in> {(p, c). t c = Some p}) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b); (slot, aa, ba) \<in> {(p, c). t c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of slot t
 2. \<And>a b aa ba. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b); (slot, aa, ba) \<in> {(p, c). t c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> P slot
 3. \<And>a b aa ba. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b); (slot, aa, ba) \<in> {(p, c). t c = Some p}\<^sup>+; P (aa, ba)\<rbrakk> \<Longrightarrow> P (aa, ba)
 4. \<And>a b. \<lbrakk>equiv_for P id s t; all_children P s; all_children P t; P slot; (slot, a, b) \<in> {(p, c). t c = Some p}\<^sup>+; P (a, b)\<rbrakk> \<Longrightarrow> \<forall>x y. P x \<longrightarrow> ((y, x) \<in> {(p, c). s c = Some p}) = ((y, x) \<in> {(p, c). t c = Some p}) proof (prove)
goal:
No subgoals!