theory Deterministic_AI

lemma next_not_child_linearI:
  notes split_paired_All[simp del] split_paired_Ex[simp del] if_weak_cong[cong]
  assumes f_d: "finite_depth m" shows
  "\<lbrakk>m p = m' p; next_sib p t m = next_sib p t' m';
     \<forall>q. p \<in> descendants_of q m \<longrightarrow> m q = m' q
     \<and> next_sib q t m = next_sib q t' m'; finite_depth m; finite_depth m'\<rbrakk>
    \<Longrightarrow> next_not_child p t' m' = next_not_child p t m" supply subst_all [simp del] apply(induct rule: next_not_child_pinduct[where t=t and m=m]) apply(simp) apply(case_tac "m slot") apply(simp add: next_not_child_termination) apply(case_tac "next_sib slot t m") apply(simp add: next_not_child_termination) apply(case_tac "m' slot") apply(simp) apply(simp) apply(atomize) apply(erule_tac x=aa in allE) apply(simp split: if_split_asm) apply(case_tac "m' aa") apply(simp) apply(simp add: next_not_child_termination) apply(intro conjI impI) apply(case_tac "m aa") apply(simp) apply(erule_tac x=aa in allE) apply(erule impE) apply(fastforce simp: cdt_parent_defs descendants_of_def) apply(simp) apply(erule exE) apply(erule_tac x=aa in allE) (* condense *)
       apply(erule impE) apply(fastforce simp: cdt_parent_defs descendants_of_def) apply(simp) apply(simp) apply(erule impE) apply(erule_tac x=aa in allE) apply(fastforce simp: cdt_parent_defs descendants_of_def) apply(erule impE) apply(erule_tac x=aa in allE) apply(fastforce simp: cdt_parent_defs descendants_of_def) apply(erule impE) apply(intro allI impI) apply(erule_tac x=q in allE) apply(erule impE) apply(simp add: cdt_parent_defs descendants_of_def) apply(rule_tac b=aa in trancl_into_trancl) apply(simp, simp) apply(simp) apply(erule_tac x= aa in allE) apply(erule impE) apply(fastforce simp: cdt_parent_defs descendants_of_def) apply(simp add: next_not_child_termination)  (* condense *)
     apply(erule_tac x=aa in allE) apply(erule impE) apply(fastforce simp: cdt_parent_defs descendants_of_def) apply(simp add: next_not_child_termination) apply(simp) apply(fastforce simp: next_not_child_termination) using f_d apply(assumption) done

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