theory Deterministic_AI

lemma next_not_child:
  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 = Some src_p\<rbrakk>
    \<Longrightarrow> next_not_child p (t(src_p := list_insert_after (t src_p) src dest)) 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(erule conjE) apply(rule next_not_childI) apply(rule disjI2) apply(rule conjI) apply(simp add: next_sib) apply(rule_tac p=p and q=src in next_not_child_eq_next_sib_None) apply(simp_all)[6] apply(rule_tac x=src in exI) apply(simp add: next_sib descendants no_mloop_descendants desc) apply(intro allI impI) apply(rule_tac p=p and q=src in next_not_child_eq_next_sib_None) apply(simp_all add: no_mloop_descendants)[6] 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) apply(simp add: descendants_of_def no_mloop_def) apply(simp add: next_sib) 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 descendants) apply(rule disjI2) apply(simp add: next_sib descendants no_mloop_descendants) apply(simp add: descendants_of_def) apply(elim exE conjE) apply(rule_tac x=q in exI) apply(simp) apply(intro conjI impI notI) apply(simp add: desc) apply(simp add: descendants_of_def) apply(simp add: finite_depth) apply(rule next_not_childI) apply(rule disjI1) apply(simp add: next_sib) apply(simp add: finite_depth) apply(case_tac "next_not_child p t m") apply(frule(1) next_not_child_NoneD) apply(simp add: next_sib descendants desc finite_depth
        | rule next_not_child_NoneI)+ apply(intro impI notI) apply(simp) apply(case_tac "next_not_child src t m") apply(simp) apply(drule(2) next_not_childD) apply(erule disjE, simp) apply(elim exE conjE) apply(drule_tac a=p and c=q in descendants_trans, simp, simp) apply(simp add: next_sib) apply(simp add: finite_depth) apply(simp add: next_sib descendants desc no_mloop_descendants
       | drule next_not_childD | rule next_not_childI | erule disjE)+ apply(elim exE conjE) apply(rule_tac x=q in exI) apply(simp) apply(intro conjI impI notI) apply(simp_all add: desc finite_depth) apply(erule notE) apply(rule next_not_childI[symmetric]) apply(simp) apply(rule_tac x=q in exI) apply(fastforce simp: descendants_of_def cdt_parent_defs) apply(simp add: finite_depth) apply(erule notE) apply(rule next_not_childI[symmetric]) apply(simp) 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 = Some src_p\<rbrakk> \<Longrightarrow> next_not_child p (t(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p\<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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child src (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest))) \<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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child src (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> next_not_child p (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> next_sib p (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<or> next_sib p (t(src_p := list_insert_after (t src_p) src dest)) n = None \<and> (\<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(src_p := list_insert_after (t src_p) src dest)) n = None))
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> next_sib p (t(src_p := list_insert_after (t src_p) src dest)) n = None \<and> (\<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(src_p := list_insert_after (t src_p) src dest)) n = None))
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> next_sib p (t(src_p := list_insert_after (t src_p) src dest)) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> \<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(src_p := list_insert_after (t src_p) src dest)) n = None)
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> next_sib p t m = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> \<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(src_p := list_insert_after (t src_p) src dest)) n = None)
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child p t m proof (prove)
goal (11 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> next_not_child p t m = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> p \<in> descendants_of p m \<or> p = p
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> p \<in> descendants_of src m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> valid_list_2 t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth m
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> no_mloop m
 7. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> \<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(src_p := list_insert_after (t src_p) src dest)) n = None)
 8. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 9. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 10. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
