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\<rbrakk>
  \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src))
          = (if p = dest then next_slot src t m
            else next_not_child p t m)" apply(simp) apply(intro conjI impI) apply(case_tac "next_slot src t m") apply(simp add: next_slot_def split: if_split_asm) apply(case_tac "t src", simp, simp add: next_child_def) apply(drule(1) next_not_child_NoneD) apply(rule next_not_child_NoneI) apply(simp add: next_sib' descendants_child no_mloop_descendants desc) apply(simp add: descendants_of_def) apply(simp add: next_sib') apply(simp add: finite_depth_insert_child) apply(simp add: next_slot_def split: if_split_asm) apply(rule next_not_childI) apply(simp add: next_sib) apply(simp add: finite_depth_insert_child) apply(drule(2) next_not_childD) apply(rule next_not_childI) apply(simp add: next_sib' descendants_child) apply(erule disjE) apply(rule_tac x=src in exI) apply(simp add: no_mloop_descendants desc neq) apply(intro allI impI conjI) apply(drule_tac a=src and b=q' and c=src in descendants_trans, simp) apply(simp) apply(simp add: descendants_of_def) apply(elim exE conjE) apply(rule_tac x=q in exI) apply(simp) apply(intro conjI impI notI allI) apply(simp add: desc) apply(simp add: descendants_of_def) apply(simp) apply(simp add: finite_depth_insert_child) apply(case_tac "next_not_child p t m") apply(simp) apply(drule(1) next_not_child_NoneD) apply(rule next_not_child_NoneI) apply(simp add: next_sib descendants_child neq desc) apply(simp add: next_sib) apply(simp add: finite_depth_insert_child) apply(simp) apply(drule(2) next_not_childD) apply(rule next_not_childI) apply(simp add: next_sib descendants_child split del: if_split) apply(erule disjE, simp, simp split del: if_split) apply(elim exE conjE) apply(rule_tac x=q in exI) apply(simp add: desc neq) apply(intro conjI impI notI) apply(simp add: desc) apply(simp add: desc) apply(simp add: finite_depth_insert_child) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = (if p = dest then next_slot src t m 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\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m) \<and> (p \<noteq> dest \<longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = None\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src \<noteq> []; next_child src t = None\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := [dest])) (m(dest \<mapsto> src)) = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_not_child src t m = None\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := [dest])) (m(dest \<mapsto> src)) = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; (\<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_not_child dest (t(src := [dest])) (m(dest \<mapsto> src)) = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; (\<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 (m(dest \<mapsto> src)) \<longrightarrow> next_sib q (t(src := [dest])) (m(dest \<mapsto> src)) = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; (\<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 := [dest])) (m(dest \<mapsto> src)) = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; (\<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 (m(dest \<mapsto> src))
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src = []; (\<forall>q. src \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib src t m = None\<rbrakk> \<Longrightarrow> \<forall>q. src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<longrightarrow> dest \<in> descendants_of q m \<longrightarrow> next_sib q t m = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; (\<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 := [dest])) (m(dest \<mapsto> src)) = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; (\<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 (m(dest \<mapsto> src))
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; (\<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 := [dest])) (m(dest \<mapsto> src)) = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; (\<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 (m(dest \<mapsto> src))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; (\<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 (m(dest \<mapsto> src))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; next_slot src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_slot src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src \<noteq> []; next_child src t = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = Some a
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := [dest])) (m(dest \<mapsto> src)) = Some a
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src \<noteq> []; next_child src t = Some a\<rbrakk> \<Longrightarrow> next_sib dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = Some a \<or> next_sib dest (t(src := dest # t src)) (m(dest \<mapsto> src)) = None \<and> (\<exists>q. next_sib q (t(src := dest # t src)) (m(dest \<mapsto> src)) = Some a \<and> dest \<in> descendants_of q (m(dest \<mapsto> src)) \<and> (\<forall>q'. q' \<in> descendants_of q (m(dest \<mapsto> src)) \<and> dest \<in> descendants_of q' (m(dest \<mapsto> src)) \<longrightarrow> next_sib q' (t(src := dest # t src)) (m(dest \<mapsto> src)) = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src \<noteq> []; next_child src t = Some a\<rbrakk> \<Longrightarrow> finite_depth (m(dest \<mapsto> src))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := [dest])) (m(dest \<mapsto> src)) = Some a
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src \<noteq> []; next_child src t = Some a\<rbrakk> \<Longrightarrow> finite_depth (m(dest \<mapsto> src))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := [dest])) (m(dest \<mapsto> src)) = Some a
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_not_child src t m = Some a\<rbrakk> \<Longrightarrow> next_not_child dest (t(src := [dest])) (m(dest \<mapsto> src)) = Some a
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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_not_child dest (t(src := [dest])) (m(dest \<mapsto> src)) = Some a
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src = []; 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 := [dest])) (m(dest \<mapsto> src)) = Some a \<or> next_sib dest (t(src := [dest])) (m(dest \<mapsto> src)) = None \<and> (\<exists>q. next_sib q (t(src := [dest])) (m(dest \<mapsto> src)) = Some a \<and> dest \<in> descendants_of q (m(dest \<mapsto> src)) \<and> (\<forall>q'. q' \<in> descendants_of q (m(dest \<mapsto> src)) \<and> dest \<in> descendants_of q' (m(dest \<mapsto> src)) \<longrightarrow> next_sib q' (t(src := [dest])) (m(dest \<mapsto> src)) = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src = []; 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> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src = []; next_sib src t m = Some a\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src = []; next_sib src t m = Some a\<rbrakk> \<Longrightarrow> (src \<in> descendants_of src m \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of src m \<and> src \<noteq> src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> dest \<in> descendants_of src m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src 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; p = dest; t src = []; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src = []; next_sib src t m = Some a\<rbrakk> \<Longrightarrow> \<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src 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; p = dest; t src = []; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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 \<notin> descendants_of x m; p = dest; t src = []; next_sib src t m = Some a; src \<in> descendants_of q' m; q' \<noteq> dest; q' \<in> descendants_of src m\<rbrakk> \<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; p = dest; t src = []; next_sib src t m = Some a; src \<notin> descendants_of q' m \<and> q' \<noteq> src; q' \<noteq> dest; q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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 \<notin> descendants_of x m; p = dest; t src = []; next_sib src t m = Some a; q' \<noteq> dest; q' \<in> descendants_of src m; src \<in> descendants_of src m\<rbrakk> \<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; p = dest; t src = []; next_sib src t m = Some a; src \<notin> descendants_of q' m \<and> q' \<noteq> src; q' \<noteq> dest; q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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 \<notin> descendants_of x m; p = dest; t src = []; next_sib src t m = Some a; src \<notin> descendants_of q' m \<and> q' \<noteq> src; q' \<noteq> dest; q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p = dest; t src = []; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some a \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<exists>q. (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> (src \<in> descendants_of q m \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<noteq> dest \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (q = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> next_sib src t m = Some a \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<longrightarrow> next_sib q' t m = None) \<and> (q' = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> next_sib src t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of src m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)))) \<and> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> next_sib q t m = Some a \<and> dest \<in> descendants_of q m \<and> (\<forall>q'. (src \<in> descendants_of q' m \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<longrightarrow> next_sib q' t m = None) \<and> (src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> (\<forall>q'. src \<notin> descendants_of q' m \<and> q' \<noteq> src \<longrightarrow> q' \<noteq> dest \<longrightarrow> q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<and> q \<noteq> src
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (5 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>a q q'. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q \<noteq> dest; src \<notin> descendants_of q' m \<and> q' \<noteq> src; q' \<noteq> dest; q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 3. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q = src\<rbrakk> \<Longrightarrow> False
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<And>a q q'. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q \<noteq> dest; src \<notin> descendants_of q' m \<and> q' \<noteq> src; q' \<noteq> dest; q' \<in> descendants_of q m \<and> dest \<in> descendants_of q' m\<rbrakk> \<Longrightarrow> next_sib q' t m = None
 2. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q = src\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; next_sib src t m = None; next_sib q t m = Some a; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; q = src\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p = dest; t src = []; 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 (m(dest \<mapsto> src))
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; next_not_child p t m = None\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; next_not_child p t m = None\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; (\<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 := dest # t src)) (m(dest \<mapsto> src)) = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None\<rbrakk> \<Longrightarrow> \<forall>q. p \<in> descendants_of q (m(dest \<mapsto> src)) \<longrightarrow> next_sib q (t(src := dest # t src)) (m(dest \<mapsto> src)) = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; (\<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 := dest # t src)) (m(dest \<mapsto> src)) = None
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; (\<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 (m(dest \<mapsto> src))
 4. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; (\<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 := dest # t src)) (m(dest \<mapsto> src)) = None
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; (\<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 (m(dest \<mapsto> src))
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = next_not_child p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; (\<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 (m(dest \<mapsto> src))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p \<noteq> dest; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = 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; p \<noteq> dest; next_not_child p t m = Some a\<rbrakk> \<Longrightarrow> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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> next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = Some a proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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> next_sib p (t(src := dest # t src)) (m(dest \<mapsto> src)) = Some a \<or> next_sib p (t(src := dest # t src)) (m(dest \<mapsto> src)) = None \<and> (\<exists>q. next_sib q (t(src := dest # t src)) (m(dest \<mapsto> src)) = Some a \<and> p \<in> descendants_of q (m(dest \<mapsto> src)) \<and> (\<forall>q'. q' \<in> descendants_of q (m(dest \<mapsto> src)) \<and> p \<in> descendants_of q' (m(dest \<mapsto> src)) \<longrightarrow> next_sib q' (t(src := dest # t src)) (m(dest \<mapsto> src)) = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 (m(dest \<mapsto> src)) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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> next_sib p t m = Some a \<or> next_sib p t m = None \<and> (\<exists>q. (if q = dest then next_child src t else next_sib q t m) = Some a \<and> p \<in> (if src \<in> descendants_of q m \<or> q = src then insert dest (descendants_of q m) else descendants_of q m) \<and> (\<forall>q'. q' \<in> (if src \<in> descendants_of q m \<or> q = src then insert dest (descendants_of q m) else descendants_of q m) \<and> p \<in> (if src \<in> descendants_of q' m \<or> q' = src then insert dest (descendants_of q' m) else descendants_of q' m) \<longrightarrow> (if q' = dest then next_child src t else next_sib q' t m) = None))
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 (m(dest \<mapsto> src)) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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. (if q = dest then next_child src t else next_sib q t m) = Some a \<and> p \<in> (if src \<in> descendants_of q m \<or> q = src then insert dest (descendants_of q m) else descendants_of q m) \<and> (\<forall>q'. q' \<in> (if src \<in> descendants_of q m \<or> q = src then insert dest (descendants_of q m) else descendants_of q m) \<and> p \<in> (if src \<in> descendants_of q' m \<or> q' = src then insert dest (descendants_of q' m) else descendants_of q' m) \<longrightarrow> (if q' = dest then next_child src t else next_sib q' t m) = None)
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 (m(dest \<mapsto> src)) proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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. (if q = dest then next_child src t else next_sib q t m) = Some a \<and> p \<in> (if src \<in> descendants_of q m \<or> q = src then insert dest (descendants_of q m) else descendants_of q m) \<and> (\<forall>q'. q' \<in> (if src \<in> descendants_of q m \<or> q = src then insert dest (descendants_of q m) else descendants_of q m) \<and> p \<in> (if src \<in> descendants_of q' m \<or> q' = src then insert dest (descendants_of q' m) else descendants_of q' m) \<longrightarrow> (if q' = dest then next_child src t else next_sib q' t m) = None)
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 (m(dest \<mapsto> src)) proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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> (if q = dest then next_child src t else next_sib q t m) = Some a \<and> p \<in> (if src \<in> descendants_of q m \<or> q = src then insert dest (descendants_of q m) else descendants_of q m) \<and> (\<forall>q'. q' \<in> (if src \<in> descendants_of q m \<or> q = src then insert dest (descendants_of q m) else descendants_of q m) \<and> p \<in> (if src \<in> descendants_of q' m \<or> q' = src then insert dest (descendants_of q' m) else descendants_of q' m) \<longrightarrow> (if q' = dest then next_child src t else next_sib q' t m) = None)
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 (m(dest \<mapsto> src)) proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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> (src \<notin> descendants_of q m \<and> q \<noteq> src \<longrightarrow> q \<noteq> dest)
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 (m(dest \<mapsto> src)) proof (prove)
goal (3 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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; no_mloop m; p \<noteq> dest; 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 \<and> q \<noteq> src; q = dest\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 (m(dest \<mapsto> src)) proof (prove)
goal (2 subgoals):
 1. \<And>a q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 \<and> q \<noteq> src; q = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; p \<noteq> dest; 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 (m(dest \<mapsto> src)) proof (prove)
goal:
No subgoals!