theory Deterministic_AI

lemma next_not_child_helper''':
notes split_paired_All[simp del] split_paired_Ex[simp del]
  notes nnext = next_not_child.psimps[OF next_not_child_termination[OF findepth]]
  notes nnext' = next_not_child.psimps[OF next_not_child_termination[OF finite_depth]]

shows
"\<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a;
        next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' =
        (if a = src then None
         else if a = dest then next_not_child src t m
              else if next_not_child a t m = Some src then Some dest else next_not_child a t m);
        next_sib slot t m = None\<rbrakk>
       \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' =
          (if slot = src then None
           else if slot = dest then next_not_child src t m
                else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m)" apply (case_tac "src_p = dest") apply simp apply (simp add: next_sib m'_helpers
          nnext[where slot=slot]
          nnext[where slot=dest]
          nnext[where slot=src]

          nnext'[where slot=slot]
          nnext'[where slot=dest]
          nnext'[where slot=src]
split: if_split_asm) apply (intro impI conjI,simp_all) apply (drule next_not_childD[OF _ findepth no_mloop]) apply (elim disjE) apply (frule(1) next_sib_same_parent,simp) apply (elim conjE exE) apply (frule (1) next_sib_same_parent,simp) apply (frule parent_not_descendant[OF no_mloop],simp) apply (rule next_not_child_parent,simp+) apply (frule next_sib_not_self[where src=src],simp) apply (intro impI conjI) apply (rule next_not_child_parent,simp+) apply (intro impI conjI) apply (rule next_not_child_parent,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); next_sib slot t m = None\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); next_sib slot t m = None; src_p = dest\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m)
 2. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); next_sib slot t m = None; src_p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); next_sib slot t m = None; src_p \<noteq> dest\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> (next_not_child src_p t m = Some src \<longrightarrow> (slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some src) \<and> (slot \<noteq> dest \<longrightarrow> slot \<noteq> src \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest)) \<and> (next_not_child src_p t m \<noteq> Some src \<longrightarrow> (slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> (slot \<noteq> dest \<longrightarrow> slot \<noteq> src \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m))) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> (next_sib src t m = None \<longrightarrow> (next_not_child src_p t m = Some src \<longrightarrow> (slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some src) \<and> (slot \<noteq> dest \<longrightarrow> slot \<noteq> src \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest)) \<and> (next_not_child src_p t m \<noteq> Some src \<longrightarrow> (slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> (slot \<noteq> dest \<longrightarrow> slot \<noteq> src \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m))) \<and> (next_sib src t m = Some src \<longrightarrow> slot \<noteq> dest \<longrightarrow> slot = src) \<and> (next_sib src t m \<noteq> Some src \<longrightarrow> next_sib src t m = None \<longrightarrow> (slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> (slot \<noteq> dest \<longrightarrow> slot \<noteq> src \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)))
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; next_not_child src_p t m = Some src; slot \<noteq> dest; slot \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; next_not_child src_p t m \<noteq> Some src; slot \<noteq> dest; slot \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = Some src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> slot = src
 4. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 5. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; slot \<noteq> dest; slot \<noteq> src; next_sib src_p t m = Some src \<or> next_sib src_p t m = None \<and> (\<exists>q. next_sib q t m = Some src \<and> src_p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src_p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; next_not_child src_p t m \<noteq> Some src; slot \<noteq> dest; slot \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = Some src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> slot = src
 4. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 5. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; slot \<noteq> dest; slot \<noteq> src; next_sib src_p t m = Some src\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; slot \<noteq> dest; slot \<noteq> src; next_sib src_p t m = None \<and> (\<exists>q. next_sib q t m = Some src \<and> src_p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src_p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; next_not_child src_p t m \<noteq> Some src; slot \<noteq> dest; slot \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 4. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = Some src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> slot = src
 5. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 6. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; slot \<noteq> dest; slot \<noteq> src; next_sib src_p t m = None \<and> (\<exists>q. next_sib q t m = Some src \<and> src_p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src_p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; next_not_child src_p t m \<noteq> Some src; slot \<noteq> dest; slot \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = Some src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> slot = src
 4. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 5. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (5 subgoals):
 1. \<And>q. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; slot \<noteq> dest; slot \<noteq> src; next_sib src_p t m = None; next_sib q t m = Some src; src_p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src_p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; next_not_child src_p t m \<noteq> Some src; slot \<noteq> dest; slot \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = Some src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> slot = src
 4. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 5. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (5 subgoals):
 1. \<And>q. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; slot \<noteq> dest; slot \<noteq> src; next_sib src_p t m = None; next_sib q t m = Some src; src_p \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src_p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some src_p\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; next_not_child src_p t m \<noteq> Some src; slot \<noteq> dest; slot \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = Some src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> slot = src
 4. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 5. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = None; next_not_child src_p t m \<noteq> Some src; slot \<noteq> dest; slot \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = Some src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> slot = src
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 4. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some src; a = src; next_sib src t m = Some src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> slot = src
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m)
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest; next_sib src t m = None; slot = dest\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m = Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = Some dest; \<exists>y. next_sib src t m = Some y; next_sib src t m = None; slot = dest\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 3. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m; next_sib src t m = None; slot = dest\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m
 2. \<lbrakk>next_sib slot t m = None; src_p \<noteq> dest; valid_list_2 t m; m src = Some src_p; src_p \<noteq> src; m src_p \<noteq> Some src; m slot = Some a; a \<noteq> src; a \<noteq> dest; next_not_child a t m \<noteq> Some src; next_not_child a (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child a t m; \<exists>y. next_sib src t m = Some y; next_sib src t m = None; slot = dest\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m proof (prove)
goal:
No subgoals!