theory Deterministic_AI

lemma next_sib_in_next_slot_set:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s\<rbrakk>
    \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)" apply(subgoal_tac "finite (descendants_of slot (cdt s))") prefer 2 apply(rule finite_subset[OF _ cte_wp_at_set_finite[where P="\<top>\<top>" and s=s]]) apply(fastforce simp: descendants_of_cte_at) apply(frule finite_depth) apply(subgoal_tac "no_mloop (cdt s)") prefer 2 apply(simp add: valid_mdb_def) apply(case_tac "descendants_of slot (cdt s) = {}") apply(fastforce simp: next_slot_set_def next_slot_def empty_list_empty_desc next_not_child_termination) apply(case_tac "last_last_child slot (cdt_list s)") apply(drule(2) last_last_child_NoneD, simp) apply(case_tac "a \<in> next_slot_set slot (cdt_list s) (cdt s)") apply(frule(2) last_last_child_empty_desc) apply(drule(2) last_last_child_next_not_child) apply(simp add: next_slot_set_def) apply(rule_tac b=a in trancl_into_trancl2) apply(simp add: next_slot_def empty_list_empty_desc next_not_child_termination) apply(simp) apply(subgoal_tac "next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)") prefer 2 apply(rule subsetI) apply(simp add: next_slot_set_def) apply(drule trancl_Collect_rev) apply(erule trancl_induct) apply(simp add: empty_list_empty_desc next_slot_def) apply(drule(1) next_childD, simp add: child_descendant) apply(simp) apply(drule(2) desc_next_slot_desc_or_sib) apply(erule disjE, simp) apply(drule_tac b=y in trancl_Collect_rev) apply(simp) apply(subgoal_tac "(\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` (next_slot_set slot (cdt_list s) (cdt s)) \<subset> next_slot_set slot (cdt_list s) (cdt s)") prefer 2 apply(simp add: image_def) apply(rule psubsetI) apply(rule subsetI) apply(simp) apply(erule bexE) apply(simp add: next_slot_set_def) apply(case_tac "next_slot xa (cdt_list s) (cdt s)") apply(drule_tac c=xa in subsetD) apply(simp) apply(drule(2) desc_next_slot_desc_or_sib, simp) apply(drule trancl_Collect_rev) apply(drule_tac c=x in trancl_into_trancl) apply(case_tac "next_slot xa (cdt_list s) (cdt s)") apply(simp) apply(simp add: the_def) apply(simp) apply(drule trancl_Collect_rev, simp) apply(case_tac "next_slot slot (cdt_list s) (cdt s)") apply(fastforce simp: next_slot_def empty_list_empty_desc next_child_def split: if_split_asm list.splits) apply(rule_tac x=aa in set_neqI[symmetric]) apply(fastforce simp: next_slot_set_def) apply(rule ccontr, simp) apply(erule bexE) apply(simp) apply(subgoal_tac "\<exists>y. next_slot x (cdt_list s) (cdt s) = Some y") prefer 2 apply(rule ccontr) apply(simp) apply(drule_tac c=x in subsetD) apply(simp) apply(drule(2) desc_next_slot_desc_or_sib, simp) apply(erule exE, simp) apply(frule_tac x=y in next_slot_no_loop, assumption+) apply(erule notE)+ apply(simp add: next_slot_set_def) apply(drule tranclD2, simp) apply(drule rtranclD) apply(erule disjE, fastforce) apply(rule_tac b=x in trancl_into_trancl2) apply(simp) apply(simp) apply(frule finite_subset) apply(simp add: finite_descendants) apply(frule(1) psubset_card_mono) apply(drule_tac f="(\<lambda>p. the (next_slot p (cdt_list s) (cdt s)))" and A="next_slot_set slot (cdt_list s) (cdt s)" in inj_on_iff_eq_card) apply(erule iffE) apply(erule impE) apply(simp) apply(rule inj_onI) apply(frule_tac c=x in subsetD, simp) apply(frule_tac c=y in subsetD, simp) apply(case_tac "next_slot x (cdt_list s) (cdt s)") apply(drule(2) desc_next_slot_desc_or_sib)+ apply(simp) apply(case_tac "next_slot y (cdt_list s) (cdt s)") apply(drule(2) desc_next_slot_desc_or_sib)+ apply(simp) apply(simp) apply(rule ccontr) apply(drule(2) next_slot_linear) apply(erule disjE) apply(drule_tac x=x in next_slot_no_loop, assumption+) apply(simp add: next_slot_set_def) apply(drule_tac x=x in tranclD2, simp) apply(drule_tac x=x and z=x in rtrancl_trancl_trancl) apply(rule r_into_trancl, simp+) apply(drule_tac x=y in next_slot_no_loop, assumption+) apply(simp add: next_slot_set_def) apply(drule_tac x=y and y=x in tranclD2, simp) apply(drule_tac x=y and z=y in rtrancl_trancl_trancl) apply(rule r_into_trancl, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> finite (descendants_of slot (cdt s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> finite (descendants_of slot (cdt s))
 2. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) \<subseteq> {p. cte_wp_at (\<lambda>_. True) p s}
 2. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s)\<rbrakk> \<Longrightarrow> no_mloop (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s)\<rbrakk> \<Longrightarrow> no_mloop (cdt s)
 2. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) = {}\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = None\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<in> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<in> next_slot_set slot (cdt_list s) (cdt s); descendants_of a (cdt s) = {}\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; a \<in> next_slot_set slot (cdt_list s) (cdt s); descendants_of a (cdt s) = {}; next_not_child a (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; (a, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; descendants_of a (cdt s) = {}; next_not_child a (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; (a, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; descendants_of a (cdt s) = {}; next_not_child a (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> (next, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; (a, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; descendants_of a (cdt s) = {}; next_not_child a (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; (a, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; descendants_of a (cdt s) = {}; next_not_child a (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); x \<in> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> x \<in> descendants_of slot (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (x, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> descendants_of slot (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (slot, x) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> descendants_of slot (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (slot, y) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<rbrakk> \<Longrightarrow> y \<in> descendants_of slot (cdt s)
 2. \<And>a x y z. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (slot, y) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}; y \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> z \<in> descendants_of slot (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). (if descendants_of p (cdt s) \<noteq> {} then next_child p (cdt_list s) else next_not_child p (cdt_list s) (cdt s)) = Some next}\<^sup>+; next_child slot (cdt_list s) = Some y\<rbrakk> \<Longrightarrow> y \<in> descendants_of slot (cdt s)
 2. \<And>a x y z. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (slot, y) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}; y \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> z \<in> descendants_of slot (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y z. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (slot, y) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}; y \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> z \<in> descendants_of slot (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a y z. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (slot, y) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+; next_slot y (cdt_list s) (cdt s) = Some z; y \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> z \<in> descendants_of slot (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a y z. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (slot, y) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+; next_slot y (cdt_list s) (cdt s) = Some z; (\<exists>q. next_slot y (cdt_list s) (cdt s) = Some q \<and> q \<in> descendants_of slot (cdt s)) \<or> last_last_child slot (cdt_list s) = Some y \<and> next_not_child y (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> z \<in> descendants_of slot (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a y z. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (slot, y) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+; next_slot y (cdt_list s) (cdt s) = Some z; last_last_child slot (cdt_list s) = Some y \<and> next_not_child y (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> z \<in> descendants_of slot (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a y z. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_slot y (cdt_list s) (cdt s) = Some z; last_last_child slot (cdt_list s) = Some y \<and> next_not_child y (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s); (y, slot) \<in> {(x, y). next_slot y (cdt_list s) (cdt s) = Some x}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> descendants_of slot (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<subset> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<subseteq> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); x \<in> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))}\<rbrakk> \<Longrightarrow> x \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); \<exists>xa\<in>next_slot_set slot (cdt_list s) (cdt s). x = the (next_slot xa (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> x \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x xa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); xa \<in> next_slot_set slot (cdt_list s) (cdt s); x = the (next_slot xa (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> x \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x xa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (xa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; x = the (next_slot xa (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a x xa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (xa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (xa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 4. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>a x xa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (xa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> xa \<in> {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}
 2. \<And>a x xa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (xa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = None; xa \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 3. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (xa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 4. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 5. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a x xa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (xa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = None; xa \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (xa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 4. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (xa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa; (slot, xa) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}
 2. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa; (slot, x) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 4. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa; next_slot xa (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}
 2. \<And>a x xa aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa; next_slot xa (cdt_list s) (cdt s) = Some ab\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}
 3. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa; (slot, x) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 4. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 5. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a x xa aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa; next_slot xa (cdt_list s) (cdt s) = Some ab\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}
 2. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa; (slot, x) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 4. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = the (next_slot xa (cdt_list s) (cdt s)); next_slot xa (cdt_list s) (cdt s) = Some aa; (slot, x) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (the (next_slot xa (cdt_list s) (cdt s)), slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x xa aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); x = aa; next_slot xa (cdt_list s) (cdt s) = Some aa; (slot, aa) \<in> {(next, p). next_slot next (cdt_list s) (cdt s) = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))} \<noteq> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> aa \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> aa \<notin> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))}
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> aa \<notin> {y. \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). y = the (next_slot x (cdt_list s) (cdt s))}
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some aa; \<exists>x\<in>next_slot_set slot (cdt_list s) (cdt s). aa = the (next_slot x (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some aa; x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s)); \<exists>y. next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> \<exists>y. next_slot x (cdt_list s) (cdt s) = Some y
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> \<exists>y. next_slot x (cdt_list s) (cdt s) = Some y
 2. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s)); \<exists>y. next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s)); \<nexists>y. next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s)); \<exists>y. next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the None); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the None; next_slot x (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s)); \<exists>y. next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the None); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the None; next_slot x (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> x \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the None); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the None; next_slot x (cdt_list s) (cdt s) = None; x \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s)); \<exists>y. next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> False
 4. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the None); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the None; next_slot x (cdt_list s) (cdt s) = None; x \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s)); \<exists>y. next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some (the (next_slot x (cdt_list s) (cdt s))); x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = the (next_slot x (cdt_list s) (cdt s)); \<exists>y. next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = y; next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = y; next_slot x (cdt_list s) (cdt s) = Some y; y \<notin> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); last_last_child slot (cdt_list s) = Some a; next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; x \<in> next_slot_set slot (cdt_list s) (cdt s); aa = y; next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> y \<in> next_slot_set y (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); last_last_child slot (cdt_list s) = Some a; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; (x, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; aa = y; next_slot x (cdt_list s) (cdt s) = Some y\<rbrakk> \<Longrightarrow> (y, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); last_last_child slot (cdt_list s) = Some a; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; aa = y; next_slot x (cdt_list s) (cdt s) = Some y; (x, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>*\<rbrakk> \<Longrightarrow> (y, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); last_last_child slot (cdt_list s) = Some a; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; aa = y; next_slot x (cdt_list s) (cdt s) = Some y; x = y \<or> x \<noteq> y \<and> (x, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (y, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); last_last_child slot (cdt_list s) = Some a; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; aa = y; next_slot x (cdt_list s) (cdt s) = Some y; x \<noteq> y \<and> (x, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (y, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); last_last_child slot (cdt_list s) = Some a; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; aa = y; next_slot x (cdt_list s) (cdt s) = Some y; x \<noteq> y \<and> (x, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (y, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}
 2. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); last_last_child slot (cdt_list s) = Some a; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; aa = y; next_slot x (cdt_list s) (cdt s) = Some y; x \<noteq> y \<and> (x, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (x, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); last_last_child slot (cdt_list s) = Some a; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); next_slot slot (cdt_list s) (cdt s) = Some y; aa = y; next_slot x (cdt_list s) (cdt s) = Some y; x \<noteq> y \<and> (x, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (x, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> finite (descendants_of slot (cdt s))
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); finite (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); finite (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); finite (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)) = (card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s))
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s))
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a x y aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> x = y
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); next_slot x (cdt_list s) (cdt s) = None; (\<exists>q. next_slot x (cdt_list s) (cdt s) = Some q \<and> q \<in> descendants_of slot (cdt s)) \<or> last_last_child slot (cdt_list s) = Some x \<and> next_not_child x (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s); (\<exists>q. next_slot y (cdt_list s) (cdt s) = Some q \<and> q \<in> descendants_of slot (cdt s)) \<or> last_last_child slot (cdt_list s) = Some y \<and> next_not_child y (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a x y aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> x = y
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some aa; next_slot y (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some aa; next_slot y (cdt_list s) (cdt s) = Some ab\<rbrakk> \<Longrightarrow> x = y
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y aa. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); next_slot x (cdt_list s) (cdt s) = Some aa; next_slot y (cdt_list s) (cdt s) = None; (\<exists>q. next_slot x (cdt_list s) (cdt s) = Some q \<and> q \<in> descendants_of slot (cdt s)) \<or> last_last_child slot (cdt_list s) = Some x \<and> next_not_child x (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s); (\<exists>q. next_slot y (cdt_list s) (cdt s) = Some q \<and> q \<in> descendants_of slot (cdt s)) \<or> last_last_child slot (cdt_list s) = Some y \<and> next_not_child y (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some aa; next_slot y (cdt_list s) (cdt s) = Some ab\<rbrakk> \<Longrightarrow> x = y
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); the (next_slot x (cdt_list s) (cdt s)) = the (next_slot y (cdt_list s) (cdt s)); x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some aa; next_slot y (cdt_list s) (cdt s) = Some ab\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); x \<in> next_slot_set slot (cdt_list s) (cdt s); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; x \<in> next_slot_set y (cdt_list s) (cdt s) \<or> y \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; x \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; y \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; x \<in> next_slot_set y (cdt_list s) (cdt s); x \<notin> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; y \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subset> {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; card ((\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}) < card {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; (y, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; (x, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (x, x) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; y \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subset> {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; card ((\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}) < card {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; (y, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; (x, x) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (x, ab) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>*\<rbrakk> \<Longrightarrow> False
 2. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; y \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subset> {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; card ((\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}) < card {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; (y, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; (x, x) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (ab, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subset> {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; card ((\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}) < card {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; (y, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; (x, x) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (x, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> False
 3. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; y \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 4. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; y \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); y \<in> next_slot_set slot (cdt_list s) (cdt s); aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; y \<in> next_slot_set x (cdt_list s) (cdt s); y \<notin> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subset> {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; card ((\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}) < card {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; (y, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; (y, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (y, y) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subset> {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; card ((\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}) < card {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; (y, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; (y, y) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (y, ab) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>*\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subset> {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; card ((\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}) < card {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; (y, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; (y, y) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (ab, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a x y aa ab. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; (a, slot) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subseteq> descendants_of slot (cdt s); (\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+} \<subset> {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; card ((\<lambda>x. the (next_slot x (cdt_list s) (cdt s))) ` {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}) < card {next. (next, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}; (y, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; aa = ab; x \<in> descendants_of slot (cdt s); y \<in> descendants_of slot (cdt s); next_slot x (cdt_list s) (cdt s) = Some ab; next_slot y (cdt_list s) (cdt s) = Some ab; x \<noteq> y; (y, y) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (y, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some next; valid_list s; valid_mdb s; finite (descendants_of slot (cdt s)); finite_depth (cdt s); no_mloop (cdt s); descendants_of slot (cdt s) \<noteq> {}; last_last_child slot (cdt_list s) = Some a; a \<notin> next_slot_set slot (cdt_list s) (cdt s); next_slot_set slot (cdt_list s) (cdt s) \<subseteq> descendants_of slot (cdt s); (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s) \<subset> next_slot_set slot (cdt_list s) (cdt s); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) < card (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s)) \<longrightarrow> inj_on (\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) (next_slot_set slot (cdt_list s) (cdt s)); card ((\<lambda>p. the (next_slot p (cdt_list s) (cdt s))) ` next_slot_set slot (cdt_list s) (cdt s)) = card (next_slot_set slot (cdt_list s) (cdt s))\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal:
No subgoals!