theory Deterministic_AI

lemma next_slot_set_in_desc:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p;
    slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a;
    valid_list s; valid_mdb s\<rbrakk>
    \<Longrightarrow> a \<in> descendants_of p (cdt s)" apply(frule finite_depth) apply(subgoal_tac "no_mloop (cdt s)") prefer 2 apply(simp add: valid_mdb_def) apply(frule(1) next_slot_setD) apply(simp add: valid_mdb_def, simp+) apply(elim disjE) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule_tac x=slot in tranclD2) apply(simp) apply(drule(1) rtrancl_trancl_trancl) apply(simp add: no_mloop_def cdt_parent_defs) apply(frule(1) next_sib_set_same_parent) apply(simp add: next_slot_def split: if_split_asm) apply(drule(1) next_childD) apply(simp add: descendants_of_def cdt_parent_defs) apply(rule_tac b=slot in r_r_into_trancl) apply(simp) apply(simp) apply(simp add: next_not_child_termination) apply(simp split: if_split_asm option.splits) apply(fastforce dest: tranclD2 simp: next_sib_set_def)+ apply(drule(1) next_sib_same_parent, simp add: child_descendant) apply(elim exE conjE) apply(subgoal_tac "q = next") prefer 2 apply(subgoal_tac "pa \<in> descendants_of p (cdt s)") prefer 2 apply(erule disjE) apply(frule_tac b=p and c=pa in descendants_linear, simp) apply(frule(1) next_sib_set_same_parent) apply(elim exE conjE) apply(rule notI, simp) apply(erule disjE) apply(simp add: no_mloop_weaken) apply(frule_tac a="next" and c=pa in descendants_linear) apply(simp add: child_descendant) apply(fastforce simp: next_sib_set_not_self) apply(simp add: sib_not_desc) apply(frule(1) next_sib_set_same_parent) apply(erule disjE)+ apply(simp add: child_descendant) apply(simp) apply(erule disjE) apply(frule_tac a=p and c=q in descendants_linear) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule_tac x=q in tranclD2) apply(simp) apply(drule rtranclD) apply(elim disjE exE conjE) apply(fastforce dest: sib_not_desc[simplified descendants_of_def cdt_parent_defs]) apply(simp) apply(fastforce simp: next_sib_set_not_self) apply(fastforce dest: sib_not_desc) apply(simp) apply(simp) apply(erule_tac P="next = q" in disjE, simp) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule_tac x=q in tranclD2) apply(simp) apply(drule_tac x=q and z=pa in rtrancl_trancl_trancl, simp) apply(fastforce dest: sib_not_desc[simplified descendants_of_def cdt_parent_defs]
               next_sib_set_same_parent) apply(simp) apply(simp add: next_slot_def split: if_split_asm) apply(drule(1) next_childD) apply(rule descendants_trans) apply(rule child_descendant) apply(simp) apply(simp) apply(drule(2) next_not_childD) apply(erule_tac P="next_sib slot (cdt_list s) (cdt s) = Some a" in disjE) apply(simp add: next_sib_share_parent) apply(elim exE conjE) apply(case_tac "qa=pa") apply(fastforce intro: child_descendant dest: next_sib_same_parent next_sib_set_same_parent) apply(erule disjE) apply(frule_tac a=slot and b=pa and c=qa in descendants_linear) apply(simp)+ apply(erule disjE) apply(fastforce simp: next_sib_set_def dest: tranclD2) apply(drule_tac a=qa and c=p in descendants_trans) apply(fastforce dest: next_sib_set_same_parent simp: child_descendant) apply(fastforce dest: next_sib_share_parent) apply(simp) apply(fastforce simp: next_sib_set_def dest: tranclD2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s)\<rbrakk> \<Longrightarrow> no_mloop (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s)\<rbrakk> \<Longrightarrow> no_mloop (cdt s)
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> no_mloop (cdt s)
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> finite_depth (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> descendants_of slot (cdt s) \<or> next \<in> next_sib_set slot (cdt_list s) (cdt s) \<or> (\<exists>p q. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> next \<in> descendants_of q (cdt s) \<union> {q})\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> descendants_of slot (cdt s) \<or> next \<in> next_sib_set slot (cdt_list s) (cdt s) \<or> (\<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s))))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); (slot, next) \<in> {(p, c). cdt s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (p, a) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>z. (slot, z) \<in> {(p, c). cdt s c = Some p}\<^sup>* \<and> (z, next) \<in> {(p, c). cdt s c = Some p}\<rbrakk> \<Longrightarrow> (p, a) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); (slot, p) \<in> {(p, c). cdt s c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> (p, a) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); (slot, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (p, a) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); \<exists>p. cdt s slot = Some p \<and> cdt s next = Some p\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot \<noteq> []; next_child slot (cdt_list s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> (p, a) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> (p, slot) \<in> {(p, c). cdt s c = Some p}
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> (slot, a) \<in> {(p, c). cdt s c = Some p}
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 4. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> (slot, a) \<in> {(p, c). cdt s c = Some p}
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; (if next_sib slot (cdt_list s) (cdt s) = None then if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib slot (cdt_list s) (cdt s)) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (22 subgoals):
 1. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i x2j x2k x2l x2m x2n x2o x2p x2q x2r. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = None; cdt s x2i = Some x2j; next_sib x2j (cdt_list s) (cdt s) = None; cdt s x2j = Some x2k; next_sib x2k (cdt_list s) (cdt s) = None; cdt s x2k = Some x2l; next_sib x2l (cdt_list s) (cdt s) = None; cdt s x2l = Some x2m; next_sib x2m (cdt_list s) (cdt s) = None; cdt s x2m = Some x2n; next_sib x2n (cdt_list s) (cdt s) = None; cdt s x2n = Some x2o; next_sib x2o (cdt_list s) (cdt s) = None; cdt s x2o = Some x2p; next_sib x2p (cdt_list s) (cdt s) = None; cdt s x2p = Some x2q; next_sib x2q (cdt_list s) (cdt s) = None; cdt s x2q = Some x2r; next_not_child x2r (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i x2j x2k x2l x2m x2n x2o x2p x2q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = None; cdt s x2i = Some x2j; next_sib x2j (cdt_list s) (cdt s) = None; cdt s x2j = Some x2k; next_sib x2k (cdt_list s) (cdt s) = None; cdt s x2k = Some x2l; next_sib x2l (cdt_list s) (cdt s) = None; cdt s x2l = Some x2m; next_sib x2m (cdt_list s) (cdt s) = None; cdt s x2m = Some x2n; next_sib x2n (cdt_list s) (cdt s) = None; cdt s x2n = Some x2o; next_sib x2o (cdt_list s) (cdt s) = None; cdt s x2o = Some x2p; next_sib x2p (cdt_list s) (cdt s) = None; cdt s x2p = Some x2q; next_sib x2q (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i x2j x2k x2l x2m x2n x2o x2p. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = None; cdt s x2i = Some x2j; next_sib x2j (cdt_list s) (cdt s) = None; cdt s x2j = Some x2k; next_sib x2k (cdt_list s) (cdt s) = None; cdt s x2k = Some x2l; next_sib x2l (cdt_list s) (cdt s) = None; cdt s x2l = Some x2m; next_sib x2m (cdt_list s) (cdt s) = None; cdt s x2m = Some x2n; next_sib x2n (cdt_list s) (cdt s) = None; cdt s x2n = Some x2o; next_sib x2o (cdt_list s) (cdt s) = None; cdt s x2o = Some x2p; next_sib x2p (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 4. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i x2j x2k x2l x2m x2n x2o. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = None; cdt s x2i = Some x2j; next_sib x2j (cdt_list s) (cdt s) = None; cdt s x2j = Some x2k; next_sib x2k (cdt_list s) (cdt s) = None; cdt s x2k = Some x2l; next_sib x2l (cdt_list s) (cdt s) = None; cdt s x2l = Some x2m; next_sib x2m (cdt_list s) (cdt s) = None; cdt s x2m = Some x2n; next_sib x2n (cdt_list s) (cdt s) = None; cdt s x2n = Some x2o; next_sib x2o (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 5. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i x2j x2k x2l x2m x2n. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = None; cdt s x2i = Some x2j; next_sib x2j (cdt_list s) (cdt s) = None; cdt s x2j = Some x2k; next_sib x2k (cdt_list s) (cdt s) = None; cdt s x2k = Some x2l; next_sib x2l (cdt_list s) (cdt s) = None; cdt s x2l = Some x2m; next_sib x2m (cdt_list s) (cdt s) = None; cdt s x2m = Some x2n; next_sib x2n (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 6. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i x2j x2k x2l x2m. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = None; cdt s x2i = Some x2j; next_sib x2j (cdt_list s) (cdt s) = None; cdt s x2j = Some x2k; next_sib x2k (cdt_list s) (cdt s) = None; cdt s x2k = Some x2l; next_sib x2l (cdt_list s) (cdt s) = None; cdt s x2l = Some x2m; next_sib x2m (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 7. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i x2j x2k x2l. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = None; cdt s x2i = Some x2j; next_sib x2j (cdt_list s) (cdt s) = None; cdt s x2j = Some x2k; next_sib x2k (cdt_list s) (cdt s) = None; cdt s x2k = Some x2l; next_sib x2l (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 8. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i x2j x2k. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = None; cdt s x2i = Some x2j; next_sib x2j (cdt_list s) (cdt s) = None; cdt s x2j = Some x2k; next_sib x2k (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 9. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i x2j. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = None; cdt s x2i = Some x2j; next_sib x2j (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 10. \<And>x2 x2a x2b x2c x2d x2e x2f x2g x2h x2i. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib p (cdt_list s) (cdt s) = None; cdt s p = Some x2; next_sib x2 (cdt_list s) (cdt s) = None; cdt s x2 = Some x2a; next_sib x2a (cdt_list s) (cdt s) = None; cdt s x2a = Some x2b; next_sib x2b (cdt_list s) (cdt s) = None; cdt s x2b = Some x2c; next_sib x2c (cdt_list s) (cdt s) = None; cdt s x2c = Some x2d; next_sib x2d (cdt_list s) (cdt s) = None; cdt s x2d = Some x2e; next_sib x2e (cdt_list s) (cdt s) = None; cdt s x2e = Some x2f; next_sib x2f (cdt_list s) (cdt s) = None; cdt s x2f = Some x2g; next_sib x2g (cdt_list s) (cdt s) = None; cdt s x2g = Some x2h; next_sib x2h (cdt_list s) (cdt s) = None; cdt s x2h = Some x2i; next_sib x2i (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
A total of 22 subgoals... proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); cdt s slot = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> (\<exists>q. q \<in> next_sib_set p (cdt_list s) (cdt s) \<and> (next = q \<or> next \<in> descendants_of q (cdt s)))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> q = next proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> q = next
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> p \<noteq> pa
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p\<rbrakk> \<Longrightarrow> p \<noteq> pa
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa\<rbrakk> \<Longrightarrow> p \<noteq> pa
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa\<rbrakk> \<Longrightarrow> False
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (6 subgoals):
 1. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa; next = q\<rbrakk> \<Longrightarrow> False
 2. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa; next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa; next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (7 subgoals):
 1. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa; next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> next \<in> descendants_of pa (cdt s)
 2. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa; next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> q \<noteq> pa
 3. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa; next \<in> descendants_of q (cdt s); q \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> False
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 7. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (6 subgoals):
 1. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa; next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> q \<noteq> pa
 2. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa; next \<in> descendants_of q (cdt s); q \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some pa; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); cdt s pa = Some paa; cdt s q = Some paa; p = pa; next \<in> descendants_of q (cdt s); q \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (6 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next = q; p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next = q; pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next = q; pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); p \<in> descendants_of pa (cdt s) \<or> pa \<in> descendants_of p (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (7 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> p \<in> descendants_of q (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<noteq> q
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s); pa \<in> descendants_of q (cdt s) \<or> q \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 7. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (7 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; (q, next) \<in> {(p, c). cdt s c = Some p}\<^sup>+; (pa, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<noteq> q
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s); pa \<in> descendants_of q (cdt s) \<or> q \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 7. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (7 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; (pa, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+; \<exists>z. (q, z) \<in> {(p, c). cdt s c = Some p}\<^sup>* \<and> (z, next) \<in> {(p, c). cdt s c = Some p}\<rbrakk> \<Longrightarrow> (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<noteq> q
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s); pa \<in> descendants_of q (cdt s) \<or> q \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 7. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (7 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; (pa, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+; (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<noteq> q
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s); pa \<in> descendants_of q (cdt s) \<or> q \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 7. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (7 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; (pa, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+; q = p \<or> q \<noteq> p \<and> (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<noteq> q
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s); pa \<in> descendants_of q (cdt s) \<or> q \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 7. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (8 subgoals):
 1. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; (pa, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+; q = p; cdt s pa = Some paa; cdt s q = Some paa\<rbrakk> \<Longrightarrow> (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; (pa, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+; q \<noteq> p; (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+; cdt s pa = Some paa; cdt s q = Some paa\<rbrakk> \<Longrightarrow> (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<noteq> q
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s); pa \<in> descendants_of q (cdt s) \<or> q \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 7. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 8. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (7 subgoals):
 1. \<And>pa q paa. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; (pa, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+; q \<noteq> p; (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+; cdt s pa = Some paa; cdt s q = Some paa\<rbrakk> \<Longrightarrow> (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<noteq> q
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s); pa \<in> descendants_of q (cdt s) \<or> q \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 7. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (6 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<noteq> q
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s); pa \<in> descendants_of q (cdt s) \<or> q \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 6. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); p \<in> descendants_of pa (cdt s); pa \<in> descendants_of q (cdt s) \<or> q \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 5. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); slot \<in> descendants_of pa (cdt s); \<exists>p. cdt s pa = Some p \<and> cdt s q = Some p; next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 4. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa = slot\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 3. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); pa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> q = next
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); pa \<in> descendants_of p (cdt s); next \<in> descendants_of q (cdt s)\<rbrakk> \<Longrightarrow> q = next
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); (p, pa) \<in> {(p, c). cdt s c = Some p}\<^sup>+; (q, next) \<in> {(p, c). cdt s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> q = next
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); (p, pa) \<in> {(p, c). cdt s c = Some p}\<^sup>+; \<exists>z. (q, z) \<in> {(p, c). cdt s c = Some p}\<^sup>* \<and> (z, next) \<in> {(p, c). cdt s c = Some p}\<rbrakk> \<Longrightarrow> q = next
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); (p, pa) \<in> {(p, c). cdt s c = Some p}\<^sup>+; (q, p) \<in> {(p, c). cdt s c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> q = next
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (p, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+; next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); (pa, slot) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); (p, pa) \<in> {(p, c). cdt s c = Some p}\<^sup>+; (q, pa) \<in> {(p, c). cdt s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> q = next
 2. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; q \<in> next_sib_set pa (cdt_list s) (cdt s); next = q \<or> next \<in> descendants_of q (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q. \<lbrakk>next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot \<noteq> []; next_child slot (cdt_list s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of (?b792 pa q) (cdt s)
 2. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> ?b792 pa q \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> cdt s a = Some (?b792 pa q)
 2. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> ?b792 pa q \<in> descendants_of p (cdt s)
 3. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot \<noteq> []; (\<exists>xs. cdt_list s slot = a # xs) \<and> cdt s a = Some slot\<rbrakk> \<Longrightarrow> slot \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_not_child slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = Some a \<or> next_sib slot (cdt_list s) (cdt s) = None \<and> (\<exists>q. next_sib q (cdt_list s) (cdt s) = Some a \<and> slot \<in> descendants_of q (cdt s) \<and> (\<forall>q'. q' \<in> descendants_of q (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None \<and> (\<exists>q. next_sib q (cdt_list s) (cdt s) = Some a \<and> slot \<in> descendants_of q (cdt s) \<and> (\<forall>q'. q' \<in> descendants_of q (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None \<and> (\<exists>q. next_sib q (cdt_list s) (cdt s) = Some a \<and> slot \<in> descendants_of q (cdt s) \<and> (\<forall>q'. q' \<in> descendants_of q (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None))\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa = pa\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); slot \<in> descendants_of pa (cdt s) \<or> pa = slot; next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; pa = slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> slot \<in> descendants_of qa (cdt s)
 2. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<noteq> qa
 3. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s); pa \<in> descendants_of qa (cdt s) \<or> qa \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 4. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; pa = slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s); pa \<in> descendants_of qa (cdt s) \<or> qa \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; pa = slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s); pa \<in> descendants_of qa (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s); qa \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; pa = slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s); qa \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; pa = slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s)\<rbrakk> \<Longrightarrow> pa \<in> descendants_of p (cdt s)
 2. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s); qa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; pa = slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; slot \<in> descendants_of pa (cdt s); qa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; pa = slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set pa (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> pa; pa = slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>pa q qa. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_sib_set slot (cdt_list s) (cdt s); q = next; next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; slot \<in> descendants_of p (cdt s); cdt_list s slot = []; next_sib slot (cdt_list s) (cdt s) = None; next_sib qa (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of qa (cdt s); \<forall>q'. q' \<in> descendants_of qa (cdt s) \<and> slot \<in> descendants_of q' (cdt s) \<longrightarrow> next_sib q' (cdt_list s) (cdt s) = None; qa \<noteq> slot; pa = slot\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s) proof (prove)
goal:
No subgoals!