theory Deterministic_AI

lemma next_sib_2_NoneD:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  assumes "next_sib_2 slot p s = None" "slot \<in> descendants_of p (cdt s)" "valid_mdb s"
     "valid_list s" "q \<in> next_slot_set slot (cdt_list s) (cdt s)"
  shows "cdt s q \<noteq> Some p" apply(insert assms) apply(rule notI) apply(case_tac "next_slot slot (cdt_list s) (cdt s)") apply(fastforce simp: next_slot_set_def dest: tranclD2) apply(frule(5) next_slot_set_in_desc) apply(erule notE[rotated]) apply(simp) apply(induct slot rule: next_sib_2_pinduct[where s=s and p=p]) apply(simp) apply(atomize) apply(simp) apply(elim impCE) apply(fastforce simp: next_sib_2_termination) apply(simp add: next_slot_set_def) apply(drule tranclD2, simp) apply(drule rtranclD) apply(fastforce simp: next_sib_2_termination) apply(case_tac "next_slot a (cdt_list s) (cdt s)") apply(simp add: next_slot_set_def) apply(drule tranclD2, simp) apply(drule rtranclD) apply(erule disjE) apply(fastforce simp: next_sib_2_termination) apply(fastforce dest: tranclD2) apply(case_tac "q=a") apply(fastforce simp: next_sib_2_termination) apply(subgoal_tac "q \<in> next_slot_set a (cdt_list s) (cdt s)") prefer 2 apply(simp add: next_slot_set_def) apply(drule tranclD2, simp) apply(drule rtranclD) apply(fastforce simp: next_sib_2_termination) apply(frule_tac slot=a in next_slot_set_in_desc)  (* rename *)
          apply(simp_all) apply(simp) apply(erule exE) apply(case_tac "cdt s a = Some p") apply(fastforce simp: next_sib_2_termination) apply(rule_tac x=y in exI) apply(fastforce simp: next_sib_2_termination) apply(simp_all add: assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt s q \<noteq> Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = None; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> cdt s q \<noteq> Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = None; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = None; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>next_sib_2 slot p s = None; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib_2 slot p s = None; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>next_sib_2 slot p s = None; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> next_sib_2 slot p s \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<And>a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p; a \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set a (cdt_list s) (cdt s); cdt s q = Some p; next_slot a (cdt_list s) (cdt s) = Some aa; aa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 a p s = Some y; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<And>aa ab. \<lbrakk>a = aa; cdt s aa \<noteq> Some p; aa \<in> descendants_of p (cdt s); q \<in> next_slot_set aa (cdt_list s) (cdt s); next_slot aa (cdt_list s) (cdt s) = Some ab; ab \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 aa p s = Some y; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>aa ab. a = aa \<longrightarrow> cdt s aa \<noteq> Some p \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> q \<in> next_slot_set aa (cdt_list s) (cdt s) \<longrightarrow> next_slot aa (cdt_list s) (cdt s) = Some ab \<longrightarrow> ab \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 aa p s = Some y); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s a \<noteq> Some p \<longrightarrow> q \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y)); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<not> cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); q \<notin> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); q \<notin> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; (q, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); (q, a) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); (q, a) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); (q, a) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; q = a \<or> q \<noteq> a \<and> (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; (q, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = None; (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = None; q = a \<or> q \<noteq> a \<and> (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = None; q = a\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = None; q \<noteq> a \<and> (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = None; q \<noteq> a \<and> (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q = a\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a\<rbrakk> \<Longrightarrow> q \<in> next_slot_set a (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a\<rbrakk> \<Longrightarrow> q \<in> next_slot_set a (cdt_list s) (cdt s)
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; (q, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a\<rbrakk> \<Longrightarrow> (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>*\<rbrakk> \<Longrightarrow> (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q = a \<or> q \<noteq> a \<and> (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (q, a) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (8 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> cdt s q = Some (?p137 slot a aa)
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of (?p137 slot a aa) (cdt s)
 3. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_slot a (cdt_list s) (cdt s) = Some (?a137 slot a aa)
 4. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> valid_list s
 5. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> valid_mdb s
 6. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s); ?a137 slot a aa \<in> descendants_of (?p137 slot a aa) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 7. valid_mdb s
 8. valid_list s proof (prove)
goal (8 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> cdt s q = Some (?p137 slot a aa)
 2. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> a \<in> descendants_of (?p137 slot a aa) (cdt s)
 3. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_slot a (cdt_list s) (cdt s) = Some (?a137 slot a aa)
 4. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> valid_list s
 5. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> valid_mdb s
 6. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<forall>aa. next_slot a (cdt_list s) (cdt s) = Some aa \<longrightarrow> aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s); ?a137 slot a aa \<in> descendants_of (?p137 slot a aa) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 7. valid_mdb s
 8. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); aa \<in> descendants_of p (cdt s) \<longrightarrow> (\<exists>y. next_sib_2 a p s = Some y); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s); aa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a aa. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); \<exists>y. next_sib_2 a p s = Some y; next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s); aa \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a aa y. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s); aa \<in> descendants_of p (cdt s); next_sib_2 a p s = Some y\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a aa y. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s); aa \<in> descendants_of p (cdt s); next_sib_2 a p s = Some y; cdt s a = Some p\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. \<And>slot a aa y. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s); aa \<in> descendants_of p (cdt s); next_sib_2 a p s = Some y; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a aa y. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s); aa \<in> descendants_of p (cdt s); next_sib_2 a p s = Some y; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> \<exists>y. next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a aa y. \<lbrakk>slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; q \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s q = Some p; next_slot slot (cdt_list s) (cdt s) = Some a; a \<in> descendants_of p (cdt s); next_slot a (cdt_list s) (cdt s) = Some aa; q \<noteq> a; q \<in> next_slot_set a (cdt_list s) (cdt s); aa \<in> descendants_of p (cdt s); next_sib_2 a p s = Some y; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some y
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (2 subgoals):
 1. valid_mdb s
 2. valid_list s proof (prove)
goal:
No subgoals!