theory Deterministic_AI

lemma (in mdb_empty_abs') next_sib:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_list_2 t m; m slot = Some slot_p\<rbrakk>
    \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n
     = (if p = slot then None
       else if next_sib p t m = Some slot then
         if t slot = [] then next_sib slot t m
         else next_child slot t
       else if m p = Some slot \<and> after_in_list (t slot) p = None then
         next_sib slot t m
       else next_sib p t m)" apply(case_tac "p=slot") apply(simp) apply(fastforce simp: n_def intro: next_sib_NoneI) apply(case_tac "next_sib p t m = Some slot") apply(simp, intro conjI impI) apply(case_tac "next_sib slot t m") apply(simp) apply(drule next_sib_NoneD) apply(erule disjE) apply(fastforce intro: next_sib_NoneI) apply(drule next_sibD) apply(elim exE conjE) apply(rule next_sib_NoneI) apply(rule disjI2) apply(rule conjI) apply(fastforce simp: n_def) apply(simp, intro conjI impI) apply(simp add: list_replace_empty_after_empty valid_list_2_def) apply(drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(simp) apply(drule next_sibD)+ apply(elim exE conjE) apply(rule next_sibI) apply(fastforce simp: n_def) apply(simp) apply(intro conjI impI notI) apply(simp) apply(simp add: list_replace_empty_after_empty valid_list_2_def) apply(simp) apply(drule after_in_list_in_list, simp add: valid_list_2_def) apply(drule next_sibD, elim exE conjE) apply(case_tac "next_child slot t") apply(simp, drule next_child_NoneD) apply(rule next_sib_NoneI, simp add: n_def) apply(simp, drule(1) next_childD) apply(elim exE conjE) apply(rule next_sibI) apply(simp add: n_def) apply(intro conjI impI) apply(simp) apply(drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(simp) apply(intro conjI impI notI, simp) apply(subst list_replace_after_fst_list) apply(frule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(simp add: valid_list_2_def) apply(simp) apply(simp) apply(intro conjI impI) apply(case_tac "next_sib slot t m") apply(simp) apply(drule next_sib_NoneD) apply(erule disjE) apply(fastforce simp: n_def intro: next_sib_NoneI) apply(elim exE conjE) apply(rule next_sib_NoneI) apply(rule disjI2) apply(rule conjI) apply(fastforce simp: n_def) apply(simp) apply(rule impI) apply(drule_tac list="t slot_p" and slot=slot in list_replace_after_None_notin_old) apply(simp add: valid_list_2_def) apply(simp add: valid_list_2_def) apply(simp) apply(simp) apply(drule next_sibD) apply(elim exE conjE) apply(rule next_sibI) apply(simp add: n_def) apply(simp) apply(intro conjI impI notI) apply simp apply(drule_tac list="t slot_p" and slot=slot in list_replace_after_None_notin_old) apply(simp add: valid_list_2_def) apply(simp add: valid_list_2_def) apply(simp) apply(case_tac "next_sib p t m") apply(simp) apply(drule next_sib_NoneD) apply(erule disjE) apply(fastforce intro: next_sib_NoneI simp: n_def) apply(elim exE conjE) apply(case_tac "pa=slot") apply(fastforce intro: next_sib_NoneI) apply(rule_tac p=pa in next_sib_NoneI) apply(rule disjI2) apply(fastforce simp add: valid_list_2_def n_def list_replace_after_None_notin_new) apply(simp) apply(drule next_sibD) apply(elim exE conjE) apply(case_tac "pa=slot") apply(rule next_sibI) apply(simp add: n_def) apply(simp) apply(fastforce intro: list_replace_after_notin_old simp: valid_list_2_def) apply(simp) apply(rule next_sibI) apply(simp add: n_def) apply(fastforce intro: list_replace_after_notin_new simp: valid_list_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p = slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p = slot\<rbrakk> \<Longrightarrow> next_sib slot (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; m slot = None \<or> (\<exists>p. m slot = Some p \<and> after_in_list (t p) slot = None)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; m slot = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = None; \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m slot = Some pa; after_in_list (t pa) slot = None; m p = Some paa; after_in_list (t paa) p = Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m slot = Some pa; after_in_list (t pa) slot = None; m p = Some paa; after_in_list (t paa) p = Some slot\<rbrakk> \<Longrightarrow> n p = None \<or> n p = Some (?p41 pa paa) \<and> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) (?p41 pa paa)) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m slot = Some pa; after_in_list (t pa) slot = None; m p = Some paa; after_in_list (t paa) p = Some slot\<rbrakk> \<Longrightarrow> n p = Some (?p41 pa paa) \<and> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) (?p41 pa paa)) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (5 subgoals):
 1. \<And>pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m slot = Some pa; after_in_list (t pa) slot = None; m p = Some paa; after_in_list (t paa) p = Some slot\<rbrakk> \<Longrightarrow> n p = Some (?p41 pa paa)
 2. \<And>pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m slot = Some pa; after_in_list (t pa) slot = None; m p = Some paa; after_in_list (t paa) p = Some slot\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) (?p41 pa paa)) p = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m slot = Some pa; after_in_list (t pa) slot = None; m p = Some paa; after_in_list (t paa) p = Some slot\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) paa) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (5 subgoals):
 1. \<And>pa paa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; t slot = []; m slot = Some slot_p; after_in_list (t slot_p) slot = None; m p = Some paa; after_in_list (t paa) p = Some slot; paa = slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot []) p = None
 2. \<And>pa paa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; t slot = []; m slot = Some slot_p; after_in_list (t slot_p) slot = None; m p = Some paa; after_in_list (t paa) p = Some slot; paa \<noteq> slot_p\<rbrakk> \<Longrightarrow> paa = slot
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>pa paa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; t slot = []; m slot = Some slot_p; after_in_list (t slot_p) slot = None; m p = Some paa; after_in_list (t paa) p = Some slot; paa \<noteq> slot_p\<rbrakk> \<Longrightarrow> paa = slot
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>pa paa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; t slot = []; m slot = Some slot_p; after_in_list (t slot_p) slot = None; m p = Some paa; paa \<noteq> slot_p; slot \<in> set (t paa)\<rbrakk> \<Longrightarrow> paa = slot
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = next_sib slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot = []; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = Some slot; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>a pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some paa; after_in_list (t paa) slot = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) n = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>a pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some paa; after_in_list (t paa) slot = Some a\<rbrakk> \<Longrightarrow> n p = Some (?p86 a pa paa)
 2. \<And>a pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some paa; after_in_list (t paa) slot = Some a\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) (?p86 a pa paa)) p = Some a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>a pa paa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some paa; after_in_list (t paa) slot = Some a\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot [], slot := [])) pa) p = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a\<rbrakk> \<Longrightarrow> (pa = slot_p \<longrightarrow> slot_p \<noteq> slot \<and> (slot_p \<noteq> slot \<longrightarrow> after_in_list (list_replace_list (t slot_p) slot []) p = Some a)) \<and> (pa \<noteq> slot_p \<longrightarrow> pa \<noteq> slot \<and> (pa \<noteq> slot \<longrightarrow> slot = a))
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (6 subgoals):
 1. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa = slot_p; slot_p = slot\<rbrakk> \<Longrightarrow> False
 2. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa = slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot []) p = Some a
 3. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa \<noteq> slot_p; pa = slot\<rbrakk> \<Longrightarrow> False
 4. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa \<noteq> slot_p; pa \<noteq> slot\<rbrakk> \<Longrightarrow> slot = a
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 6. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (5 subgoals):
 1. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa = slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot []) p = Some a
 2. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa \<noteq> slot_p; pa = slot\<rbrakk> \<Longrightarrow> False
 3. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa \<noteq> slot_p; pa \<noteq> slot\<rbrakk> \<Longrightarrow> slot = a
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa \<noteq> slot_p; pa = slot\<rbrakk> \<Longrightarrow> False
 2. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa \<noteq> slot_p; pa \<noteq> slot\<rbrakk> \<Longrightarrow> slot = a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>a pa paa. \<lbrakk>valid_list_2 t m; paa = slot_p; p \<noteq> slot; t slot = []; m p = Some pa; after_in_list (t pa) p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; pa \<noteq> slot_p; pa \<noteq> slot\<rbrakk> \<Longrightarrow> slot = a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m = Some slot; t slot \<noteq> []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; next_child slot t = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 2. \<And>pa a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; next_child slot t = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; t slot = []\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>pa a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; next_child slot t = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<And>pa a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; next_child slot t = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_child slot t
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<And>pa a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; (\<exists>xs. t slot = a # xs) \<and> m a = Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> n p = Some (?p152 pa a xs)
 2. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) (?p152 pa a xs)) p = Some a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> (pa = slot \<longrightarrow> slot_p = ?p152 slot a xs) \<and> (pa \<noteq> slot \<longrightarrow> pa = ?p152 pa a xs)
 2. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) (?p152 pa a xs)) p = Some a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; pa = slot\<rbrakk> \<Longrightarrow> slot_p = ?p152 slot a xs
 2. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; pa \<noteq> slot\<rbrakk> \<Longrightarrow> pa = ?p152 pa a xs
 3. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) (?p152 pa a xs)) p = Some a
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; pa \<noteq> slot\<rbrakk> \<Longrightarrow> pa = slot_p
 2. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) slot_p) p = Some a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; m a = Some slot; t slot = a # xs; pa \<noteq> slot; slot \<in> set (t pa)\<rbrakk> \<Longrightarrow> pa = slot_p
 2. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) slot_p) p = Some a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t slot \<noteq> []; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) slot_p) p = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs\<rbrakk> \<Longrightarrow> slot_p \<noteq> slot \<and> (slot_p \<noteq> slot \<longrightarrow> after_in_list (list_replace_list (t slot_p) slot (a # xs)) p = Some a)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (a # xs)) p = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (t slot_p) p = Some slot
 2. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (t slot_p)
 3. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> Some a = Some a
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (4 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot; slot \<in> set (t pa)\<rbrakk> \<Longrightarrow> after_in_list (t slot_p) p = Some slot
 2. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (t slot_p)
 3. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> Some a = Some a
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (3 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (t slot_p)
 2. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> Some a = Some a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<And>pa a xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some slot; m a = Some slot; t slot = a # xs; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> Some a = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = (if p = slot then None else if next_sib p t m = Some slot then if t slot = [] then next_sib slot t m else next_child slot t else if m p = Some slot \<and> after_in_list (t slot) p = None then next_sib slot t m else next_sib p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot\<rbrakk> \<Longrightarrow> (m p = Some slot \<and> after_in_list (t slot) p = None \<longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m) \<and> ((m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)) \<longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; m slot = None \<or> (\<exists>p. m slot = Some p \<and> after_in_list (t p) slot = None)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; m slot = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = None\<rbrakk> \<Longrightarrow> n p = None \<or> n p = Some (?p201 pa) \<and> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) (?p201 pa)) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = None\<rbrakk> \<Longrightarrow> n p = Some (?p201 pa) \<and> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) (?p201 pa)) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (4 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = None\<rbrakk> \<Longrightarrow> n p = Some (?p201 pa)
 2. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = None\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) (?p201 pa)) p = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = None\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) pa) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some slot_p; after_in_list (t slot_p) slot = None\<rbrakk> \<Longrightarrow> slot_p \<noteq> slot \<longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some slot_p; after_in_list (t slot_p) slot = None; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (5 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = None; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> p \<in> set (t slot)
 2. \<And>pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = None; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> p \<notin> set (t slot_p)
 3. \<And>pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = None; slot_p \<noteq> slot; after_in_list (list_replace_list (t slot_p) slot (t slot)) p = after_in_list (t slot_p) slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = None
 4. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 5. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (4 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = None; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> p \<notin> set (t slot_p)
 2. \<And>pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = None; slot_p \<noteq> slot; after_in_list (list_replace_list (t slot_p) slot (t slot)) p = after_in_list (t slot_p) slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = None; slot_p \<noteq> slot; after_in_list (list_replace_list (t slot_p) slot (t slot)) p = after_in_list (t slot_p) slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib slot t m
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; next_sib slot t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<and> after_in_list (t slot) p = None; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = Some a\<rbrakk> \<Longrightarrow> n p = Some (?p224 a pa)
 2. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = Some a\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) (?p224 a pa)) p = Some a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some pa; after_in_list (t pa) slot = Some a\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) pa) p = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a\<rbrakk> \<Longrightarrow> slot_p \<noteq> slot \<and> (slot_p \<noteq> slot \<longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = Some a)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; slot_p = slot\<rbrakk> \<Longrightarrow> False
 2. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = Some a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; after_in_list (t slot) p = None; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (4 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> p \<in> set (t slot)
 2. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> p \<notin> set (t slot_p)
 3. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; slot_p \<noteq> slot; after_in_list (list_replace_list (t slot_p) slot (t slot)) p = after_in_list (t slot_p) slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = Some a
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> p \<notin> set (t slot_p)
 2. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; slot_p \<noteq> slot; after_in_list (list_replace_list (t slot_p) slot (t slot)) p = after_in_list (t slot_p) slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = Some a
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; pa = slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot; m slot = Some slot_p; after_in_list (t slot_p) slot = Some a; slot_p \<noteq> slot; after_in_list (list_replace_list (t slot_p) slot (t slot)) p = after_in_list (t slot_p) slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = Some a
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = None \<or> (\<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = None)\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = None; pa = slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = None; pa \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = None; pa \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = None; pa \<noteq> slot\<rbrakk> \<Longrightarrow> n p = None \<or> n p = Some pa \<and> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) pa) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = None; pa \<noteq> slot\<rbrakk> \<Longrightarrow> n p = Some pa \<and> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) pa) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_sib p t m \<noteq> Some slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = next_sib p t m proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a proof (prove)
goal (2 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a; pa = slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a
 2. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a; pa \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a proof (prove)
goal (3 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a; pa = slot\<rbrakk> \<Longrightarrow> n p = Some (?p310 a pa)
 2. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a; pa = slot\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) (?p310 a pa)) p = Some a
 3. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a; pa \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a proof (prove)
goal (2 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a; pa = slot\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) slot_p) p = Some a
 2. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a; pa \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a proof (prove)
goal (2 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot; after_in_list (t slot) p = Some a; pa = slot\<rbrakk> \<Longrightarrow> slot_p \<noteq> slot \<and> (slot_p \<noteq> slot \<longrightarrow> after_in_list (list_replace_list (t slot_p) slot (t slot)) p = Some a)
 2. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a; pa \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some slot \<longrightarrow> (\<exists>y. after_in_list (t slot) p = Some y); m p = Some pa; after_in_list (t pa) p = Some a; pa \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some a; pa \<noteq> slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n = Some a proof (prove)
goal (2 subgoals):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some a; pa \<noteq> slot\<rbrakk> \<Longrightarrow> n p = Some (?p350 a pa)
 2. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some a; pa \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) (?p350 a pa)) p = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a pa. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; m p = Some pa; after_in_list (t pa) p = Some a; pa \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list ((t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) pa) p = Some a proof (prove)
goal:
No subgoals!