theory Deterministic_AI

lemma (in mdb_empty_abs') next_not_child_no_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>valid_list_2 t m; finite_depth m; m slot = None\<rbrakk>
    \<Longrightarrow> next_not_child p (t(slot := [])) n
    = (if (\<exists>sl. next_not_child p t m = Some sl \<and> m sl = Some slot)
        then None
      else next_not_child p t m)" apply(simp) apply(intro conjI impI) apply(elim exE conjE) apply(drule(1) next_not_childD, simp add: no_mloop) apply(rule next_not_child_NoneI) apply(simp add: next_sib_no_parent descendants) apply(intro allI impI) apply(erule disjE) apply(drule next_sibD) apply(elim exE conjE) apply(drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule tranclD2, simp) apply(drule rtranclD, simp) apply(drule tranclD2, simp) apply(elim conjE exE) apply(erule_tac x=q in allE) apply(erule impE) apply(simp) apply(drule next_sibD) apply(elim exE conjE) apply(drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(drule_tac a=p and b=q and c=qa in descendants_linear) apply(simp) apply(fastforce) apply(erule disjE) apply(simp) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule_tac x=q in tranclD2, simp) apply(drule rtranclD, simp) apply(drule_tac x=q in tranclD2, simp) apply(simp) apply(simp add: next_sib_no_parent) apply(rule impI) apply(erule disjE) apply(drule next_sibD) apply(elim exE conjE) apply(drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(simp) apply(simp add: finite_depth) apply(case_tac "next_not_child p t m") apply(simp) apply(drule(1) next_not_child_NoneD) apply(rule next_not_child_NoneI) apply(intro allI impI) apply(simp add: next_sib_no_parent descendants split: if_split_asm) apply(simp add: next_sib_no_parent) apply(simp add: finite_depth) apply(simp) apply(drule(1) next_not_childD, simp add: no_mloop) apply(rule next_not_childI) apply(erule disjE) apply(rule disjI1) apply(simp add: next_sib_no_parent) apply(drule next_sibD) apply(elim exE conjE, drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(rule disjI2) apply(rule conjI) apply(simp add: next_sib_no_parent) apply(elim conjE exE) apply(rule_tac x=q in exI) apply(intro conjI) apply(simp add: next_sib_no_parent) apply(drule next_sibD) apply(elim exE conjE, drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(simp add: descendants) apply(drule next_sibD) apply(elim exE conjE, drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(rule conjI) apply(fastforce) apply(intro notI impI) apply(simp) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule tranclD2, simp) apply(intro allI impI) apply(simp add: next_sib_no_parent descendants split: if_split_asm) apply(simp add: finite_depth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = (if \<exists>sl. next_not_child p t m = Some sl \<and> m sl = Some slot then None else next_not_child p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None\<rbrakk> \<Longrightarrow> ((\<exists>sl. next_not_child p t m = Some sl \<and> m sl = Some slot) \<longrightarrow> next_not_child p (t(slot := [])) n = None) \<and> ((\<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot) \<longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<exists>sl. next_not_child p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; next_not_child p t m = Some sl; m sl = Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<forall>q. p \<in> descendants_of q n \<longrightarrow> next_sib q (t(slot := [])) n = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<forall>q. q \<noteq> slot \<longrightarrow> m q \<noteq> Some slot \<longrightarrow> p \<in> descendants_of q m \<and> p \<noteq> slot \<longrightarrow> next_sib q t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = Some sl\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = Some sl\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q pa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some sl\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q pa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; m p = Some pa; sl \<in> set (t pa)\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<in> descendants_of q m; p \<noteq> pa; m p = Some pa; slot = pa\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; (q, p) \<in> {(p, c). m c = Some p}\<^sup>+; p \<noteq> pa; m p = Some pa; slot = pa\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; m p = Some pa; slot = pa; (q, pa) \<in> {(p, c). m c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; m p = Some pa; slot = pa; (q, pa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m \<and> p \<noteq> slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; \<forall>q'. q' \<in> descendants_of qa m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; q \<in> descendants_of qa m \<and> p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m \<and> p \<in> descendants_of q m
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; p \<in> descendants_of qa m; \<exists>p. m qa = Some p \<and> after_in_list (t p) qa = Some sl\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; after_in_list (t pa) qa = Some sl\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; sl \<in> set (t pa)\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<in> descendants_of q m; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (7 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa\<rbrakk> \<Longrightarrow> p \<in> descendants_of qa m
 2. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa\<rbrakk> \<Longrightarrow> q \<noteq> qa
 3. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa; q \<in> descendants_of qa m \<or> qa \<in> descendants_of q m\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 4. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 5. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 6. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 7. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (6 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa\<rbrakk> \<Longrightarrow> q \<noteq> qa
 2. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa; q \<in> descendants_of qa m \<or> qa \<in> descendants_of q m\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 3. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 5. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 6. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa; q \<in> descendants_of qa m \<or> qa \<in> descendants_of q m\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (6 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa; q \<in> descendants_of qa m\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 2. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa; qa \<in> descendants_of q m\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 3. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 5. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 6. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; p \<in> descendants_of qa m; m qa = Some pa; slot = pa; qa \<in> descendants_of q m\<rbrakk> \<Longrightarrow> q \<in> descendants_of qa m
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; (qa, p) \<in> {(p, c). m c = Some p}\<^sup>+; m qa = Some pa; slot = pa; (q, qa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (qa, q) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; (qa, p) \<in> {(p, c). m c = Some p}\<^sup>+; m qa = Some pa; slot = pa; (q, pa) \<in> {(p, c). m c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> (qa, q) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>sl q qa pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m pa = None; m sl = Some pa; q \<noteq> pa; m q \<noteq> Some pa; p \<noteq> pa; next_sib p t m = None; (qa, p) \<in> {(p, c). m c = Some p}\<^sup>+; m qa = Some pa; slot = pa; (q, pa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (qa, q) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 4. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 5. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl q qa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; q \<noteq> slot; m q \<noteq> Some slot; p \<in> descendants_of q m; p \<noteq> slot; next_sib p t m = None; next_sib qa t m = Some sl; p \<in> descendants_of qa m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> m p \<noteq> Some slot \<longrightarrow> next_sib p t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); m p \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; m p \<noteq> Some slot; next_sib p t m = Some sl\<rbrakk> \<Longrightarrow> next_sib p t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; m p \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; m p \<noteq> Some slot; \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = Some sl\<rbrakk> \<Longrightarrow> next_sib p t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; m p \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl pa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; m p \<noteq> Some slot; m p = Some pa; after_in_list (t pa) p = Some sl\<rbrakk> \<Longrightarrow> next_sib p t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; m p \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>sl pa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; m p \<noteq> Some slot; m p = Some pa; sl \<in> set (t pa)\<rbrakk> \<Longrightarrow> next_sib p t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; m p \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p t m = None
 3. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; m p \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p t m = None
 2. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m sl = Some slot; next_sib p t m = Some sl \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some sl \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 2. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot; next_not_child p t m = None\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; next_not_child p t m = None\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> \<forall>q. p \<in> descendants_of q n \<longrightarrow> next_sib q (t(slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None; p \<in> descendants_of q n\<rbrakk> \<Longrightarrow> next_sib q (t(slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; \<forall>sl. next_not_child p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = next_not_child p t m proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = Some a proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = Some a \<or> next_sib p (t(slot := [])) n = None \<and> (\<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = Some a \<or> next_sib p (t(slot := [])) n = None \<and> (\<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = Some a \<or> next_sib p (t(slot := [])) n = None \<and> (\<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = Some a
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = Some a \<or> next_sib p (t(slot := [])) n = None \<and> (\<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> m p \<noteq> Some slot
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = Some a \<or> next_sib p (t(slot := [])) n = None \<and> (\<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = Some a\<rbrakk> \<Longrightarrow> m p \<noteq> Some slot
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = Some a \<or> next_sib p (t(slot := [])) n = None \<and> (\<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; m p = Some pa; a \<in> set (t pa)\<rbrakk> \<Longrightarrow> m p \<noteq> Some slot
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = Some a \<or> next_sib p (t(slot := [])) n = None \<and> (\<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = Some a \<or> next_sib p (t(slot := [])) n = None \<and> (\<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None \<and> (\<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None)
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None)
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<exists>q. next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None)
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q (t(slot := [])) n = Some a \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None)
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (4 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q (t(slot := [])) n = Some a
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> p \<in> descendants_of q n
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (4 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> m q \<noteq> Some slot
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> p \<in> descendants_of q n
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (4 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; \<exists>p. m q = Some p \<and> after_in_list (t p) q = Some a\<rbrakk> \<Longrightarrow> m q \<noteq> Some slot
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> p \<in> descendants_of q n
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (4 subgoals):
 1. \<And>a q pa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some pa; a \<in> set (t pa)\<rbrakk> \<Longrightarrow> m q \<noteq> Some slot
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> p \<in> descendants_of q n
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> p \<in> descendants_of q n
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> q \<noteq> slot \<and> (q \<noteq> slot \<longrightarrow> p \<noteq> slot)
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; \<exists>p. m q = Some p \<and> after_in_list (t p) q = Some a\<rbrakk> \<Longrightarrow> q \<noteq> slot \<and> (q \<noteq> slot \<longrightarrow> p \<noteq> slot)
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q pa. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some pa; a \<in> set (t pa)\<rbrakk> \<Longrightarrow> q \<noteq> slot \<and> (q \<noteq> slot \<longrightarrow> p \<noteq> slot)
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m slot = None; pa \<noteq> slot; next_sib p t m = None; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some pa; m a = Some pa\<rbrakk> \<Longrightarrow> q \<noteq> slot \<and> (q \<noteq> slot \<longrightarrow> p \<noteq> slot)
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (4 subgoals):
 1. \<And>a q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m slot = None; pa \<noteq> slot; next_sib p t m = None; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some pa; m a = Some pa\<rbrakk> \<Longrightarrow> q \<noteq> slot
 2. \<And>a q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m slot = None; pa \<noteq> slot; next_sib p t m = None; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some pa; m a = Some pa\<rbrakk> \<Longrightarrow> q \<noteq> slot \<longrightarrow> p \<noteq> slot
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m slot = None; pa \<noteq> slot; next_sib p t m = None; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some pa; m a = Some pa\<rbrakk> \<Longrightarrow> q \<noteq> slot \<longrightarrow> p \<noteq> slot
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m slot = None; pa \<noteq> slot; next_sib p t m = None; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some pa; m a = Some pa; q \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> False
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m slot = None; pa \<noteq> slot; next_sib slot t m = None; slot \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some pa; m a = Some pa; q \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> False
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q pa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); finite_depth m; m slot = None; pa \<noteq> slot; next_sib slot t m = None; (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+; \<forall>q'. (q, q') \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (q', slot) \<in> {(p, c). m c = Some p}\<^sup>+ \<longrightarrow> next_sib q' t m = None; m q = Some pa; m a = Some pa; q \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> False
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a q q'. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n\<rbrakk> \<Longrightarrow> next_sib q' (t(slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; m slot = None; m a \<noteq> Some slot; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal:
No subgoals!