theory Deterministic_AI

lemma next_not_childI':
    notes split_paired_All[simp del] split_paired_Ex[simp del]
  assumes f_d: "finite_depth m" shows
  "\<lbrakk>next_sib p t m = Some n \<or>
   (next_sib p t m = None \<and>
     (\<exists>q. next_sib q t m = Some n \<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))); finite_depth m\<rbrakk>
    \<Longrightarrow> next_not_child p t m = Some n" apply(induct p rule: next_not_child_pinduct[where t=t and m=m]) apply(simp) apply(erule disjE) apply(simp add: next_not_child_termination) apply(simp) apply(elim conjE exE) apply(subst next_not_child.psimps, simp add: next_not_child_termination) apply(simp) apply(case_tac "m slot") apply(simp) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule tranclD2) apply(fastforce) apply(atomize) apply(erule_tac x=a in allE) apply(simp) apply(case_tac "next_sib a t m") apply(simp) apply(case_tac "a=q") apply(simp) apply(erule impE) apply(rule_tac x=q in exI) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule tranclD2) apply(elim exE conjE, simp) apply(drule rtranclD, simp) apply(intro allI impI) apply(erule_tac x=q' in allE) apply(simp) apply(elim impE conjE) apply(drule_tac x=q' and y=z in tranclD2) apply(elim exE conjE) apply(simp) apply(rule_tac b=z in trancl_into_trancl) apply(rule_tac b=za in rtrancl_into_trancl1) apply(simp) apply(simp) apply(simp) apply(simp) apply(simp) apply(simp) apply(case_tac "a=q") apply(simp) apply(erule_tac x=a in allE) apply(erule_tac Q="next_sib a t m = None" in impE) apply(simp add: descendants_of_def cdt_parent_defs) apply(rule conjI) apply(drule tranclD2) apply(elim conjE exE) apply(simp) apply(drule rtranclD) apply(simp) apply(fastforce) apply(simp) using f_d apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib p t m = Some n \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some n \<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)); finite_depth m\<rbrakk> \<Longrightarrow> next_not_child p t m = Some n proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); finite_depth m\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; next_sib slot t m = Some n \<or> next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); finite_depth m\<rbrakk> \<Longrightarrow> next_not_child slot t m = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; next_sib slot t m = Some n \<or> next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); finite_depth m\<rbrakk> \<Longrightarrow> next_not_child slot t m = Some n
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = Some n\<rbrakk> \<Longrightarrow> next_not_child slot t m = Some n
 2. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child slot t m = Some n
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child slot t m = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child slot t m = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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\<rbrakk> \<Longrightarrow> next_not_child slot t m = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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\<rbrakk> \<Longrightarrow> (if next_sib slot t m = None then case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m else next_sib slot t m) = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = None\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n
 2. \<And>slot q a. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = None\<rbrakk> \<Longrightarrow> False
 2. \<And>slot q a. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (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 slot = None\<rbrakk> \<Longrightarrow> False
 2. \<And>slot q a. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; \<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 slot = None; \<exists>z. (q, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, slot) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> False
 2. \<And>slot q a. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q a. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q a. \<lbrakk>\<forall>a. m slot = Some a \<longrightarrow> next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n; finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; m slot = Some a \<longrightarrow> next_sib a t m = Some n \<or> next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n)\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = None; a = q\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = None; a \<noteq> q\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = None; a \<noteq> q\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q\<rbrakk> \<Longrightarrow> \<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q\<rbrakk> \<Longrightarrow> next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (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 slot = Some a; next_sib a t m = None; a \<noteq> q\<rbrakk> \<Longrightarrow> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (\<forall>q'. (q, q') \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (q', a) \<in> {(p, c). m c = Some p}\<^sup>+ \<longrightarrow> next_sib q' t m = None)
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; \<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 slot = Some a; next_sib a t m = None; a \<noteq> q; \<exists>z. (q, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, slot) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (\<forall>q'. (q, q') \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (q', a) \<in> {(p, c). m c = Some p}\<^sup>+ \<longrightarrow> next_sib q' t m = None)
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a z. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; \<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 slot = Some z; next_sib z t m = None; z \<noteq> q; (q, z) \<in> {(p, c). m c = Some p}\<^sup>*; a = z\<rbrakk> \<Longrightarrow> (q, z) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (\<forall>q'. (q, q') \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (q', z) \<in> {(p, c). m c = Some p}\<^sup>+ \<longrightarrow> next_sib q' t m = None)
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a z. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; \<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 slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> \<forall>q'. (q, q') \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (q', z) \<in> {(p, c). m c = Some p}\<^sup>+ \<longrightarrow> next_sib q' t m = None
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; \<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 slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (q', z) \<in> {(p, c). m c = Some p}\<^sup>+; (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\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (q', z) \<in> {(p, c). m c = Some p}\<^sup>+; (q', slot) \<in> {(p, c). m c = Some p}\<^sup>+ \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (q', slot) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; next_sib q' t m = None; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; \<exists>za. (q', za) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (za, z) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (q', slot) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; next_sib q' t m = None; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; (za, z) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (q', slot) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; next_sib q' t m = None; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; m z = Some za\<rbrakk> \<Longrightarrow> (q', slot) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; next_sib q' t m = None; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 5. finite_depth m proof (prove)
goal (6 subgoals):
 1. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; m z = Some za\<rbrakk> \<Longrightarrow> (q', z) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; m z = Some za\<rbrakk> \<Longrightarrow> (z, slot) \<in> {(p, c). m c = Some p}
 3. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; next_sib q' t m = None; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 4. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 5. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 6. finite_depth m proof (prove)
goal (7 subgoals):
 1. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; m z = Some za\<rbrakk> \<Longrightarrow> (q', za) \<in> {(p, c). m c = Some p}\<^sup>*
 2. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; m z = Some za\<rbrakk> \<Longrightarrow> (za, z) \<in> {(p, c). m c = Some p}
 3. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; m z = Some za\<rbrakk> \<Longrightarrow> (z, slot) \<in> {(p, c). m c = Some p}
 4. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; next_sib q' t m = None; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 5. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 6. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 7. finite_depth m proof (prove)
goal (6 subgoals):
 1. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; m z = Some za\<rbrakk> \<Longrightarrow> (za, z) \<in> {(p, c). m c = Some p}
 2. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; m z = Some za\<rbrakk> \<Longrightarrow> (z, slot) \<in> {(p, c). m c = Some p}
 3. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; next_sib q' t m = None; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 4. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 5. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 6. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot q a z q' za. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', za) \<in> {(p, c). m c = Some p}\<^sup>*; m z = Some za\<rbrakk> \<Longrightarrow> (z, slot) \<in> {(p, c). m c = Some p}
 2. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; next_sib q' t m = None; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 5. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a z q'. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; next_sib z t m = None; z \<noteq> q; a = z; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; next_sib q' t m = None; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q a. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; next_sib a t m = None; a \<noteq> q; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; (next_sib a t m = Some n \<longrightarrow> next_not_child a t m = Some n) \<and> (next_sib a t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> a \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<longrightarrow> next_not_child a t m = Some n); next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a = q\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; 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 slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; a \<in> descendants_of q m \<and> slot \<in> descendants_of a m \<longrightarrow> next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> a \<in> descendants_of q m \<and> slot \<in> descendants_of a m
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (a, slot) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; \<exists>z. (q, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, slot) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a aa z. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; (q, z) \<in> {(p, c). m c = Some p}\<^sup>*; (z, slot) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a aa z. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; aa = n \<longrightarrow> next_not_child z t m = Some n; next_sib z t m = Some aa; z \<noteq> q; (q, z) \<in> {(p, c). m c = Some p}\<^sup>*; a = z\<rbrakk> \<Longrightarrow> (q, z) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot q a aa z. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; m slot = Some z; aa = n \<longrightarrow> next_not_child z t m = Some n; next_sib z t m = Some aa; z \<noteq> q; a = z; q = z \<or> q \<noteq> z \<and> (q, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (q, z) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 4. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot q a aa. \<lbrakk>finite_depth m; next_sib slot t m = None; next_sib q t m = Some n; slot \<in> descendants_of q m; m slot = Some a; aa = n \<longrightarrow> next_not_child a t m = Some n; next_sib a t m = Some aa; a \<noteq> q; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = Some n
 2. finite_depth m proof (prove)
goal (1 subgoal):
 1. finite_depth m proof (prove)
using this:
finite_depth m

goal (1 subgoal):
 1. finite_depth m proof (prove)
goal:
No subgoals!