theory Deterministic_AI

lemma next_sib_2I:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  assumes "cdt s next = Some p" "next \<in> next_slot_set slot (cdt_list s) (cdt s)"
    "\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and>
     next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p"
    "slot \<in> descendants_of p (cdt s)" "valid_mdb s" "valid_list s"
  shows "next_sib_2 slot p s = Some next" using assms apply(induct slot rule: next_sib_2_pinduct[where s=s and p=p]) apply(simp) apply(case_tac "next_slot slot (cdt_list s) (cdt s)") apply(fastforce simp: next_slot_set_def dest: tranclD2) apply(atomize) apply(erule_tac x=a in allE) apply(simp) apply(case_tac "a=next") apply(simp add: next_sib_2_termination) apply(erule impE) apply(rule notI) apply(erule_tac x=a in allE) apply(erule impE) apply(rule conjI) apply(fastforce simp: next_slot_set_def) apply(fastforce dest: rtranclD tranclD2 simp: next_slot_set_def) apply(simp) apply(elim impE) apply(fastforce simp: next_slot_set_def dest: rtranclD tranclD2) apply(intro allI impI notI) apply(erule_tac x=q in allE) apply(erule impE) apply(fastforce intro: trancl_into_trancl simp: next_slot_set_def) apply(simp) apply(drule(5) next_slot_set_in_desc, simp) apply(simp add: next_sib_2_termination) apply(erule_tac x=a in allE, erule impE) apply(rule conjI) apply(fastforce simp: next_slot_set_def) apply(fastforce simp: next_slot_set_def dest: tranclD2 rtranclD) using assms apply(simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_sib_2 slot p s = Some next proof (prove)
using this:
cdt s next = Some p
next \<in> next_slot_set slot (cdt_list s) (cdt s)
\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p
slot \<in> descendants_of p (cdt s)
valid_mdb s
valid_list s

goal (1 subgoal):
 1. next_sib_2 slot p s = Some next proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p; cdt s next = Some p; next \<in> next_slot_set a (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; a \<in> descendants_of p (cdt s); valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> next_sib_2 a p s = Some next; cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p; next \<in> next_slot_set a (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> next_sib_2 a p s = Some next; cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p; next \<in> next_slot_set a (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> next_sib_2 a p s = Some next; cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p; next \<in> next_slot_set a (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> next_sib_2 a p s = Some next; cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p; next \<in> next_slot_set a (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; a \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> next_sib_2 a p s = Some next; cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>a. next_slot slot (cdt_list s) (cdt s) = Some a \<longrightarrow> cdt s a \<noteq> Some p \<longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next; cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; next_slot slot (cdt_list s) (cdt s) = Some a \<longrightarrow> cdt s a \<noteq> Some p \<longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p \<longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p \<longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next; a = next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p \<longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next; a \<noteq> next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p \<longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next; a \<noteq> next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> cdt s a \<noteq> Some p
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p; a \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p\<rbrakk> \<Longrightarrow> a \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set a (cdt_list s) (cdt s)
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> False
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (6 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p\<rbrakk> \<Longrightarrow> a \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p\<rbrakk> \<Longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s)
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> False
 4. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 5. valid_mdb s
 6. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p\<rbrakk> \<Longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s)
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> False
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; cdt s a = Some p; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next \<in> next_slot_set a (cdt_list s) (cdt s) \<longrightarrow> (\<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<longrightarrow> a \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (6 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s)
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> \<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 4. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 5. valid_mdb s
 6. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> \<forall>q. q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>slot a q. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s); cdt s q = Some p\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>slot a q. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s); cdt s q = Some p; q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (6 subgoals):
 1. \<And>slot a q. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s); cdt s q = Some p\<rbrakk> \<Longrightarrow> q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s)
 2. \<And>slot a q. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s); cdt s q = Some p; cdt s q \<noteq> Some p\<rbrakk> \<Longrightarrow> False
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 4. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 5. valid_mdb s
 6. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>slot a q. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; q \<in> next_slot_set a (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s); cdt s q = Some p; cdt s q \<noteq> Some p\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next\<rbrakk> \<Longrightarrow> a \<in> descendants_of p (cdt s)
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; next_sib_2 a p s = Some next\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = Some next
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next\<rbrakk> \<Longrightarrow> cdt s a \<noteq> Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next\<rbrakk> \<Longrightarrow> a \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set a (cdt_list s) (cdt s)
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s a \<noteq> Some p
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next\<rbrakk> \<Longrightarrow> a \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next\<rbrakk> \<Longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s)
 3. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s a \<noteq> Some p
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next\<rbrakk> \<Longrightarrow> next \<in> next_slot_set a (cdt_list s) (cdt s)
 2. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s a \<noteq> Some p
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s a \<noteq> Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
using this:
cdt s next = Some p
next \<in> next_slot_set slot (cdt_list s) (cdt s)
\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> next \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p
slot \<in> descendants_of p (cdt s)
valid_mdb s
valid_list s

goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>cdt s next = Some p; next \<in> next_slot_set slot (cdt_list s) (cdt s); slot \<in> descendants_of p (cdt s); valid_mdb s; valid_list s; next_slot slot (cdt_list s) (cdt s) = Some a; a \<noteq> next; (if a \<in> descendants_of p (cdt s) then case next_slot a (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s a \<noteq> Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
goal:
No subgoals!