theory CSpace1_R

lemma valid_dlist_preserve_oneway:
  assumes dom:"\<And>x. (x \<in> dom m) = (x \<in> dom m')"
  assumes misc:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte'"
  shows  "valid_dlist m \<Longrightarrow> valid_dlist m'" apply (clarsimp simp:valid_dlist_def Let_def) apply (frule domI[where m = m'],drule iffD2[OF dom],erule domE) apply (elim allE impE) apply assumption apply (intro conjI impI) apply clarsimp apply (frule(1) misc) apply (clarsimp) apply (frule_tac b = cte' in domI[where m = m]) apply (drule iffD1[OF dom]) apply clarsimp apply (drule(1) misc)+ apply simp apply clarsimp apply (frule(1) misc) apply (clarsimp) apply (frule_tac b = cte' in domI[where m = m]) apply (drule iffD1[OF dom]) apply clarsimp apply (drule(1) misc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist m \<Longrightarrow> valid_dlist m' proof (prove)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>\<forall>p cte. m p = Some cte \<longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); m' p = Some cte\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m' (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)) proof (prove)
goal (1 subgoal):
 1. \<And>p cte r. \<lbrakk>\<forall>p cte. m p = Some cte \<longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); m' p = Some cte; m p = Some r\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m' (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)) proof (prove)
goal (2 subgoals):
 1. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r\<rbrakk> \<Longrightarrow> m (?p12 p cte r) = Some (?cte13 p cte r)
 2. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode (?cte13 p cte r)) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode (?cte13 p cte r))) = Some cte' \<and> mdbNext (cteMDBNode cte') = ?p12 p cte r)) \<and> (mdbNext (cteMDBNode (?cte13 p cte r)) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode (?cte13 p cte r))) = Some cte' \<and> mdbPrev (cteMDBNode cte') = ?p12 p cte r))\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m' (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)) proof (prove)
goal (1 subgoal):
 1. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p))\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m' (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)) proof (prove)
