theory Deterministic_AI

lemma next_not_child_NoneD':
  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 = None; finite_depth m\<rbrakk>
    \<Longrightarrow> (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and>
        next_sib p t m = None" apply(induct p rule: next_not_child_pinduct[where t=t and m=m]) apply(subgoal_tac "next_sib slot t m = None") prefer 2 apply(subst(asm)(2) next_not_child.psimps) apply(simp add: next_not_child_termination) apply(case_tac "next_sib slot t m") apply(simp) apply(simp) apply(simp) apply(intro allI impI) apply(case_tac "m slot") apply(subst(asm)(2) next_not_child.psimps) apply(simp add: next_not_child_termination) apply(case_tac "next_sib slot t m") apply(simp add: descendants_of_def cdt_parent_defs) apply(drule tranclD2) apply(fastforce) apply(simp) apply(atomize) apply(erule_tac x=a in allE) apply(simp) apply(erule impE) apply(simp add: next_not_child_termination) apply(case_tac "q=a") apply(simp add: next_not_child_termination split: if_split_asm) apply(erule conjE) apply(erule_tac x=q in allE) apply(erule impE) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule tranclD2) apply(elim conjE exE) apply(simp) apply(drule rtranclD) apply(simp) apply(simp) using f_d apply(simp) done

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