theory Deterministic_AI

lemma (in mdb_empty_abs') next_slot:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m\<rbrakk>
    \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n
     = (if p = slot then None
       else if next_slot p t m = Some slot then next_slot slot t m
       else next_slot p t m)" apply(case_tac "p=slot") apply(simp add: next_slot_def next_not_child next_child) apply(case_tac "next_slot p t m = Some slot") apply(simp only: next_slot_def next_not_child next_child) apply(case_tac "t slot = []") apply(simp split del: if_split) apply(case_tac "t p = []") apply(fastforce) apply(case_tac "p=slot_p \<and> t slot_p = [slot]") apply(simp) apply(rule impI) apply(subgoal_tac "next_not_child_dom (slot, t, m)") prefer 2 apply(simp add: next_not_child_termination valid_list_2_def) apply(simp) apply(rule impI, erule exE) apply(frule_tac src=slot in next_sib_not_self) apply(drule next_sibD) apply(fastforce) apply(simp split del: if_split) apply(case_tac "p = slot_p") apply(subgoal_tac "list_replace_list (t slot_p) slot [] \<noteq> []") prefer 2 apply(case_tac "t slot_p") apply(simp) apply(simp add: valid_list_2_def) apply(simp split del: if_split) apply(simp) apply(intro conjI impI) apply(case_tac "t slot_p") apply(simp) apply(simp) apply(case_tac list) apply(simp) apply(simp) apply(rule next_not_childI[symmetric]) apply(simp add: next_sib_def) apply(simp) apply(case_tac "t slot_p") apply(simp) apply(simp add: next_child_def) apply(simp) apply(rule conjI) apply(rule impI) apply(case_tac "t p") apply(simp) apply(simp add: valid_list_2_def) apply(erule conjE) apply(erule_tac x=p in allE) apply(simp add: set_eq_subset) apply(intro conjI impI) apply(fastforce simp: valid_list_2_def) apply(case_tac "t p") apply(simp) apply(simp add: next_child_def) apply(simp split del: if_split) apply(case_tac "t p") apply(fastforce) apply(case_tac "t p = [slot]") apply(fastforce) apply(fastforce split: if_split_asm) apply(simp) apply(simp add: next_slot_def split del: if_split) apply(case_tac "t p") apply(fastforce simp: next_not_child next_child) apply(case_tac "t p = [slot]") apply(simp add: next_not_child next_child next_child_def) apply(simp add: next_child next_not_child) apply(fastforce split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p = slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p = []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<and> t slot_p = [slot]\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]\<rbrakk> \<Longrightarrow> next_not_child slot_p t m \<noteq> Some slot \<longrightarrow> next_not_child slot_p t m = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child slot_p t m = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot; next_not_child_dom (slot, t, m)\<rbrakk> \<Longrightarrow> next_not_child slot_p t m = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child_dom (slot, t, m)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child_dom (slot, t, m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot; next_not_child_dom (slot, t, m)\<rbrakk> \<Longrightarrow> next_not_child slot_p t m = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot; next_not_child_dom (slot, t, m)\<rbrakk> \<Longrightarrow> next_not_child slot_p t m = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot; next_not_child_dom (slot, t, m)\<rbrakk> \<Longrightarrow> (\<exists>y. next_sib slot t m = Some y) \<longrightarrow> next_not_child slot_p t m = next_sib slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot; next_not_child_dom (slot, t, m); next_sib slot t m = Some y\<rbrakk> \<Longrightarrow> next_not_child slot_p t m = next_sib slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot; next_not_child_dom (slot, t, m); next_sib slot t m = Some y; next_sib slot t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child slot_p t m = next_sib slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p \<and> t slot_p = [slot]; next_not_child slot_p t m \<noteq> Some slot; next_not_child_dom (slot, t, m); next_sib slot t m \<noteq> Some slot; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = Some y\<rbrakk> \<Longrightarrow> next_not_child slot_p t m = next_sib slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot = []; t p \<noteq> []; \<not> (p = slot_p \<and> t slot_p = [slot])\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if next_child p t = Some slot then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child p t else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p\<rbrakk> \<Longrightarrow> list_replace_list (t slot_p) slot [] \<noteq> []
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p\<rbrakk> \<Longrightarrow> list_replace_list (t slot_p) slot [] \<noteq> []
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p; t slot_p = []\<rbrakk> \<Longrightarrow> list_replace_list (t slot_p) slot [] \<noteq> []
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p; t slot_p = a # list\<rbrakk> \<Longrightarrow> list_replace_list (t slot_p) slot [] \<noteq> []
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 6. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p; t slot_p = a # list\<rbrakk> \<Longrightarrow> list_replace_list (t slot_p) slot [] \<noteq> []
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []\<rbrakk> \<Longrightarrow> (if hd (t slot_p) = slot then after_in_list (t slot_p) slot else Some (hd (t slot_p))) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []\<rbrakk> \<Longrightarrow> (hd (t slot_p) = slot \<longrightarrow> after_in_list (t slot_p) slot = next_not_child slot t m) \<and> (hd (t slot_p) \<noteq> slot \<longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) = slot\<rbrakk> \<Longrightarrow> after_in_list (t slot_p) slot = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) = slot; t slot_p = []\<rbrakk> \<Longrightarrow> after_in_list (t slot_p) slot = next_not_child slot t m
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) = slot; t slot_p = a # list\<rbrakk> \<Longrightarrow> after_in_list (t slot_p) slot = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 6. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) = slot; t slot_p = a # list\<rbrakk> \<Longrightarrow> after_in_list (t slot_p) slot = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; list \<noteq> []; p = slot_p; a = slot; t slot_p = slot # list\<rbrakk> \<Longrightarrow> after_in_list (slot # list) slot = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (6 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; list \<noteq> []; p = slot_p; a = slot; t slot_p = slot # list; list = []\<rbrakk> \<Longrightarrow> after_in_list (slot # list) slot = next_not_child slot t m
 2. \<And>a list aa lista. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; list \<noteq> []; p = slot_p; a = slot; t slot_p = slot # list; list = aa # lista\<rbrakk> \<Longrightarrow> after_in_list (slot # list) slot = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 6. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<And>a list aa lista. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; list \<noteq> []; p = slot_p; a = slot; t slot_p = slot # list; list = aa # lista\<rbrakk> \<Longrightarrow> after_in_list (slot # list) slot = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<And>a list aa lista. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p; a = slot; t slot_p = slot # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> Some aa = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (6 subgoals):
 1. \<And>a list aa lista. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p; a = slot; t slot_p = slot # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> next_sib slot t m = Some aa \<or> next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some aa \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))
 2. \<And>a list aa lista. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p; a = slot; t slot_p = slot # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> finite_depth m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 6. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<And>a list aa lista. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; p = slot_p; a = slot; t slot_p = slot # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> finite_depth m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot; t slot_p = []\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot; t slot_p = a # list\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; slot_p \<noteq> slot; next_child slot_p t = Some slot; t slot = []; t slot_p \<noteq> []; t slot_p \<noteq> [slot]; p = slot_p; list_replace_list (t slot_p) slot [] \<noteq> []; hd (t slot_p) \<noteq> slot; t slot_p = a # list\<rbrakk> \<Longrightarrow> Some (hd (t slot_p)) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p = slot_p \<longrightarrow> t slot_p \<noteq> [slot]; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot [] else t p) \<noteq> [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else if next_not_child p t m = Some slot then next_not_child slot t m else next_not_child p t m) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> (hd (t p) = slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> after_in_list (t p) slot = next_not_child slot t m)) \<and> (hd (t p) \<noteq> slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> Some (hd (t p)) = next_not_child slot t m))
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> hd (t p) = slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> after_in_list (t p) slot = next_not_child slot t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> hd (t p) \<noteq> slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> Some (hd (t p)) = next_not_child slot t m)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) = slot\<rbrakk> \<Longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> after_in_list (t p) slot = next_not_child slot t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> hd (t p) \<noteq> slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> Some (hd (t p)) = next_not_child slot t m)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) = slot; t p = []\<rbrakk> \<Longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> after_in_list (t p) slot = next_not_child slot t m)
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) = slot; t p = a # list\<rbrakk> \<Longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> after_in_list (t p) slot = next_not_child slot t m)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> hd (t p) \<noteq> slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> Some (hd (t p)) = next_not_child slot t m)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) = slot; t p = a # list\<rbrakk> \<Longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> after_in_list (t p) slot = next_not_child slot t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> hd (t p) \<noteq> slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> Some (hd (t p)) = next_not_child slot t m)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; p \<noteq> slot_p; a = slot; t p = slot # list\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> None = next_not_child slot t m) \<and> (list \<noteq> [] \<longrightarrow> after_in_list (slot # list) slot = next_not_child slot t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> hd (t p) \<noteq> slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> Some (hd (t p)) = next_not_child slot t m)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; p \<noteq> slot_p; a = slot; t p = slot # list; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p)\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> None = next_not_child slot t m) \<and> (list \<noteq> [] \<longrightarrow> after_in_list (slot # list) slot = next_not_child slot t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> hd (t p) \<noteq> slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> Some (hd (t p)) = next_not_child slot t m)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; p \<noteq> slot_p; a = slot; t p = slot # list; \<forall>p. distinct (t p); set (t p) = {c. m c = Some p}\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> None = next_not_child slot t m) \<and> (list \<noteq> [] \<longrightarrow> after_in_list (slot # list) slot = next_not_child slot t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> hd (t p) \<noteq> slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> Some (hd (t p)) = next_not_child slot t m)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p\<rbrakk> \<Longrightarrow> hd (t p) \<noteq> slot \<longrightarrow> (t p = [slot] \<longrightarrow> None = next_not_child slot t m) \<and> (t p \<noteq> [slot] \<longrightarrow> Some (hd (t p)) = next_not_child slot t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) \<noteq> slot; t p = [slot]\<rbrakk> \<Longrightarrow> None = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) \<noteq> slot; t p \<noteq> [slot]\<rbrakk> \<Longrightarrow> Some (hd (t p)) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) \<noteq> slot; t p \<noteq> [slot]\<rbrakk> \<Longrightarrow> Some (hd (t p)) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) \<noteq> slot; t p \<noteq> [slot]; t p = []\<rbrakk> \<Longrightarrow> Some (hd (t p)) = next_not_child slot t m
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) \<noteq> slot; t p \<noteq> [slot]; t p = a # list\<rbrakk> \<Longrightarrow> Some (hd (t p)) = next_not_child slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t = Some slot; t slot = []; t p \<noteq> []; p \<noteq> slot_p; hd (t p) \<noteq> slot; t p \<noteq> [slot]; t p = a # list\<rbrakk> \<Longrightarrow> Some (hd (t p)) = next_not_child slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p \<noteq> [] then if False then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t else if False then None else if next_not_child p t m = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else next_not_child p t m) = (if False then None else if Some slot = Some slot then if t slot \<noteq> [] then next_child slot t else next_not_child slot t m else Some slot)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then if next_child p t = Some slot then next_child slot t else next_child p t else if next_not_child p t m = Some slot then next_child slot t else next_not_child p t m) = next_child slot t
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []; t p = []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then if next_child p t = Some slot then next_child slot t else next_child p t else if next_not_child p t m = Some slot then next_child slot t else next_not_child p t m) = next_child slot t
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []; t p = a # list\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then if next_child p t = Some slot then next_child slot t else next_child p t else if next_not_child p t m = Some slot then next_child slot t else next_not_child p t m) = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []; t p = a # list\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then if next_child p t = Some slot then next_child slot t else next_child p t else if next_not_child p t m = Some slot then next_child slot t else next_not_child p t m) = next_child slot t
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []; t p = a # list; t p = [slot]\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then if next_child p t = Some slot then next_child slot t else next_child p t else if next_not_child p t m = Some slot then next_child slot t else next_not_child p t m) = next_child slot t
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []; t p = a # list; t p \<noteq> [slot]\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then if next_child p t = Some slot then next_child slot t else next_child p t else if next_not_child p t m = Some slot then next_child slot t else next_not_child p t m) = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some slot; t slot \<noteq> []; t p = a # list; t p \<noteq> [slot]\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then if next_child p t = Some slot then next_child slot t else next_child p t else if next_not_child p t m = Some slot then next_child slot t else next_not_child p t m) = next_child slot t
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_slot p t m = Some slot then next_slot slot t m else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_slot p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_slot p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) \<noteq> Some slot\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) else next_not_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n) = (if t p \<noteq> [] then next_child p t else next_not_child p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) \<noteq> Some slot; t p = []\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) else next_not_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n) = (if t p \<noteq> [] then next_child p t else next_not_child p t m)
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) \<noteq> Some slot; t p = a # list\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) else next_not_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n) = (if t p \<noteq> [] then next_child p t else next_not_child p t m) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) \<noteq> Some slot; t p = a # list\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) else next_not_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n) = (if t p \<noteq> [] then next_child p t else next_not_child p t m) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) \<noteq> Some slot; t p = a # list; t p = [slot]\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) else next_not_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n) = (if t p \<noteq> [] then next_child p t else next_not_child p t m)
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) \<noteq> Some slot; t p = a # list; t p \<noteq> [slot]\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) else next_not_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n) = (if t p \<noteq> [] then next_child p t else next_not_child p t m) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; (if t p \<noteq> [] then next_child p t else next_not_child p t m) \<noteq> Some slot; t p = a # list; t p \<noteq> [slot]\<rbrakk> \<Longrightarrow> (if (if p = slot_p then list_replace_list (t slot_p) slot (t slot) else t p) \<noteq> [] then next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) else next_not_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n) = (if t p \<noteq> [] then next_child p t else next_not_child p t m) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; no_mloop m; finite_depth m; p \<noteq> slot; next_child p t \<noteq> Some slot; t p = a # list; a = slot \<longrightarrow> list \<noteq> []\<rbrakk> \<Longrightarrow> p = slot_p \<longrightarrow> (next_not_child slot_p t m = Some slot \<longrightarrow> list_replace_list (t slot_p) slot (t slot) = [] \<longrightarrow> next_slot slot t m = next_child slot_p t) \<and> (next_not_child slot_p t m \<noteq> Some slot \<longrightarrow> list_replace_list (t slot_p) slot (t slot) = [] \<longrightarrow> next_not_child slot_p t m = next_child slot_p t) proof (prove)
goal:
No subgoals!