theory Deterministic_AI

lemma next_not_child_parent:
notes split_paired_All[simp del] split_paired_Ex[simp del]
shows
"\<lbrakk>valid_list_2 t m; m src = 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' =
       next_not_child src_p t m" apply (case_tac "src_p = dest",simp) apply (insert src_loop_facts[where src_p=src_p]) apply (rule next_not_child_linearI'[OF findepth finite_depth]) apply (simp add: m'_def m''_def) apply (simp add: next_sib) apply (rule notI) apply (frule(1) next_sib_same_parent,simp) apply (intro impI allI conjI) apply (simp add: m'_def m''_def) apply (intro impI conjI) apply (rule notI) apply simp apply (cut_tac dest_desc,simp) apply (rule notI) apply simp apply (frule parent_not_descendant[OF no_mloop],simp) apply (rule notI) apply (subgoal_tac "q \<in> descendants_of src_p m") apply (frule ancestor_not_descendant[OF no_mloop],simp) apply (rule descendants_trans) apply (rule child_descendant) apply simp apply (rule child_descendant) apply simp apply (simp add: next_sib) apply (intro impI conjI) apply (simp add:  m'_helpers)+ apply (frule(1) next_sib_same_parent,simp) apply (frule parent_not_descendant[OF no_mloop],simp) apply (simp add: m'_def m''_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = 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' = next_not_child src_p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> 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 (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<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 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src\<rbrakk> \<Longrightarrow> m src_p = m' src_p
 2. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src\<rbrakk> \<Longrightarrow> next_sib src_p t m = next_sib src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m'
 3. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src\<rbrakk> \<Longrightarrow> \<forall>q. src_p \<in> descendants_of q m \<longrightarrow> m q = m' q \<and> (m q = m' q \<longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src\<rbrakk> \<Longrightarrow> next_sib src_p t m = next_sib src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m'
 2. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src\<rbrakk> \<Longrightarrow> \<forall>q. src_p \<in> descendants_of q m \<longrightarrow> m q = m' q \<and> (m q = m' q \<longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src\<rbrakk> \<Longrightarrow> next_sib src_p t m \<noteq> Some src
 2. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src\<rbrakk> \<Longrightarrow> \<forall>q. src_p \<in> descendants_of q m \<longrightarrow> m q = m' q \<and> (m q = m' q \<longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; next_sib src_p t m = Some src\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src\<rbrakk> \<Longrightarrow> \<forall>q. src_p \<in> descendants_of q m \<longrightarrow> m q = m' q \<and> (m q = m' q \<longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src\<rbrakk> \<Longrightarrow> \<forall>q. src_p \<in> descendants_of q m \<longrightarrow> m q = m' q \<and> (m q = m' q \<longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m') proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m\<rbrakk> \<Longrightarrow> m q = m' q
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m\<rbrakk> \<Longrightarrow> q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> m q \<noteq> Some src))
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (4 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m\<rbrakk> \<Longrightarrow> q \<noteq> dest
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest\<rbrakk> \<Longrightarrow> q \<noteq> src
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src\<rbrakk> \<Longrightarrow> m q \<noteq> Some src
 4. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (4 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest\<rbrakk> \<Longrightarrow> q \<noteq> src
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src\<rbrakk> \<Longrightarrow> m q \<noteq> Some src
 4. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (4 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of dest m; q = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest\<rbrakk> \<Longrightarrow> q \<noteq> src
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src\<rbrakk> \<Longrightarrow> m q \<noteq> Some src
 4. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest\<rbrakk> \<Longrightarrow> q \<noteq> src
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src\<rbrakk> \<Longrightarrow> m q \<noteq> Some src
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> False
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src\<rbrakk> \<Longrightarrow> m q \<noteq> Some src
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of src m; q = src\<rbrakk> \<Longrightarrow> False
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src\<rbrakk> \<Longrightarrow> m q \<noteq> Some src
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src\<rbrakk> \<Longrightarrow> m q \<noteq> Some src
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src\<rbrakk> \<Longrightarrow> False
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src; q \<in> descendants_of src_p m\<rbrakk> \<Longrightarrow> False
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src\<rbrakk> \<Longrightarrow> q \<in> descendants_of src_p m
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src\<rbrakk> \<Longrightarrow> q \<in> descendants_of src_p m
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src\<rbrakk> \<Longrightarrow> q \<in> descendants_of (?b53 q) m
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src\<rbrakk> \<Longrightarrow> ?b53 q \<in> descendants_of src_p m
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src\<rbrakk> \<Longrightarrow> m q = Some (?b53 q)
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src\<rbrakk> \<Longrightarrow> ?b53 q \<in> descendants_of src_p m
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src\<rbrakk> \<Longrightarrow> src \<in> descendants_of src_p m
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; q \<noteq> dest; q \<noteq> src; m q = Some src\<rbrakk> \<Longrightarrow> m src = Some src_p
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src; m src = Some src_p \<Longrightarrow> src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> next_sib q t m = next_sib q (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q\<rbrakk> \<Longrightarrow> (next_sib q t m = Some src \<longrightarrow> (q = dest \<longrightarrow> next_sib dest t m = next_sib src t m) \<and> (q \<noteq> dest \<longrightarrow> (q = src \<longrightarrow> next_sib src t m = None) \<and> q = src)) \<and> (next_sib q t m \<noteq> Some src \<longrightarrow> (q = dest \<longrightarrow> next_sib dest t m = next_sib src t m) \<and> (q \<noteq> dest \<longrightarrow> q = src \<longrightarrow> next_sib src t m = None)) proof (prove)
goal (5 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m = Some src; q = dest\<rbrakk> \<Longrightarrow> next_sib dest t m = next_sib src t m
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m = Some src; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> next_sib src t m = None
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m = Some src; q \<noteq> dest\<rbrakk> \<Longrightarrow> q = src
 4. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m \<noteq> Some src; q = dest\<rbrakk> \<Longrightarrow> next_sib dest t m = next_sib src t m
 5. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m \<noteq> Some src; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> next_sib src t m = None proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m = Some src; q \<noteq> dest\<rbrakk> \<Longrightarrow> q = src
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m \<noteq> Some src; q = dest\<rbrakk> \<Longrightarrow> next_sib dest t m = next_sib src t m
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m \<noteq> Some src; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> next_sib src t m = None proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = Some src_p; next_sib q t m = Some src; q \<noteq> dest; m' q = Some src_p\<rbrakk> \<Longrightarrow> q = src
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m \<noteq> Some src; q = dest\<rbrakk> \<Longrightarrow> next_sib dest t m = next_sib src t m
 3. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m \<noteq> Some src; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> next_sib src t m = None proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m \<noteq> Some src; q = dest\<rbrakk> \<Longrightarrow> next_sib dest t m = next_sib src t m
 2. \<And>q. \<lbrakk>valid_list_2 t m; m src = Some src_p; src_p \<noteq> dest; m src_p \<noteq> Some src; src_p \<noteq> src; src_p \<in> descendants_of q m; m q = m' q; next_sib q t m \<noteq> Some src; q \<noteq> dest; q = src\<rbrakk> \<Longrightarrow> next_sib src t m = None proof (prove)
goal:
No subgoals!