theory CNodeInv_R

lemma (in mdb_swap) n_dest_prev:
  assumes md: "m (mdbPrev dest_node) = Some cte"
  shows "\<exists>cte'. n (mdbPrev dest_node) = Some cte'
  \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src)
  \<and> mdbPrev (cteMDBNode cte') =
  (if (mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node) then dest else
  mdbPrev (cteMDBNode cte))" proof - have nz: "(mdbPrev dest_node) \<noteq> 0" using md by (rule dom_into_not0 [OF no_0 domI]) show ?thesis proof (cases rule: cases2 [of "dest = mdbNext src_node"  "mdbNext src_node = mdbPrev dest_node"]) case pos_pos thus ?thesis by simp next case neg_pos thus ?thesis using nz md unfolding n_def n'_def apply (simp only: dest2_next dest2_prev) apply (clarsimp simp add: modify_map_same modify_map_other) done next case pos_neg hence "(mdbPrev dest_node) = src" by simp thus ?thesis using pos_neg md p_0 unfolding n_def n'_def apply (simp only: dest2_next dest2_prev) apply (simp add: modify_map_same modify_map_other del: dest2_parts ) apply (simp only: next_unfold' dest2_next dest2_prev) apply (subst if_not_P) apply simp+ done next case neg_neg thus ?thesis using md nz unfolding n_def n'_def apply (simp only: dest2_next dest2_prev) apply (clarsimp simp add: modify_map_same modify_map_other) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
goal (1 subgoal):
 1. mdbPrev dest_node \<noteq> 0 proof (prove)
using this:
m (mdbPrev dest_node) = Some cte

goal (1 subgoal):
 1. mdbPrev dest_node \<noteq> 0 proof (state)
this:
mdbPrev dest_node \<noteq> 0

goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
goal (4 subgoals):
 1. \<lbrakk>dest = mdbNext src_node; mdbNext src_node = mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 2. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node = mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 3. \<lbrakk>dest = mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 4. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
this:
dest = mdbNext src_node
mdbNext src_node = mdbPrev dest_node

goal (4 subgoals):
 1. \<lbrakk>dest = mdbNext src_node; mdbNext src_node = mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 2. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node = mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 3. \<lbrakk>dest = mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 4. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
dest = mdbNext src_node
mdbNext src_node = mdbPrev dest_node

goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
this:
\<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))

goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node = mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 2. \<lbrakk>dest = mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 3. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node = mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 2. \<lbrakk>dest = mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 3. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
this:
dest \<noteq> mdbNext src_node
mdbNext src_node = mdbPrev dest_node

goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node = mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 2. \<lbrakk>dest = mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 3. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
dest \<noteq> mdbNext src_node
mdbNext src_node = mdbPrev dest_node

goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
dest \<noteq> mdbNext src_node
mdbNext src_node = mdbPrev dest_node
mdbPrev dest_node \<noteq> 0
m (mdbPrev dest_node) = Some cte

goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
dest \<noteq> mdbNext src_node
mdbNext src_node = mdbPrev dest_node
mdbPrev dest_node \<noteq> 0
m (mdbPrev dest_node) = Some cte

goal (1 subgoal):
 1. \<exists>cte'. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (mdbPrev (cteMDBNode dest2)) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext (cteMDBNode dest2)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dest \<noteq> mdbPrev dest_node; mdbNext src_node = mdbPrev dest_node; mdbPrev dest_node \<noteq> 0; m (mdbPrev dest_node) = Some cte\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbPrev dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if False then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if False then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbPrev dest_node = mdbPrev dest_node \<or> False then dest else mdbPrev (cteMDBNode cte)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))

goal (2 subgoals):
 1. \<lbrakk>dest = mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 2. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
goal (2 subgoals):
 1. \<lbrakk>dest = mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 2. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
this:
dest = mdbNext src_node
mdbNext src_node \<noteq> mdbPrev dest_node

goal (2 subgoals):
 1. \<lbrakk>dest = mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 2. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
dest = mdbNext src_node
mdbNext src_node \<noteq> mdbPrev dest_node

goal (1 subgoal):
 1. mdbPrev dest_node = src proof (state)
this:
mdbPrev dest_node = src

goal (2 subgoals):
 1. \<lbrakk>dest = mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))
 2. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
mdbPrev dest_node = src

goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
mdbPrev dest_node = src
dest = mdbNext src_node
mdbNext src_node \<noteq> mdbPrev dest_node
m (mdbPrev dest_node) = Some cte
dest \<noteq> 0

goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
mdbPrev dest_node = src
dest = mdbNext src_node
mdbNext src_node \<noteq> mdbPrev dest_node
m (mdbPrev dest_node) = Some cte
dest \<noteq> 0

goal (1 subgoal):
 1. \<exists>cte'. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (mdbPrev (cteMDBNode dest2)) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext (cteMDBNode dest2)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev dest_node = src; dest = mdbNext src_node; mdbNext src_node \<noteq> src; m src = Some cte; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) (mdbNext src_node) (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext src_node)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbNext src_node)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) (mdbNext src_node) (cteMDBNode_update (const src_node))) (if mdbNext src_node = mdbNext src_node then mdbNext src_node else src) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if mdbNext src_node = mdbPrev src_node then mdbNext src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) src = Some cte' \<and> mdbNext (cteMDBNode cte') = (if mdbNext src_node = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if False \<or> mdbNext src_node = mdbNext src_node then mdbNext src_node else mdbPrev (cteMDBNode cte)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dest = mdbNext src_node; m src = Some cte; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode dest2) = mdbNext dest_node \<and> mdbPrev (cteMDBNode dest2) = mdbNext src_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dest = mdbNext src_node; m src = Some cte; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> (if mdbNext src_node = mdbPrev src_node then mdbNext src_node else mdbNext dest_node) = mdbNext dest_node \<and> (if mdbNext src_node = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) = mdbNext src_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dest = mdbNext src_node; m src = Some cte; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> mdbPrev src_node
 2. \<lbrakk>dest = mdbNext src_node; m src = Some cte; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext dest_node = mdbNext dest_node \<and> (if mdbNext src_node = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) = mdbNext src_node proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))

goal (1 subgoal):
 1. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
goal (1 subgoal):
 1. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (state)
this:
dest \<noteq> mdbNext src_node
mdbNext src_node \<noteq> mdbPrev dest_node

goal (1 subgoal):
 1. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
dest \<noteq> mdbNext src_node
mdbNext src_node \<noteq> mdbPrev dest_node

goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
dest \<noteq> mdbNext src_node
mdbNext src_node \<noteq> mdbPrev dest_node
m (mdbPrev dest_node) = Some cte
mdbPrev dest_node \<noteq> 0

goal (1 subgoal):
 1. \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
using this:
dest \<noteq> mdbNext src_node
mdbNext src_node \<noteq> mdbPrev dest_node
m (mdbPrev dest_node) = Some cte
mdbPrev dest_node \<noteq> 0

goal (1 subgoal):
 1. \<exists>cte'. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (mdbPrev (cteMDBNode dest2)) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext (cteMDBNode dest2)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dest \<noteq> mdbNext src_node; mdbNext src_node \<noteq> mdbPrev dest_node; m (mdbPrev dest_node) = Some cte; mdbPrev dest_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if False then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if False then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if False \<or> False then dest else mdbPrev (cteMDBNode cte)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))

goal:
No subgoals! proof (state)
this:
\<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode cte))

goal:
No subgoals!