goal (2 subgoals):
 1. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p); mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p); mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p); cteMDBNode r = cteMDBNode cte\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>cte r cte'. \<lbrakk>m' (mdbNext (cteMDBNode cte')) = Some cte; m (mdbNext (cteMDBNode cte')) = Some r; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbNext (cteMDBNode cte)) = Some cte'a \<and> mdbPrev (cteMDBNode cte'a) = mdbNext (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m (mdbPrev (cteMDBNode cte)) = Some cte'\<rbrakk> \<Longrightarrow> \<exists>cte'a. m' (mdbPrev (cteMDBNode cte)) = Some cte'a \<and> mdbNext (cteMDBNode cte'a) = mdbNext (cteMDBNode cte')
 2. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>cte r cte'. \<lbrakk>m' (mdbNext (cteMDBNode cte')) = Some cte; m (mdbNext (cteMDBNode cte')) = Some r; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbNext (cteMDBNode cte)) = Some cte'a \<and> mdbPrev (cteMDBNode cte'a) = mdbNext (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m (mdbPrev (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte) \<in> dom m\<rbrakk> \<Longrightarrow> \<exists>cte'a. m' (mdbPrev (cteMDBNode cte)) = Some cte'a \<and> mdbNext (cteMDBNode cte'a) = mdbNext (cteMDBNode cte')
 2. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>cte r cte'. \<lbrakk>m' (mdbNext (cteMDBNode cte')) = Some cte; m (mdbNext (cteMDBNode cte')) = Some r; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbNext (cteMDBNode cte)) = Some cte'a \<and> mdbPrev (cteMDBNode cte'a) = mdbNext (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m (mdbPrev (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte) \<in> dom m'\<rbrakk> \<Longrightarrow> \<exists>cte'a. m' (mdbPrev (cteMDBNode cte)) = Some cte'a \<and> mdbNext (cteMDBNode cte'a) = mdbNext (cteMDBNode cte')
 2. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>cte r cte' y. \<lbrakk>m' (mdbNext (cteMDBNode cte')) = Some cte; m (mdbNext (cteMDBNode cte')) = Some r; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbNext (cteMDBNode cte)) = Some cte'a \<and> mdbPrev (cteMDBNode cte'a) = mdbNext (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m (mdbPrev (cteMDBNode cte)) = Some cte'; m' (mdbPrev (cteMDBNode cte)) = Some y\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode y) = mdbNext (cteMDBNode cte')
 2. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>cte r cte' y. \<lbrakk>m' (mdbNext (cteMDBNode cte')) = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbNext (cteMDBNode cte)) = Some cte'a \<and> mdbPrev (cteMDBNode cte'a) = mdbNext (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m' (mdbPrev (cteMDBNode cte)) = Some y; cteMDBNode r = cteMDBNode cte; cteMDBNode cte' = cteMDBNode y\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode y) = mdbNext (cteMDBNode cte')
 2. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (1 subgoal):
 1. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; (mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (1 subgoal):
 1. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p); mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (1 subgoal):
 1. \<And>p cte r. \<lbrakk>m' p = Some cte; m p = Some r; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode r)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p); mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode r)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p); cteMDBNode r = cteMDBNode cte\<rbrakk> \<Longrightarrow> \<exists>cte'. m' (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (1 subgoal):
 1. \<And>cte r cte'. \<lbrakk>m' (mdbPrev (cteMDBNode cte')) = Some cte; m (mdbPrev (cteMDBNode cte')) = Some r; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbPrev (cteMDBNode cte)) = Some cte'a \<and> mdbNext (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m (mdbNext (cteMDBNode cte)) = Some cte'\<rbrakk> \<Longrightarrow> \<exists>cte'a. m' (mdbNext (cteMDBNode cte)) = Some cte'a \<and> mdbPrev (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte') proof (prove)
goal (1 subgoal):
 1. \<And>cte r cte'. \<lbrakk>m' (mdbPrev (cteMDBNode cte')) = Some cte; m (mdbPrev (cteMDBNode cte')) = Some r; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbPrev (cteMDBNode cte)) = Some cte'a \<and> mdbNext (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m (mdbNext (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode cte) \<in> dom m\<rbrakk> \<Longrightarrow> \<exists>cte'a. m' (mdbNext (cteMDBNode cte)) = Some cte'a \<and> mdbPrev (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte') proof (prove)
goal (1 subgoal):
 1. \<And>cte r cte'. \<lbrakk>m' (mdbPrev (cteMDBNode cte')) = Some cte; m (mdbPrev (cteMDBNode cte')) = Some r; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbPrev (cteMDBNode cte)) = Some cte'a \<and> mdbNext (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m (mdbNext (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode cte) \<in> dom m'\<rbrakk> \<Longrightarrow> \<exists>cte'a. m' (mdbNext (cteMDBNode cte)) = Some cte'a \<and> mdbPrev (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte') proof (prove)
goal (1 subgoal):
 1. \<And>cte r cte' y. \<lbrakk>m' (mdbPrev (cteMDBNode cte')) = Some cte; m (mdbPrev (cteMDBNode cte')) = Some r; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbPrev (cteMDBNode cte)) = Some cte'a \<and> mdbNext (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m (mdbNext (cteMDBNode cte)) = Some cte'; m' (mdbNext (cteMDBNode cte)) = Some y\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode y) = mdbPrev (cteMDBNode cte') proof (prove)
goal (1 subgoal):
 1. \<And>cte r cte' y. \<lbrakk>m' (mdbPrev (cteMDBNode cte')) = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'a. m (mdbPrev (cteMDBNode cte)) = Some cte'a \<and> mdbNext (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte')); cteMDBNode r = cteMDBNode cte; m' (mdbNext (cteMDBNode cte)) = Some y; cteMDBNode r = cteMDBNode cte; cteMDBNode cte' = cteMDBNode y\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode y) = mdbPrev (cteMDBNode cte') proof (prove)
goal:
No subgoals!