theory Deterministic_AI

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_not_child p t m = Some n; finite_depth m; no_mloop m\<rbrakk> \<Longrightarrow> 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)) proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_not_child a t m = Some n; finite_depth m; no_mloop m\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m\<rbrakk> \<Longrightarrow> 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))
 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_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m\<rbrakk> \<Longrightarrow> 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))
 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_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = None\<rbrakk> \<Longrightarrow> 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))
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a\<rbrakk> \<Longrightarrow> 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))
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = None\<rbrakk> \<Longrightarrow> 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))
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a\<rbrakk> \<Longrightarrow> 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))
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = None; \<not> (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_sib slot t m = Some n
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a\<rbrakk> \<Longrightarrow> 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))
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = None; (\<exists>y. next_sib slot t m = Some y) \<or> (\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = Some n \<longrightarrow> (\<exists>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<and> (\<exists>y. next_sib q' t m = Some y)))\<rbrakk> \<Longrightarrow> next_sib slot t m = Some n
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a\<rbrakk> \<Longrightarrow> 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))
 3. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = None; \<exists>y. next_sib slot t m = Some y\<rbrakk> \<Longrightarrow> next_sib slot t m = Some n
 2. \<And>slot. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = None; \<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = Some n \<longrightarrow> (\<exists>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<and> (\<exists>y. next_sib q' t m = Some y))\<rbrakk> \<Longrightarrow> next_sib slot t m = Some n
 3. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot y. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = None; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = Some y\<rbrakk> \<Longrightarrow> next_sib slot t m = Some n
 2. \<And>slot. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = None; \<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = Some n \<longrightarrow> (\<exists>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<and> (\<exists>y. next_sib q' t m = Some y))\<rbrakk> \<Longrightarrow> next_sib slot t m = Some n
 3. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = None; \<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = Some n \<longrightarrow> (\<exists>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<and> (\<exists>y. next_sib q' t m = Some y))\<rbrakk> \<Longrightarrow> next_sib slot t m = Some n
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a\<rbrakk> \<Longrightarrow> 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))
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; next_not_child a t m = Some n\<rbrakk> \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a\<rbrakk> \<Longrightarrow> 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))
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>a. next_sib slot t m = None \<longrightarrow> m slot = Some a \<longrightarrow> next_not_child a t m = Some n \<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)); next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a\<rbrakk> \<Longrightarrow> 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))
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> m slot = Some a \<longrightarrow> next_not_child a t m = Some n \<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))\<rbrakk> \<Longrightarrow> 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))
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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))\<rbrakk> \<Longrightarrow> 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))
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = None\<rbrakk> \<Longrightarrow> 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))
 2. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None\<rbrakk> \<Longrightarrow> \<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)
 2. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 3. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> \<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)
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; 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)); next_sib slot t m = None; next_not_child a t m = Some n\<rbrakk> \<Longrightarrow> \<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)
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n\<rbrakk> \<Longrightarrow> \<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)
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n\<rbrakk> \<Longrightarrow> next_sib a t m = Some n \<and> slot \<in> descendants_of a m \<and> (\<forall>q'. q' \<in> descendants_of a m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n\<rbrakk> \<Longrightarrow> slot \<in> descendants_of a m \<and> (\<forall>q'. q' \<in> descendants_of a m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (6 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n\<rbrakk> \<Longrightarrow> slot \<in> descendants_of a m
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of a m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 4. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 5. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 6. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of a m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n; q' \<in> descendants_of a m \<and> slot \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n; (a, q') \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (q', slot) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n; (a, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', slot) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n; (a, q') \<in> {(p, c). m c = Some p}\<^sup>+; \<exists>z. (q', z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, slot) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q' z. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = Some n; (a, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>*; (z, slot) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q' z. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some z; next_sib slot t m = None; next_not_child z t m = Some n; next_sib z t m = Some n; (z, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', z) \<in> {(p, c). m c = Some p}\<^sup>*; a = z\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (6 subgoals):
 1. \<And>slot a q' z. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some z; next_sib slot t m = None; next_not_child z t m = Some n; next_sib z t m = Some n; (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 a q' z. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some z; next_sib slot t m = None; next_not_child z t m = Some n; next_sib z t m = Some n; (q', z) \<in> {(p, c). m c = Some p}\<^sup>*; a = z; (z, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 4. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 5. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 6. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q' z. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some z; next_sib slot t m = None; next_not_child z t m = Some n; next_sib z t m = Some n; (q', z) \<in> {(p, c). m c = Some p}\<^sup>*; a = z; (z, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; 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> \<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)
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<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)
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<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_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)
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> 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)
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> slot \<in> descendants_of q m
 2. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; \<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\<rbrakk> \<Longrightarrow> (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (6 subgoals):
 1. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; \<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\<rbrakk> \<Longrightarrow> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; \<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\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}
 3. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None
 4. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 5. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 6. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; \<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\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}
 2. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a = q'\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'; q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'\<rbrakk> \<Longrightarrow> q' \<in> descendants_of q m \<and> a \<in> descendants_of q' m
 2. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'; next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; (q, a) \<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>+; a \<noteq> q'\<rbrakk> \<Longrightarrow> (q', a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'; next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> q'; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (q', slot) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (q', a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'; next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> q'; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; \<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 a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'; next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q q' z. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> q'; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (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 a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'; next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q q' z. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some z; next_sib slot t m = None; next_not_child z t m = Some n; next_sib z t m = None; next_sib q t m = Some n; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; z \<noteq> q'; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; (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 a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'; next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q q' z. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some z; next_sib slot t m = None; next_not_child z t m = Some n; next_sib z t m = None; next_sib q t m = Some n; (q, z) \<in> {(p, c). m c = Some p}\<^sup>+; z \<noteq> q'; (q, q') \<in> {(p, c). m c = Some p}\<^sup>+; 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 a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'; next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 4. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 5. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q q'. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None; next_not_child a t m = Some n; next_sib a t m = None; next_sib q t m = Some n; a \<in> descendants_of q m; q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m; a \<noteq> q'; next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 3. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 4. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_not_child a t m = Some n \<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)); next_sib slot t m = None; next_not_child a t m \<noteq> Some n\<rbrakk> \<Longrightarrow> \<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)
 2. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a aa. \<lbrakk>next_not_child slot t m = Some n; finite_depth m; no_mloop m; m slot = Some a; next_sib slot t m = None \<longrightarrow> next_not_child a t m = Some n \<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)); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> 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))
 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!