theory CNodeInv_R

lemma (in mdb_swap) n_src_next:
  assumes md: "m (mdbNext src_node) = Some cte"
  shows "\<exists>cte'. n (mdbNext src_node) = Some cte'
  \<and> mdbNext (cteMDBNode cte') = (if (dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node) then src else mdbNext (cteMDBNode cte))
  \<and> mdbPrev (cteMDBNode cte') =  (if dest = mdbNext src_node then mdbPrev src_node else dest)" proof - have nz: "(mdbNext src_node) \<noteq> 0" using md by (rule dom_into_not0 [OF no_0 domI]) show ?thesis proof (cases rule: cases2 [of "src = mdbNext dest_node"  "mdbNext dest_node = mdbPrev src_node"]) case pos_pos thus ?thesis by simp next case neg_pos hence "(mdbPrev src_node) \<noteq> dest" by - (rule, simp add: next_dest_prev_src_sym) thus ?thesis using nz md neg_pos unfolding n_def n'_def apply (simp only: dest2_next dest2_prev) by (clarsimp simp add: modify_map_same modify_map_other) next case pos_neg hence pd: "mdbPrev src_node = dest" by simp have "mdbNext src_node \<noteq> dest" proof assume a: "mdbNext src_node = dest" from pd have "mdbPrev src_node \<noteq> 0" by simp hence "m \<turnstile> mdbPrev src_node \<leadsto> src" .. also have "m \<turnstile> src \<leadsto> dest" using src using a next_fold by auto finally show False using pd by simp qed thus ?thesis using md p_0 pd pos_neg nz unfolding n_def n'_def apply (simp only: dest2_next dest2_prev) by (clarsimp simp add: modify_map_same modify_map_other del: dest2_parts ) next case neg_neg thus ?thesis using md nz unfolding n_def n'_def apply (simp only: dest2_next dest2_prev) by (clarsimp simp add: modify_map_same modify_map_other) qed qed

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

goal (1 subgoal):
 1. mdbNext src_node \<noteq> 0 proof (state)
this:
mdbNext src_node \<noteq> 0

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

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

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

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

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

goal (1 subgoal):
 1. mdbPrev src_node \<noteq> dest proof (state)
this:
mdbPrev src_node \<noteq> dest

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

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

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

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))) (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev src_node \<noteq> dest; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some cte; src \<noteq> mdbPrev src_node; mdbNext dest_node = mdbPrev src_node\<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 dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbPrev src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest) proof (state)
this:
\<exists>cte'. n (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest)

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

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

goal (1 subgoal):
 1. mdbPrev src_node = dest proof (state)
this:
mdbPrev src_node = dest

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

goal (1 subgoal):
 1. mdbNext src_node = dest \<Longrightarrow> False proof (chain)
picking this:
mdbPrev src_node = dest proof (prove)
using this:
mdbPrev src_node = dest

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

goal (1 subgoal):
 1. mdbNext src_node = dest \<Longrightarrow> False proof (prove)
using this:
mdbPrev src_node \<noteq> 0

goal (1 subgoal):
 1. m \<turnstile> mdbPrev src_node \<leadsto> src proof (state)
this:
m \<turnstile> mdbPrev src_node \<leadsto> src

goal (1 subgoal):
 1. mdbNext src_node = dest \<Longrightarrow> False proof (state)
this:
m \<turnstile> mdbPrev src_node \<leadsto> src

goal (1 subgoal):
 1. mdbNext src_node = dest \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> dest proof (prove)
using this:
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> dest proof (prove)
using this:
m src = Some (CTE src_cap src_node)
mdbNext src_node = dest
\<lbrakk>?m ?a = Some ?cte; mdbNext (cteMDBNode ?cte) = ?b\<rbrakk> \<Longrightarrow> ?m \<turnstile> ?a \<leadsto> ?b

goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> dest proof (state)
this:
m \<turnstile> src \<leadsto> dest

goal (1 subgoal):
 1. mdbNext src_node = dest \<Longrightarrow> False proof (chain)
picking this:
m \<turnstile> mdbPrev src_node \<leadsto>\<^sup>+ dest proof (prove)
using this:
m \<turnstile> mdbPrev src_node \<leadsto>\<^sup>+ dest

goal (1 subgoal):
 1. False proof (prove)
using this:
m \<turnstile> mdbPrev src_node \<leadsto>\<^sup>+ dest
mdbPrev src_node = dest

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals! proof (state)
this:
mdbNext src_node \<noteq> dest

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

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

goal (1 subgoal):
 1. \<exists>cte'. n (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest) proof (prove)
using this:
mdbNext src_node \<noteq> dest
m (mdbNext src_node) = Some cte
dest \<noteq> 0
mdbPrev src_node = dest
src = mdbNext dest_node
mdbNext dest_node \<noteq> mdbPrev src_node
mdbNext src_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))) (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext src_node \<noteq> dest; m (mdbNext src_node) = Some cte; dest \<noteq> 0; mdbPrev src_node = dest; src = mdbNext dest_node; mdbNext dest_node \<noteq> dest; 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 (mdbNext dest_node) (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) dest (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) (mdbNext dest_node) (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext dest_node)))) (if dest = dest then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbNext dest_node))) (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then mdbNext dest_node else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then dest else dest) proof (state)
this:
\<exists>cte'. n (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest)

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

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

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

goal (1 subgoal):
 1. \<exists>cte'. n (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest) proof (prove)
using this:
src \<noteq> mdbNext dest_node
mdbNext dest_node \<noteq> mdbPrev src_node
m (mdbNext src_node) = Some cte
mdbNext src_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))) (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src \<noteq> mdbNext dest_node; mdbNext dest_node \<noteq> mdbPrev src_node; m (mdbNext src_node) = 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))) 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 dest = mdbNext src_node 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))) (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest) proof (state)
this:
\<exists>cte'. n (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest)

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

goal:
No subgoals!