theory CNodeInv_R

lemma (in mdb_swap) n_dest_next:
  assumes md: "m (mdbNext dest_node) = Some cte"
  shows "\<exists>cte'. n (mdbNext dest_node) = Some cte'
  \<and> mdbNext (cteMDBNode cte') = (if (src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node) then dest else mdbNext (cteMDBNode cte))
  \<and> mdbPrev (cteMDBNode cte') =  (if src = mdbNext dest_node then mdbPrev dest_node else src)" proof - have nz: "(mdbNext dest_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) apply (clarsimp simp add: modify_map_same modify_map_other) done 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 next_fold a 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) apply (simp add: modify_map_same modify_map_other del: dest2_parts ) apply (simp only: dest2_next dest2_prev) apply (subst if_P [OF refl]) 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 (mdbNext dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src) proof (state)
goal (1 subgoal):
 1. \<exists>cte'. n (mdbNext dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src) proof (prove)
goal (1 subgoal):
 1. mdbNext dest_node \<noteq> 0 proof (prove)
using this:
m (mdbNext dest_node) = Some cte

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

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

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

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

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

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

goal (2 subgoals):
 1. \<lbrakk>src = mdbNext dest_node; mdbNext dest_node \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbNext dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src)
 2. \<lbrakk>src \<noteq> mdbNext dest_node; mdbNext dest_node \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbNext dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src) proof (state)
goal (2 subgoals):
 1. \<lbrakk>src = mdbNext dest_node; mdbNext dest_node \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbNext dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src)
 2. \<lbrakk>src \<noteq> mdbNext dest_node; mdbNext dest_node \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbNext dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src) 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 dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src)
 2. \<lbrakk>src \<noteq> mdbNext dest_node; mdbNext dest_node \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbNext dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src) 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 dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src)
 2. \<lbrakk>src \<noteq> mdbNext dest_node; mdbNext dest_node \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>cte'. n (mdbNext dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode cte)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src) 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)
\<lbrakk>?m ?a = Some ?cte; mdbNext (cteMDBNode ?cte) = ?b\<rbrakk> \<Longrightarrow> ?m \<turnstile> ?a \<leadsto> ?b
mdbNext src_node = dest

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

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

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

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

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

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

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

goal:
No subgoals!