theory Deterministic_AI

lemma between_next_sib_2_not_sib:
  notes split_paired_All[simp del] split_paired_Ex[simp del] if_weak_cong[cong]
  assumes
  "next_sib_2 slot p s = Some next" "q \<in> next_slot_set slot (cdt_list s) (cdt s)"
  "next \<in> next_slot_set q (cdt_list s) (cdt s)" "valid_list s" "valid_mdb s"
  shows "cdt s q \<noteq> Some p" using assms apply(subgoal_tac "no_mloop (cdt s)") prefer 2 apply(simp add: valid_mdb_def) apply(frule finite_depth) apply(rule notI) apply(case_tac "next_sib_2 slot p s = Some q") apply(simp add: next_slot_no_loop) apply(subgoal_tac "\<exists>q'. next_sib_2 slot p s = Some q' \<and>
                   q \<in> next_slot_set q' (cdt_list s) (cdt s)") prefer 2 apply(rule_tac P="\<lambda>q'. cdt s q' = Some p \<and>
    q' \<in> next_slot_set slot (cdt_list s) (cdt s) \<and>
    (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and>
    q' \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and>
    q \<in> next_slot_set q' (cdt_list s) (cdt s)" in ex_imp) apply(simp) apply(intro allI impI) apply(elim conjE) apply(drule(2) next_sib_2I) apply(simp add: next_sib_2_termination split: if_split_asm) apply(simp) apply(simp) apply(simp) apply(simp) apply(induct slot rule: next_slot_induct[where s=s]) apply(fastforce simp: next_slot_set_def dest: tranclD2) apply(simp) apply(case_tac "y=next") apply(simp add: next_slot_set_def) apply(drule_tac x=q in tranclD2) apply(simp) apply(drule(1) rtrancl_trancl_trancl) apply(drule(2) next_slot_no_loop[simplified next_slot_set_def, where x=q]) apply(simp) apply(case_tac "y=q") apply(simp add: next_sib_2_termination split: if_split_asm) apply(atomize) apply(elim impE) apply(simp add: next_sib_2_termination split: if_split_asm) apply(fastforce simp: next_slot_set_def dest: rtranclD tranclD2) apply(elim exE conjE) apply(rule_tac x=xa in exI) apply(simp) apply(rule conjI) apply(simp add: next_slot_set_def) apply(rule trancl_into_trancl) apply(simp)+ apply(intro allI impI) apply(erule_tac x=qa in allE) apply(simp) apply(case_tac "qa=y") apply(simp add: next_sib_2_termination split: if_split_asm) apply(simp add: next_slot_set_def) apply(erule conjE) apply(drule_tac x=qa and y=x in tranclD2, simp) apply(drule rtranclD, simp) using assms apply(simp_all add: next_slot_set_def) apply(drule(1) trancl_trans[where y="next"]) apply(fastforce dest: next_slot_no_loop simp: next_slot_set_def) done

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

goal (1 subgoal):
 1. cdt s q \<noteq> Some p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s)\<rbrakk> \<Longrightarrow> cdt s q \<noteq> Some p
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> no_mloop (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> no_mloop (cdt s)
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s)\<rbrakk> \<Longrightarrow> cdt s q \<noteq> Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s)\<rbrakk> \<Longrightarrow> cdt s q \<noteq> Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s)\<rbrakk> \<Longrightarrow> cdt s q \<noteq> Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s = Some q\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<forall>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s) \<longrightarrow> next_sib_2 slot p s = Some x \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 3. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q\<rbrakk> \<Longrightarrow> \<forall>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s) \<longrightarrow> next = x
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 3. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next = x
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 3. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; cdt s x = Some p; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next = x
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 3. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> slot \<in> descendants_of p (cdt s)
 2. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> valid_mdb s
 3. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> valid_list s
 4. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 slot p s = Some x\<rbrakk> \<Longrightarrow> next = x
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 6. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> valid_list s
 3. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 slot p s = Some x\<rbrakk> \<Longrightarrow> next = x
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> valid_list s
 2. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 slot p s = Some x\<rbrakk> \<Longrightarrow> next = x
 3. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; x \<in> next_slot_set slot (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 slot p s = Some x\<rbrakk> \<Longrightarrow> next = x
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 3. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set slot (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)
 2. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>next_slot x (cdt_list s) (cdt s) = None; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y = next\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some next; \<lbrakk>next_sib_2 next p s = Some next; (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> (x, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (x, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib_2 x p s = Some next; (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y = next\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> (xa, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (xa, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some next; \<lbrakk>next_sib_2 next p s = Some next; (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> (x, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (x, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib_2 x p s = Some next; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y = next; \<exists>z. (q, z) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>* \<and> (z, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> (xa, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (xa, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some next; \<lbrakk>next_sib_2 next p s = Some next; (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> (x, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (x, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib_2 x p s = Some next; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y = next; (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> (xa, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (xa, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some next; \<lbrakk>next_sib_2 next p s = Some next; (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> (x, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (x, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib_2 x p s = Some next; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y = next; (q, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> (xa, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (xa, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some next; \<lbrakk>next_sib_2 next p s = Some next; (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> (x, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (x, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib_2 x p s = Some next; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y = next; (q, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; q \<notin> {next. (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> (xa, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (\<forall>q. (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (xa, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p) \<and> (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y = q\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; q \<in> next_slot_set y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 y p s = Some next \<longrightarrow> q \<in> next_slot_set y (cdt_list s) (cdt s) \<longrightarrow> (\<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)); next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q\<rbrakk> \<Longrightarrow> next_sib_2 y p s = Some next
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q\<rbrakk> \<Longrightarrow> q \<in> next_slot_set y (cdt_list s) (cdt s)
 3. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 4. valid_mdb s
 5. valid_list s
 6. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q\<rbrakk> \<Longrightarrow> q \<in> next_slot_set y (cdt_list s) (cdt s)
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; \<exists>x. cdt s x = Some p \<and> x \<in> next_slot_set y (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> x \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set x (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set xa (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>xa. cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set xa (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> cdt s xa = Some p \<and> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p) \<and> q \<in> next_slot_set xa (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set xa (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> xa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> (\<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p)
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set xa (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> xa \<in> next_slot_set x (cdt_list s) (cdt s)
 2. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set xa (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; (xa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; \<forall>q. (q, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (xa, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p; (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set xa (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; (xa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; \<forall>q. (q, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (xa, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p; (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (xa, ?b96 x y xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; (xa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; \<forall>q. (q, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (xa, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s q \<noteq> Some p; (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (?b96 x y xa, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}
 3. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set xa (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p
 4. valid_mdb s
 5. valid_list s
 6. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set xa (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> \<forall>q. q \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa qa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); \<forall>q. q \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set q (cdt_list s) (cdt s) \<longrightarrow> cdt s q \<noteq> Some p; q \<in> next_slot_set xa (cdt_list s) (cdt s); qa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set qa (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> cdt s qa \<noteq> Some p
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa qa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); q \<in> next_slot_set xa (cdt_list s) (cdt s); qa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set qa (cdt_list s) (cdt s); qa \<in> next_slot_set y (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set qa (cdt_list s) (cdt s) \<longrightarrow> cdt s qa \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s qa \<noteq> Some p
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa qa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); q \<in> next_slot_set xa (cdt_list s) (cdt s); qa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set qa (cdt_list s) (cdt s); qa \<in> next_slot_set y (cdt_list s) (cdt s) \<longrightarrow> cdt s qa \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s qa \<noteq> Some p
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y xa qa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); q \<in> next_slot_set xa (cdt_list s) (cdt s); qa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set qa (cdt_list s) (cdt s); qa \<in> next_slot_set y (cdt_list s) (cdt s) \<longrightarrow> cdt s qa \<noteq> Some p; qa = y\<rbrakk> \<Longrightarrow> cdt s qa \<noteq> Some p
 2. \<And>x y xa qa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); q \<in> next_slot_set xa (cdt_list s) (cdt s); qa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set qa (cdt_list s) (cdt s); qa \<in> next_slot_set y (cdt_list s) (cdt s) \<longrightarrow> cdt s qa \<noteq> Some p; qa \<noteq> y\<rbrakk> \<Longrightarrow> cdt s qa \<noteq> Some p
 3. valid_mdb s
 4. valid_list s
 5. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa qa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; q \<in> next_slot_set x (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; xa \<in> next_slot_set y (cdt_list s) (cdt s); q \<in> next_slot_set xa (cdt_list s) (cdt s); qa \<in> next_slot_set x (cdt_list s) (cdt s) \<and> xa \<in> next_slot_set qa (cdt_list s) (cdt s); qa \<in> next_slot_set y (cdt_list s) (cdt s) \<longrightarrow> cdt s qa \<noteq> Some p; qa \<noteq> y\<rbrakk> \<Longrightarrow> cdt s qa \<noteq> Some p
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa qa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; (xa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (qa, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<and> (xa, qa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (qa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s qa \<noteq> Some p; qa \<noteq> y\<rbrakk> \<Longrightarrow> cdt s qa \<noteq> Some p
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa qa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; (xa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (qa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s qa \<noteq> Some p; qa \<noteq> y; (qa, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (xa, qa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> cdt s qa \<noteq> Some p
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x y xa qa. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2 x p s = Some next; (q, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; y \<noteq> next; y \<noteq> q; cdt s xa = Some p; (xa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (q, xa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (qa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ \<longrightarrow> cdt s qa \<noteq> Some p; qa \<noteq> y; (xa, qa) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (qa, y) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>*\<rbrakk> \<Longrightarrow> cdt s qa \<noteq> Some p
 2. valid_mdb s
 3. valid_list s
 4. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. valid_mdb s
 2. valid_list s
 3. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
next_sib_2 slot p s = Some next
q \<in> next_slot_set slot (cdt_list s) (cdt s)
next \<in> next_slot_set q (cdt_list s) (cdt s)
valid_list s
valid_mdb s

goal (3 subgoals):
 1. valid_mdb s
 2. valid_list s
 3. \<lbrakk>next_sib_2 slot p s = Some next; q \<in> next_slot_set slot (cdt_list s) (cdt s); next \<in> next_slot_set q (cdt_list s) (cdt s); valid_list s; valid_mdb s; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next_sib_2 slot p s \<noteq> Some q; \<exists>q'. next_sib_2 slot p s = Some q' \<and> q \<in> next_slot_set q' (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(q, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; (q, next) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib_2 slot p s = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(q, slot) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; (next, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; no_mloop (cdt s); finite_depth (cdt s); cdt s q = Some p; next \<noteq> q; next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; (q, q) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!