A total of 11 subgoals... proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> \<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<and> p \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(src_p := list_insert_after (t src_p) src dest)) n = None)
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> next_sib src (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<and> p \<in> descendants_of src n \<and> (\<forall>q'. q' \<in> descendants_of src n \<and> p \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(src_p := list_insert_after (t src_p) src dest)) n = None)
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> \<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<and> p \<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 = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>q'. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m; q' \<noteq> dest; q' \<noteq> src; q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child p t m proof (prove)
goal (10 subgoals):
 1. \<And>q'. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m; q' \<noteq> dest; q' \<noteq> src; q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_not_child p t m = next_not_child src t m
 2. \<And>q'. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m; q' \<noteq> dest; q' \<noteq> src; q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> p \<in> descendants_of q' m \<or> p = q'
 3. \<And>q'. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m; q' \<noteq> dest; q' \<noteq> src; q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> q' \<in> descendants_of src m
 4. \<And>q'. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m; q' \<noteq> dest; q' \<noteq> src; q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> valid_list_2 t m
 5. \<And>q'. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m; q' \<noteq> dest; q' \<noteq> src; q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> finite_depth m
 6. \<And>q'. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m; q' \<noteq> dest; q' \<noteq> src; q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> no_mloop m
 7. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 8. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 9. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 10. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<noteq> dest; p \<noteq> src; p \<in> descendants_of src m; next_not_child p t m = next_not_child src t m\<rbrakk> \<Longrightarrow> finite_depth n
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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> (src \<in> descendants_of src m \<longrightarrow> (\<forall>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<longrightarrow> q \<noteq> src) \<and> (src \<notin> descendants_of q m \<longrightarrow> q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> dest \<in> descendants_of q m \<longrightarrow> next_sib q t m = None)))) \<and> (src \<notin> descendants_of src m \<longrightarrow> (\<forall>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<longrightarrow> q = src \<longrightarrow> dest \<notin> descendants_of src m) \<and> (src \<notin> descendants_of q m \<longrightarrow> q \<noteq> dest \<longrightarrow> (q = src \<longrightarrow> dest \<notin> descendants_of src m) \<and> (q \<noteq> src \<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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some a
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some a \<or> next_sib dest (t(src_p := list_insert_after (t src_p) src dest)) n = None \<and> (\<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) 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(src_p := list_insert_after (t src_p) src dest)) n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some a \<or> next_sib dest (t(src_p := list_insert_after (t src_p) src dest)) n = None \<and> (\<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) 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(src_p := list_insert_after (t src_p) src dest)) n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some a \<or> next_sib dest (t(src_p := list_insert_after (t src_p) src dest)) n = None \<and> (\<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) 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(src_p := list_insert_after (t src_p) src dest)) n = None))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some a \<or> next_sib dest (t(src_p := list_insert_after (t src_p) src dest)) n = None \<and> (\<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) 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(src_p := list_insert_after (t src_p) src dest)) n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = None \<and> (\<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) 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(src_p := list_insert_after (t src_p) src dest)) n = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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> (q = src \<longrightarrow> dest = a \<and> dest \<in> descendants_of src m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))) \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> (q' = src \<longrightarrow> dest \<notin> descendants_of src m) \<and> (q' \<noteq> src \<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' = src \<longrightarrow> dest \<notin> descendants_of src m) \<and> (q' \<noteq> src \<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> (q = src \<longrightarrow> dest = a \<and> dest \<in> descendants_of src m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))) \<and> (q \<noteq> src \<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' \<noteq> src \<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' \<noteq> src \<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 = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. (x, x) \<notin> (cdt_parent_rel m)\<^sup>+; m src = Some src_p; p = dest; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> m \<Turnstile> q \<rightarrow> src \<and> (\<forall>q'. m \<Turnstile> q \<rightarrow> q' \<and> m \<Turnstile> q' \<rightarrow> src \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. (m \<Turnstile> q \<rightarrow> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. m \<Turnstile> q' \<rightarrow> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> m \<Turnstile> q \<rightarrow> q' \<longrightarrow> next_sib q' t m = None)))) \<and> m \<Turnstile> q \<rightarrow> src
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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; \<forall>x. (x, x) \<notin> (cdt_parent_rel m)\<^sup>+; m src = Some src_p; p = dest; next_sib src t m = None; next_sib q t m = Some a; m \<Turnstile> q \<rightarrow> src; \<forall>q'. m \<Turnstile> q \<rightarrow> q' \<and> m \<Turnstile> q' \<rightarrow> src \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<exists>q. (m \<Turnstile> q \<rightarrow> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. m \<Turnstile> q' \<rightarrow> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> m \<Turnstile> q \<rightarrow> q' \<longrightarrow> next_sib q' t m = None)))) \<and> m \<Turnstile> q \<rightarrow> src
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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; \<forall>x. (x, x) \<notin> (cdt_parent_rel m)\<^sup>+; m src = Some src_p; p = dest; next_sib src t m = None; next_sib q t m = Some a; m \<Turnstile> q \<rightarrow> src; \<forall>q'. m \<Turnstile> q \<rightarrow> q' \<and> m \<Turnstile> q' \<rightarrow> src \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> (m \<Turnstile> q \<rightarrow> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. m \<Turnstile> q' \<rightarrow> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> m \<Turnstile> q \<rightarrow> q' \<longrightarrow> next_sib q' t m = None)))) \<and> m \<Turnstile> q \<rightarrow> src
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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; \<forall>x. (x, x) \<notin> (cdt_parent_rel m)\<^sup>+; m src = Some src_p; p = dest; next_sib src t m = None; next_sib q t m = Some a; m \<Turnstile> q \<rightarrow> src; \<forall>q'. m \<Turnstile> q \<rightarrow> q' \<and> m \<Turnstile> q' \<rightarrow> src \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src)
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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; \<forall>x. (x, x) \<notin> (cdt_parent_rel m)\<^sup>+; m src = Some src_p; p = dest; next_sib src t m = None; next_sib q t m = Some a; m \<Turnstile> q \<rightarrow> src; \<forall>q'. m \<Turnstile> q \<rightarrow> q' \<and> m \<Turnstile> q' \<rightarrow> src \<longrightarrow> next_sib q' t m = None; q = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. (x, x) \<notin> (cdt_parent_rel m)\<^sup>+; m src = Some src_p; p = dest; next_sib src t m = None; next_sib q t m = Some a; m \<Turnstile> q \<rightarrow> src; \<forall>q'. m \<Turnstile> q \<rightarrow> q' \<and> m \<Turnstile> q' \<rightarrow> src \<longrightarrow> next_sib q' t m = None; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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; \<forall>x. (x, x) \<notin> (cdt_parent_rel m)\<^sup>+; m src = Some src_p; p = dest; next_sib src t m = None; next_sib q t m = Some a; m \<Turnstile> q \<rightarrow> src; \<forall>q'. m \<Turnstile> q \<rightarrow> q' \<and> m \<Turnstile> q' \<rightarrow> src \<longrightarrow> next_sib q' t m = None; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<or> next_sib src (t(src_p := list_insert_after (t src_p) src dest)) n = None \<and> (\<exists>q. next_sib q (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest \<and> src \<in> descendants_of q n \<and> (\<forall>q'. q' \<in> descendants_of q n \<and> src \<in> descendants_of q' n \<longrightarrow> next_sib q' (t(src_p := list_insert_after (t src_p) src dest)) n = None))
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child p t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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; (\<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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child p t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> src \<noteq> dest \<longrightarrow> p \<notin> descendants_of src m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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(src_p := list_insert_after (t src_p) src dest)) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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(src_p := list_insert_after (t src_p) src dest)) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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(src_p := list_insert_after (t src_p) src dest)) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None; src \<noteq> dest; p \<in> descendants_of src m; next_not_child src t m = None\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None; src \<noteq> dest; p \<in> descendants_of src m; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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(src_p := list_insert_after (t src_p) src dest)) n = None
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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
 5. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None; src \<noteq> dest; p \<in> descendants_of src m; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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(src_p := list_insert_after (t src_p) src dest)) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None; src \<noteq> dest; p \<in> descendants_of src m; 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> False
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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(src_p := list_insert_after (t src_p) src dest)) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None; src \<noteq> dest; p \<in> descendants_of src m; 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> False
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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(src_p := list_insert_after (t src_p) src dest)) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; src \<noteq> dest; p \<in> descendants_of src m; \<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib p t m = None; 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> False
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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(src_p := list_insert_after (t src_p) src dest)) n = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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(src_p := list_insert_after (t src_p) src dest)) n = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; p \<in> descendants_of src m \<longrightarrow> None \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_not_child p t m = None; (\<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. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) 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 = Some src_p; 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(src_p := list_insert_after (t src_p) src dest)) n = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> (q = src \<longrightarrow> dest = a \<and> p \<in> descendants_of src m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> (q' = src \<longrightarrow> p \<notin> descendants_of src m) \<and> (q' \<noteq> src \<longrightarrow> q' \<in> descendants_of q m \<and> p \<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> (q = src \<longrightarrow> dest = a \<and> p \<in> descendants_of src m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<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; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> (q = src \<longrightarrow> dest = a \<and> p \<in> descendants_of src m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> (q' = src \<longrightarrow> p \<notin> descendants_of src m) \<and> (q' \<noteq> src \<longrightarrow> q' \<in> descendants_of q m \<and> p \<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> (q = src \<longrightarrow> dest = a \<and> p \<in> descendants_of src m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<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; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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> (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> (q = src \<longrightarrow> dest = a \<and> p \<in> descendants_of src m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> (q' = src \<longrightarrow> p \<notin> descendants_of src m) \<and> (q' \<noteq> src \<longrightarrow> q' \<in> descendants_of q m \<and> p \<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> (q = src \<longrightarrow> dest = a \<and> p \<in> descendants_of src m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<longrightarrow> q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<and> (q \<noteq> src \<longrightarrow> next_sib q t m = Some a \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<noteq> dest \<longrightarrow> q' \<noteq> src \<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; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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> (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> (q = src \<longrightarrow> dest = a \<and> p \<in> descendants_of src m) \<and> (q \<noteq> src \<longrightarrow> src \<noteq> dest \<longrightarrow> p \<notin> descendants_of src m))) \<and> (src \<notin> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q = src \<longrightarrow> dest = a \<and> p \<in> descendants_of src m))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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 (8 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> dest = a
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> p \<in> descendants_of src m
 4. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> False
 5. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<notin> descendants_of q m; q = dest\<rbrakk> \<Longrightarrow> False
 6. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<notin> descendants_of q m; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> dest = a
 7. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<notin> descendants_of q m; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> p \<in> descendants_of src m
 8. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> False
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> dest = a proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> Some a = next_not_child src t m
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> dest = a proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> 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))
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> finite_depth m
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> dest = a proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> \<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)
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> finite_depth m
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> dest = a proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> 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)
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> finite_depth m
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> dest = a proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; 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; src \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; src \<noteq> dest; p \<in> descendants_of src m\<rbrakk> \<Longrightarrow> finite_depth m
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> dest = a proof (prove)
goal (1 subgoal):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; Some a \<noteq> next_not_child src t m; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> dest = a proof (prove)
goal (1 subgoal):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> Some a = next_not_child src t m proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> 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))
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> finite_depth m proof (prove)
goal (1 subgoal):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; \<forall>x. x \<notin> descendants_of x m; m src = Some src_p; p \<noteq> dest; p \<noteq> src; next_sib p t m = None; next_sib src t m = Some a; p \<in> descendants_of src m; \<forall>q'. q' \<in> descendants_of src m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; src \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> finite_depth m proof (prove)
goal:
No subgoals!