theory Deterministic_AI

lemma next_slot_setD:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>next \<in> next_slot_set slot t m; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk>
    \<Longrightarrow> next \<in> descendants_of slot m \<or> next \<in> next_sib_set slot t m \<or>
  (\<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q})" apply(subst(asm) next_slot_set_def) apply(simp) apply(induct "next" slot rule: trancl.induct) apply simp apply(simp add: next_slot_def split: if_split_asm) apply(simp add: next_child_def valid_list_2_def descendants_of_def cdt_parent_defs) apply(case_tac "t b", simp, fastforce) apply(drule(2) next_not_childD) apply(erule disjE) apply(fastforce simp: next_sib_set_def) apply(fastforce simp: next_sib_set_def) apply(simp) apply(erule disjE) apply(simp add: next_slot_def split: if_split_asm) apply(rule disjI1) apply(rule_tac b=b in descendants_trans) apply(simp) apply(fastforce dest: next_childD simp: descendants_of_def cdt_parent_defs) apply(drule(2) next_not_childD) apply(fastforce simp: next_sib_set_def) apply(erule disjE) apply(simp add: next_slot_def split: if_split_asm) apply(rule disjI1) apply(fastforce intro: child_descendant dest: next_childD next_sib_set_same_parent) apply(drule(2) next_not_childD) apply(erule disjE, rule disjI2, rule disjI1) apply(fastforce simp: next_sib_set_def intro: trancl_into_trancl) apply(intro disjI2, elim exE conjE) apply(rule_tac x=q in exI) apply(fastforce simp: next_sib_set_def intro: trancl_into_trancl) apply(simp add: next_slot_def split: if_split_asm) apply(erule disjE) apply(rule disjI2)+ apply(rule_tac x=p in exI) apply(rule conjI) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule(1) next_childD) apply(drule_tac x=p in tranclD2) apply(elim exE conjE, simp) apply(fastforce dest: rtranclD) apply(fastforce) apply(rule disjI1) apply(frule(1) next_sib_set_same_parent) apply(drule(1) next_childD) apply(fastforce simp: descendants_of_def cdt_parent_defs intro: trancl_into_trancl2) apply(drule(2) next_not_childD) apply(rule disjI2)+ apply(case_tac "next_sib c t m = Some b") apply(erule disjE) apply(simp) apply(rule_tac x=p in exI) apply(fastforce dest: next_sib_share_parent) apply(rule_tac x=c in exI) apply(simp) apply(rule_tac x=q in exI) apply(fastforce simp: next_sib_set_def intro: trancl_into_trancl) apply(simp | elim conjE exE)+ apply(erule disjE) apply(rule_tac x=p in exI) apply(rule conjI) apply(rule disjI1) apply(drule_tac c=p in next_sib_share_parent, simp) apply(rule_tac b=qa in descendants_trans, simp, simp) apply(fastforce) apply(fastforce simp: next_sib_set_def intro: trancl_into_trancl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> next_slot_set slot t m; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> next \<in> descendants_of slot m \<or> next \<in> next_sib_set slot t m \<or> (\<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> {next. (next, slot) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> next \<in> descendants_of slot m \<or> next \<in> next_sib_set slot t m \<or> (\<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(next, slot) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> next \<in> descendants_of slot m \<or> next \<in> next_sib_set slot t m \<or> (\<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (next = q \<or> next \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); (b, c) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>next_slot b t m = Some a; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); (b, c) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; t b \<noteq> []; next_child b t = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; t b = []; next_not_child b t m = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); (b, c) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); no_mloop m; finite_depth m; t b \<noteq> []; (case t b of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = Some a\<rbrakk> \<Longrightarrow> (b, a) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. ((p, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+)))
 2. \<And>a b. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; t b = []; next_not_child b t m = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); (b, c) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; t b = []; next_not_child b t m = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); (b, c) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; t b = []; next_sib b t m = Some a \<or> next_sib b t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> b \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> b \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); (b, c) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; t b = []; next_sib b t m = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; t b = []; next_sib b t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> b \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> b \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); (b, c) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; t b = []; next_sib b t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> b \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> b \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); (b, c) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); (b, c) \<in> {(next, p). next_slot p t m = Some next}; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<in> descendants_of b m \<or> a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))); next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m
 2. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of b m
 2. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b\<rbrakk> \<Longrightarrow> b \<in> descendants_of c m
 3. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 4. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b\<rbrakk> \<Longrightarrow> b \<in> descendants_of c m
 2. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> descendants_of b m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m \<or> (\<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m
 2. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> next_sib_set c t m
 2. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib q t m = Some b; c \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; a \<in> next_sib_set b t m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib q t m = Some b; c \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> (c \<in> descendants_of q m \<or> q = c) \<and> (\<exists>qa. qa \<in> next_sib_set q t m \<and> (a = qa \<or> a \<in> descendants_of qa m))
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some b; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p. (b \<in> descendants_of p m \<or> p = b) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (4 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> c \<in> descendants_of p m \<or> p = c
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 4. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (4 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; (p, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (p, c) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> p = c
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 4. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (4 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; (p, b) \<in> {(p, c). m c = Some p}\<^sup>+; (\<exists>xs. t c = b # xs) \<and> m b = Some c\<rbrakk> \<Longrightarrow> (p, c) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> p = c
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 4. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (4 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; (\<exists>xs. t c = b # xs) \<and> m b = Some c; \<exists>z. (p, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, b) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (p, c) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> p = c
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 4. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (4 subgoals):
 1. \<And>a b c p q z xs. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; m b = Some z; t z = b # xs; (p, z) \<in> {(p, c). m c = Some p}\<^sup>*; c = z\<rbrakk> \<Longrightarrow> (p, z) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> p = z
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 4. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; next_child c t = Some b; p = b; \<exists>pa. m p = Some pa \<and> m q = Some pa\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c \<noteq> []; p = b; \<exists>pa. m p = Some pa \<and> m q = Some pa; (\<exists>xs. t c = b # xs) \<and> m b = Some c\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_not_child c t m = Some b\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m \<or> a \<in> next_sib_set c t m \<or> (\<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m = Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m \<noteq> Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m = Some b; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m \<noteq> Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m = Some b; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m \<noteq> Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m = Some b; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 3. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m \<noteq> Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m = Some b; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m \<noteq> Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m = Some b; p = b\<rbrakk> \<Longrightarrow> (c \<in> descendants_of c m \<or> c = c) \<and> (\<exists>q. q \<in> next_sib_set c t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m \<noteq> Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set b t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b; p = b\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set c t m \<and> (a = q \<or> a \<in> descendants_of q m)
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m \<noteq> Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set b t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b; p = b\<rbrakk> \<Longrightarrow> q \<in> next_sib_set c t m \<and> (a = q \<or> a \<in> descendants_of q m)
 2. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m \<noteq> Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (1 subgoal):
 1. \<And>a b c p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = Some b \<or> next_sib c t m = None \<and> (\<exists>q. next_sib q t m = Some b \<and> c \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); next_sib c t m \<noteq> Some b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (1 subgoal):
 1. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; b \<in> descendants_of p m \<or> p = b; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m))
 2. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> c \<in> descendants_of p m \<or> p = c
 2. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 3. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> c \<in> descendants_of p m
 2. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 3. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (3 subgoals):
 1. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; b \<in> descendants_of p m; (qa \<in> descendants_of p m) = (b \<in> descendants_of p m)\<rbrakk> \<Longrightarrow> c \<in> descendants_of p m
 2. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 3. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (2 subgoals):
 1. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; b \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)
 2. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal (1 subgoal):
 1. \<And>a b c p q qa. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set p t m; a = q \<or> a \<in> descendants_of q m; (a, b) \<in> {(next, p). (t p = [] \<or> next_child p t = Some next) \<and> (t p = [] \<longrightarrow> next_not_child p t m = Some next)}\<^sup>+; t c = []; next_sib c t m = None; next_sib qa t m = Some b; c \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> c \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; p = b\<rbrakk> \<Longrightarrow> \<exists>p. (c \<in> descendants_of p m \<or> p = c) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (a = q \<or> a \<in> descendants_of q m)) proof (prove)
goal:
No subgoals!