theory Deterministic_AI

lemma next_not_child_no_parent:
    notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None\<rbrakk>
    \<Longrightarrow> next_not_child p t n
    = (if p = src then (if m src = None then None else Some dest)
       else if p = dest then next_not_child src t m
       else if p \<in> descendants_of src m
         \<and> next_not_child p t m = next_not_child src t m then
           (if m src = None then None else Some dest)
       else next_not_child p t m)" apply(simp) apply(intro conjI impI) apply(simp add: descendants_of_def) apply(simp add: no_mloop_def descendants_of_def) apply(subgoal_tac "next_not_child src t m = None") prefer 2 apply(rule next_not_child_NoneI) apply(fastforce dest: descendants_of_NoneD) apply(simp add: next_sib_def) apply(simp) apply(erule conjE, simp) apply(drule(1) next_not_child_NoneD[where p=p]) apply(rule next_not_child_NoneI) apply(simp add: next_sib_no_parent descendants desc) apply(simp add: next_sib_no_parent) apply(simp add: finite_depth) apply(case_tac "next_not_child src t m") apply(simp) apply(drule(1) next_not_child_NoneD, rule next_not_child_NoneI) apply(simp add: descendants next_sib_no_parent) apply(simp add: descendants_of_def ) apply(simp add: next_sib_no_parent) apply(simp add: finite_depth) apply(simp) apply(drule(2) next_not_childD, rule next_not_childI) apply(erule disjE) apply(simp add: next_sib_no_parent descendants) apply(rule disjI2) apply(simp add: next_sib_no_parent descendants) apply(elim exE conjE) apply(rule_tac x=q in exI) apply(simp) apply(intro allI conjI impI notI) apply(simp add: desc) apply(simp add: descendants_of_def) apply(simp add: finite_depth) apply(rule next_not_child_NoneI) apply(intro allI impI) apply(fastforce simp: descendants split: if_split_asm dest: descendants_of_NoneD) apply(simp add: next_sib_no_parent) apply(simp add: next_sib_def) apply(simp add: finite_depth) apply(case_tac "next_not_child p t m") apply(simp add: next_sib_no_parent descendants desc finite_depth
        | drule next_not_child_NoneD | rule next_not_child_NoneI)+ apply(simp add: next_sib_no_parent descendants desc
       | drule next_not_childD | rule next_not_childI | erule disjE)+ apply(elim exE conjE) apply(rule_tac x=q in exI) apply(case_tac "m dest") apply(fastforce simp: next_sib_def) apply(fastforce simp: next_sib_def dest) apply(simp add: finite_depth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None\<rbrakk> \<Longrightarrow> next_not_child p t n = (if p = src then if m src = None then None else Some dest else if p = dest then next_not_child src t m else if p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m then if m src = None then None else Some dest else next_not_child p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None\<rbrakk> \<Longrightarrow> (p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m \<longrightarrow> (p = dest \<longrightarrow> next_not_child dest t n = next_not_child src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child src t n = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p t n = None))) \<and> ((p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m) \<longrightarrow> (p = dest \<longrightarrow> next_not_child dest t n = next_not_child src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child src t n = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p t n = next_not_child p t m))) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src t m = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src t m = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (7 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> \<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_sib src t m = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> finite_depth m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 7. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_sib src t m = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> finite_depth m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> finite_depth m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None; p \<in> descendants_of src m; next_not_child p t m = None\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None; p \<in> descendants_of src m; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> next_not_child p t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None; p \<in> descendants_of src m; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> \<forall>q. p \<in> descendants_of q n \<longrightarrow> next_sib q t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None; p \<in> descendants_of src m; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> next_sib p t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None; p \<in> descendants_of src m; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None; p \<in> descendants_of src m; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> next_sib p t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None; p \<in> descendants_of src m; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<noteq> dest; p \<noteq> src; next_not_child src t m = None; p \<in> descendants_of src m; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child dest t n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> \<forall>q. dest \<in> descendants_of q n \<longrightarrow> next_sib q t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> next_sib dest t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> \<forall>q. src \<notin> descendants_of q m \<longrightarrow> q \<noteq> dest \<longrightarrow> dest \<in> descendants_of q m \<longrightarrow> next_sib q t m = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> next_sib dest t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> next_sib dest t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> (\<exists>y. next_not_child dest t m = Some y); p = dest; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> finite_depth n
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = dest; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest t n = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest t n = Some a
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib dest t n = Some a \<or> next_sib dest t n = None \<and> (\<exists>q. next_sib q t n = Some a \<and> dest \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> dest \<in> descendants_of q' n \<longrightarrow> next_sib q' t n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a\<rbrakk> \<Longrightarrow> next_sib dest t n = Some a \<or> next_sib dest t n = None \<and> (\<exists>q. next_sib q t n = Some a \<and> dest \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> dest \<in> descendants_of q' n \<longrightarrow> next_sib q' t n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib dest t n = Some a \<or> next_sib dest t n = None \<and> (\<exists>q. next_sib q t n = Some a \<and> dest \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> dest \<in> descendants_of q' n \<longrightarrow> next_sib q' t n = None))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib dest t n = Some a \<or> next_sib dest t n = None \<and> (\<exists>q. next_sib q t n = Some a \<and> dest \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> dest \<in> descendants_of q' n \<longrightarrow> next_sib q' t n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_sib dest t n = None \<and> (\<exists>q. next_sib q t n = Some a \<and> dest \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> dest \<in> descendants_of q' n \<longrightarrow> next_sib q' t n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> (\<forall>q'. src \<notin> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>a q q'. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q \<noteq> dest; src \<notin> descendants_of q' m; q' \<noteq> dest; q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a q q'. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q \<noteq> dest; src \<notin> descendants_of q' m; q' \<noteq> dest; q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; dest \<in> descendants_of src m \<longrightarrow> next_not_child dest t m \<noteq> Some a; p = dest; next_sib src t m = Some a \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_not_child src t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> \<forall>q. src \<in> descendants_of q n \<longrightarrow> next_sib q t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_sib src t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src; src \<in> descendants_of q n\<rbrakk> \<Longrightarrow> next_sib q t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_sib src t n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_sib src t n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; src \<notin> descendants_of src m; src \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_sib src t m = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> finite_depth n
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p t n = next_not_child p t m proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p t n = Some a proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<exists>q. q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m dest = None\<rbrakk> \<Longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))
 2. \<And>a q aa. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m dest = Some aa\<rbrakk> \<Longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (2 subgoals):
 1. \<And>a q aa. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib q t m = Some a; p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m dest = Some aa\<rbrakk> \<Longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None; p \<in> descendants_of src m \<longrightarrow> Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> finite_depth n proof (prove)
goal:
No subgoals!