theory CSpace1_R

lemma n_next:
  "n p = Some (CTE cap node) \<Longrightarrow>
  if p = dest then
    (if mdbNext src_node = dest then mdbNext node = src
    else mdbNext node = mdbNext src_node)
  else if p = src then
    (if mdbNext dest_node = src then mdbNext node = dest
    else mdbNext node = mdbNext dest_node)
  else if p = mdbPrev src_node then mdbNext node = dest
  else if p = mdbPrev dest_node then mdbNext node = src
  else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node'" apply (simp add: n_def del: dest2_parts split del: if_split) apply (simp only: dest2_next dest2_prev split del: if_split) apply (simp add: dest2_node_def split del: if_split) apply (simp add: n'_def const_def cong: if_cong split del: if_split) apply(case_tac "p=dest") apply(clarsimp simp: modify_map_cases const_def split: if_split_asm) apply(case_tac "p=src") apply(simp split del: if_split) apply(clarsimp simp: modify_map_cases const_def split: if_split_asm) apply(case_tac "p=mdbPrev src_node") apply(simp split del: if_split) apply(clarsimp simp: modify_map_cases const_def split: if_split_asm) apply(fastforce) apply(fastforce) apply(case_tac "p=mdbPrev dest_node") apply(simp split del: if_split) apply(clarsimp simp: modify_map_cases const_def split: if_split_asm) apply(fastforce) apply(simp split del: if_split) apply (clarsimp simp: modify_map_cases const_def split: if_split_asm) apply(fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some (CTE cap node) \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbNext dest_node = src then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map n' 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))) p = Some (CTE cap node) \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map n' 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))) p = Some (CTE cap node) \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map n' src (cteMDBNode_update (const (MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node))))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node) \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. 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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node) \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p = dest\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node'
 2. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node'
 2. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) src = Some (CTE cap node); p = src\<rbrakk> \<Longrightarrow> if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node
 2. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node'
 2. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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 (\<lambda>y. MDB (mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) (mdbPrev src_node) = Some (CTE cap node); mdbPrev src_node \<noteq> dest; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> mdbNext node = dest
 2. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0; p = mdbPrev src_node; dest = mdbNext src_node; mdbNext dest_node \<noteq> mdbPrev src_node \<longrightarrow> (\<exists>nodea. m (mdbPrev src_node) = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. mdbNext src_node) nodea = node); mdbNext dest_node = mdbPrev src_node \<longrightarrow> (\<exists>nodea. (\<exists>node. m (mdbPrev src_node) = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. mdbNext src_node) node = nodea) \<and> mdbPrev_update (\<lambda>_. src) nodea = node)\<rbrakk> \<Longrightarrow> mdbNext node = mdbNext src_node
 2. \<lbrakk>mdbPrev src_node \<noteq> dest; p = mdbPrev src_node; dest \<noteq> mdbNext src_node; mdbNext dest_node \<noteq> mdbPrev src_node \<longrightarrow> ((mdbPrev dest_node = 0 \<longrightarrow> mdbPrev src_node \<noteq> 0) \<longrightarrow> ((mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (\<exists>nodea. m (mdbPrev src_node) = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)) \<and> (mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0)) \<and> (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node = 0 \<and> mdbNext src_node \<noteq> 0 \<and> (\<exists>nodea. mdbNext_update (\<lambda>_. src) nodea = node)); mdbNext dest_node = mdbPrev src_node \<longrightarrow> (\<exists>nodea. ((mdbPrev dest_node = 0 \<longrightarrow> mdbPrev src_node \<noteq> 0) \<longrightarrow> ((mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (\<exists>node. m (mdbPrev src_node) = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea)) \<and> (mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0)) \<and> (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node = 0 \<and> mdbNext src_node \<noteq> 0 \<and> (\<exists>node. mdbNext_update (\<lambda>_. src) node = nodea)) \<and> mdbPrev_update (\<lambda>_. src) nodea = node)\<rbrakk> \<Longrightarrow> mdbNext node = dest
 3. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbPrev src_node \<noteq> dest; p = mdbPrev src_node; dest \<noteq> mdbNext src_node; mdbNext dest_node \<noteq> mdbPrev src_node \<longrightarrow> ((mdbPrev dest_node = 0 \<longrightarrow> mdbPrev src_node \<noteq> 0) \<longrightarrow> ((mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (\<exists>nodea. m (mdbPrev src_node) = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)) \<and> (mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0)) \<and> (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node = 0 \<and> mdbNext src_node \<noteq> 0 \<and> (\<exists>nodea. mdbNext_update (\<lambda>_. src) nodea = node)); mdbNext dest_node = mdbPrev src_node \<longrightarrow> (\<exists>nodea. ((mdbPrev dest_node = 0 \<longrightarrow> mdbPrev src_node \<noteq> 0) \<longrightarrow> ((mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (\<exists>node. m (mdbPrev src_node) = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea)) \<and> (mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0)) \<and> (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node = 0 \<and> mdbNext src_node \<noteq> 0 \<and> (\<exists>node. mdbNext_update (\<lambda>_. src) node = nodea)) \<and> mdbPrev_update (\<lambda>_. src) nodea = node)\<rbrakk> \<Longrightarrow> mdbNext node = dest
 2. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node; p = mdbPrev dest_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node'
 2. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node; p \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) (mdbPrev dest_node) = Some (CTE cap node); mdbNext src_node \<noteq> dest; mdbPrev dest_node = 0 \<longrightarrow> mdbPrev src_node \<noteq> 0; p = mdbPrev dest_node\<rbrakk> \<Longrightarrow> if mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0 then mdbNext node = dest else mdbNext node = src
 2. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node; p \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext src_node \<noteq> dest; mdbPrev dest_node = 0 \<longrightarrow> mdbPrev src_node \<noteq> 0; p = mdbPrev dest_node; dest \<noteq> mdbPrev src_node; (mdbPrev dest_node = 0 \<longrightarrow> mdbNext dest_node \<noteq> 0) \<longrightarrow> (\<exists>nodea. (mdbNext src_node \<noteq> mdbPrev dest_node \<longrightarrow> m (mdbPrev dest_node) = Some (CTE cap nodea)) \<and> (mdbNext src_node = mdbPrev dest_node \<longrightarrow> (\<exists>node. m (mdbPrev dest_node) = Some (CTE cap node) \<and> mdbPrev_update (\<lambda>_. dest) node = nodea)) \<and> mdbNext_update (\<lambda>_. src) nodea = node); mdbPrev dest_node = 0 \<and> mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node = 0 \<and> mdbNext src_node \<noteq> 0 \<and> (\<exists>nodea. (\<exists>node. mdbNext_update (\<lambda>_. src) node = nodea) \<and> mdbPrev_update (\<lambda>_. src) nodea = node)\<rbrakk> \<Longrightarrow> (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0 \<longrightarrow> mdbNext node = dest) \<and> mdbNext node = src
 2. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node; p \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node; p \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> if p = dest then if mdbNext src_node = dest then mdbNext node = src else mdbNext node = mdbNext src_node else if p = src then if mdbPrev src_node = dest then mdbNext node = dest else mdbNext node = mdbNext dest_node else if p = mdbPrev src_node then mdbNext node = dest else if p = mdbPrev dest_node then mdbNext node = src else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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 (\<lambda>y. MDB (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)))) dest (cteMDBNode_update (\<lambda>y. src_node))) (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node; p \<noteq> mdbPrev dest_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<noteq> src; p \<noteq> mdbPrev src_node; p \<noteq> mdbPrev dest_node; dest = mdbPrev src_node; mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0; mdbNext src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node); mdbNext src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbPrev_update (\<lambda>_. mdbPrev src_node) nodea = node)\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node'
 2. \<lbrakk>p \<noteq> mdbNext src_node; p \<noteq> src; p \<noteq> mdbPrev src_node; p \<noteq> mdbPrev dest_node; mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0; dest = mdbNext src_node; mdbNext dest_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node); mdbNext dest_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbPrev_update (\<lambda>_. src) nodea = node)\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node'
 3. \<lbrakk>p \<noteq> dest; p \<noteq> src; p \<noteq> mdbPrev src_node; p \<noteq> mdbPrev dest_node; dest \<noteq> mdbPrev src_node; dest \<noteq> mdbNext src_node; mdbNext dest_node \<noteq> p \<longrightarrow> (mdbNext src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node)); mdbNext dest_node = p \<longrightarrow> (\<exists>nodea. (mdbNext src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbPrev_update (\<lambda>_. dest) node = nodea)) \<and> mdbPrev_update (\<lambda>_. src) nodea = node)\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal:
No subgoals!