theory Deterministic_AI

lemma next_slot_set_after_in_list:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>next \<in> next_slot_set slot t m; m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk>
    \<Longrightarrow> next \<in> next_sib_set slot t m" apply(drule(3) next_slot_setD) apply(elim disjE) apply(simp add: descendants_of_def cdt_parent_defs no_mloop_def) apply(drule tranclD2) apply(fastforce dest: trancl_into_trancl rtranclD) apply(simp) apply(elim exE conjE) apply(frule(1) next_sib_set_same_parent) apply(simp) apply(elim conjE exE disjE) apply(fastforce dest: sib_not_desc) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule tranclD2)+ apply(elim exE conjE) apply(drule rtranclD)+ apply(elim disjE) apply(simp add: next_sib_set_not_self) apply(simp) apply(drule_tac x=za and y=q in sib_not_desc) apply(assumption)+ apply(simp add: descendants_of_def cdt_parent_defs) apply(simp) apply(drule_tac x=za and y=pa in sib_not_desc) apply(assumption)+ apply(simp add: descendants_of_def cdt_parent_defs) apply(simp) apply(subgoal_tac "za \<in> descendants_of pa m \<and> za \<in> descendants_of q m") prefer 2 apply(simp add: descendants_of_def cdt_parent_defs) apply(erule conjE, drule(1) descendants_linear) apply(fastforce simp: next_sib_set_not_self) apply(simp add: sib_not_desc) apply(simp) apply(simp add: sib_not_desc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> next_slot_set slot t m; m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; next \<in> descendants_of slot m \<or> next \<in> next_sib_set slot t m \<or> (\<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q})\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; next \<in> descendants_of slot m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; next \<in> next_sib_set slot t m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q}\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; \<forall>p. (p, p) \<notin> {(p, c). m c = Some p}\<^sup>+; finite_depth m; (slot, next) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; next \<in> next_sib_set slot t m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q}\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; \<forall>p. (p, p) \<notin> {(p, c). m c = Some p}\<^sup>+; finite_depth m; \<exists>z. (slot, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, next) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; next \<in> next_sib_set slot t m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q}\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; next \<in> next_sib_set slot t m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q}\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; \<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q}\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (1 subgoal):
 1. \<And>pa q. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; slot \<in> descendants_of pa m \<or> pa = slot; q \<in> next_sib_set pa t m; next \<in> descendants_of q m \<union> {q}\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (1 subgoal):
 1. \<And>pa q. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; slot \<in> descendants_of pa m \<or> pa = slot; q \<in> next_sib_set pa t m; next \<in> descendants_of q m \<union> {q}; \<exists>p. m pa = Some p \<and> m q = Some p\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (1 subgoal):
 1. \<And>pa q. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; slot \<in> descendants_of pa m \<or> pa = slot; q \<in> next_sib_set pa t m; next = q \<or> next \<in> descendants_of q m; \<exists>p. m pa = Some p \<and> m q = Some p\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (4 subgoals):
 1. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; slot \<in> descendants_of pa m; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; slot \<in> descendants_of pa m; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; slot \<in> descendants_of pa m; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (pa, slot) \<in> {(p, c). m c = Some p}\<^sup>+; (q, next) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; \<exists>z. (pa, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, slot) \<in> {(p, c). m c = Some p}; \<exists>z. (q, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, next) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (pa, z) \<in> {(p, c). m c = Some p}\<^sup>*; (z, slot) \<in> {(p, c). m c = Some p}; (q, za) \<in> {(p, c). m c = Some p}\<^sup>*; (za, next) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa = z \<or> pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q = za \<or> q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (6 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa = z; q = za\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa = z; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q = za\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 5. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 6. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (5 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa = z; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q = za\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 5. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (5 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set za t m; m za = Some paa; m q = Some paa; p = za; z = za; pa = za; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q = za\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 5. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (7 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; finite_depth m; q \<in> next_sib_set za t m; m za = Some paa; m q = Some paa; p = za; z = za; pa = za; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> m za = Some (?p66 pa q paa z za)
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; finite_depth m; q \<in> next_sib_set za t m; m za = Some paa; m q = Some paa; p = za; z = za; pa = za; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> m q = Some (?p66 pa q paa z za)
 3. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; finite_depth m; q \<in> next_sib_set za t m; m za = Some paa; m q = Some paa; p = za; z = za; pa = za; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+; za \<notin> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q = za\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 5. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 6. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 7. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (5 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; finite_depth m; q \<in> next_sib_set za t m; m za = Some paa; m q = Some paa; p = za; z = za; pa = za; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+; za \<notin> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q = za\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 5. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (4 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q = za\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (4 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; za \<in> next_sib_set pa t m; m pa = Some paa; m za = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q = za\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (6 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; finite_depth m; za \<in> next_sib_set pa t m; m pa = Some paa; m za = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q = za\<rbrakk> \<Longrightarrow> m za = Some (?p68 pa q paa z za)
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; finite_depth m; za \<in> next_sib_set pa t m; m pa = Some paa; m za = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q = za\<rbrakk> \<Longrightarrow> m pa = Some (?p68 pa q paa z za)
 3. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; finite_depth m; za \<in> next_sib_set pa t m; m pa = Some paa; m za = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q = za; za \<notin> descendants_of pa m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 5. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 6. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (4 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; finite_depth m; za \<in> next_sib_set pa t m; m pa = Some paa; m za = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q = za; za \<notin> descendants_of pa m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; (z, slot) \<in> {(p, c). m c = Some p}; (za, next) \<in> {(p, c). m c = Some p}; pa \<noteq> z \<and> (pa, z) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (4 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+; za \<in> descendants_of pa m \<and> za \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> za \<in> descendants_of pa m \<and> za \<in> descendants_of q m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (4 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> za \<in> descendants_of pa m \<and> za \<in> descendants_of q m
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+; za \<in> descendants_of pa m \<and> za \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+; za \<in> descendants_of pa m \<and> za \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (4 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+; za \<in> descendants_of q m\<rbrakk> \<Longrightarrow> pa \<noteq> q
 2. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+; za \<in> descendants_of q m; pa \<in> descendants_of q m \<or> q \<in> descendants_of pa m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 4. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (3 subgoals):
 1. \<And>pa q paa z za. \<lbrakk>m slot = Some za; m next = Some za; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; p = za; z = za; pa \<noteq> za \<and> (pa, za) \<in> {(p, c). m c = Some p}\<^sup>+; q \<noteq> za \<and> (q, za) \<in> {(p, c). m c = Some p}\<^sup>+; za \<in> descendants_of q m; pa \<in> descendants_of q m \<or> q \<in> descendants_of pa m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 3. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (2 subgoals):
 1. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next = q\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m
 2. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal (1 subgoal):
 1. \<And>pa q paa. \<lbrakk>m slot = Some p; m next = Some p; valid_list_2 t m; no_mloop m; finite_depth m; q \<in> next_sib_set pa t m; m pa = Some paa; m q = Some paa; pa = slot; next \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next \<in> next_sib_set slot t m proof (prove)
goal:
No subgoals!