theory CNodeInv_R

lemma (in mdb_swap) n_cap_eq':
  "(\<exists>n'. n p = Some (CTE cap n')) =
   (if p = src
    then cap = dcap
    else if p = dest
    then cap = scap
    else \<exists>n'. m p = Some (CTE cap n'))" using src dest apply simp apply (rule conjI, clarsimp) apply (rule iffI) apply (fastforce dest: n_cap) subgoal by (simp add: n_def modify_map_if dest2_node_def n'_def, auto) apply clarsimp apply (rule conjI, fastforce) apply clarsimp apply (rule iffI) apply (fastforce dest: n_cap) apply (simp add: n_def modify_map_cases n'_def) apply (simp add: dest2_node_def) apply auto[1] apply (cases "mdbNext dest_node = 0") apply (cases "mdbNext src_node = 0") apply simp apply simp apply (cases "mdbPrev dest_node = mdbNext src_node") apply simp apply simp apply simp apply (cases "mdbPrev dest_node = mdbNext src_node") apply simp apply simp apply (cases "mdbNext dest_node = p") apply simp apply fastforce apply simp apply (cases "mdbPrev dest_node = p") apply simp apply simp apply (cases "mdbNext dest_node = p") apply simp apply (cases "mdbPrev dest_node = p") apply simp apply fastforce apply simp apply (cases "mdbPrev src_node = p", simp) apply simp apply simp apply (cases "mdbPrev dest_node = p", simp) apply fastforce apply simp apply (cases "mdbPrev src_node = p", simp) apply simp apply (cases "mdbNext dest_node = p") apply simp apply (cases "mdbPrev dest_node = p") apply simp apply fastforce apply simp apply (cases "mdbPrev src_node = p", simp) apply simp apply simp apply (cases "mdbPrev dest_node = p", simp) apply fastforce apply simp apply (cases "mdbPrev src_node = p", simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>n'. n p = Some (CTE cap n')) = (if p = src then cap = dcap else if p = dest then cap = scap else \<exists>n'. m p = Some (CTE cap n')) proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. (\<exists>n'. n p = Some (CTE cap n')) = (if p = src then cap = dcap else if p = dest then cap = scap else \<exists>n'. m p = Some (CTE cap n')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> (\<exists>n'. n dest = Some (CTE cap n')) = (cap = scap)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (dcap = cap) = (cap = dcap)) \<and> (p \<noteq> src \<longrightarrow> (\<exists>n'. n p = Some (CTE cap n')) = (\<exists>n'. m p = Some (CTE cap n')))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p = dest\<rbrakk> \<Longrightarrow> (\<exists>n'. n dest = Some (CTE cap n')) = (cap = scap)
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (dcap = cap) = (cap = dcap)) \<and> (p \<noteq> src \<longrightarrow> (\<exists>n'. n p = Some (CTE cap n')) = (\<exists>n'. m p = Some (CTE cap n'))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p = dest; \<exists>n'. n dest = Some (CTE cap n')\<rbrakk> \<Longrightarrow> cap = scap
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p = dest; cap = scap\<rbrakk> \<Longrightarrow> \<exists>n'. n dest = Some (CTE cap n')
 3. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (dcap = cap) = (cap = dcap)) \<and> (p \<noteq> src \<longrightarrow> (\<exists>n'. n p = Some (CTE cap n')) = (\<exists>n'. m p = Some (CTE cap n'))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p = dest; cap = scap\<rbrakk> \<Longrightarrow> \<exists>n'. n dest = Some (CTE cap n')
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (dcap = cap) = (cap = dcap)) \<and> (p \<noteq> src \<longrightarrow> (\<exists>n'. n p = Some (CTE cap n')) = (\<exists>n'. m p = Some (CTE cap n'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p = dest; cap = scap\<rbrakk> \<Longrightarrow> \<exists>n'. n dest = Some (CTE cap n') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (dcap = cap) = (cap = dcap)) \<and> (p \<noteq> src \<longrightarrow> (\<exists>n'. n p = Some (CTE cap n')) = (\<exists>n'. m p = Some (CTE cap n'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> (dcap = cap) = (cap = dcap)) \<and> (p \<noteq> src \<longrightarrow> (\<exists>n'. n p = Some (CTE cap n')) = (\<exists>n'. m p = Some (CTE cap n'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (\<exists>n'. n p = Some (CTE cap n')) = (\<exists>n'. m p = Some (CTE cap n')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (\<exists>n'. n p = Some (CTE cap n')) = (\<exists>n'. m p = Some (CTE cap n')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; \<exists>n'. n p = Some (CTE cap n')\<rbrakk> \<Longrightarrow> \<exists>n'. m p = Some (CTE cap n')
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; \<exists>n'. m p = Some (CTE cap n')\<rbrakk> \<Longrightarrow> \<exists>n'. n p = Some (CTE cap n') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; \<exists>n'. m p = Some (CTE cap n')\<rbrakk> \<Longrightarrow> \<exists>n'. n p = Some (CTE cap n') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; \<exists>n'. m p = Some (CTE cap n')\<rbrakk> \<Longrightarrow> \<exists>n'. (mdbNext dest2_node \<noteq> p \<longrightarrow> (mdbPrev dest2_node \<noteq> p \<longrightarrow> (mdbNext src_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap n')) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = n'))) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)) \<and> mdbPrev_update (\<lambda>_. dest) node = n'))) \<and> (mdbPrev dest2_node = p \<longrightarrow> (\<exists>node. (mdbNext src_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node))) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node)) \<and> mdbNext_update (\<lambda>_. src) node = n'))) \<and> (mdbNext dest2_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest2_node \<noteq> p \<longrightarrow> (mdbNext src_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node))) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node))) \<and> (mdbPrev dest2_node = p \<longrightarrow> (\<exists>nodea. (mdbNext src_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea))) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)) \<and> mdbPrev_update (\<lambda>_. dest) node = nodea)) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; \<exists>n'. m p = Some (CTE cap n')\<rbrakk> \<Longrightarrow> (p = mdbNext src_node \<longrightarrow> (mdbPrev src_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbNext dest_node = 0 \<and> (mdbNext dest_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>n' node. mdbPrev_update (\<lambda>_. src) node = n'))) \<and> ((mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (dest = mdbNext src_node \<longrightarrow> (\<exists>node. m (mdbNext src_node) = Some (CTE cap node))) \<and> (dest \<noteq> mdbNext src_node \<longrightarrow> (dest = mdbPrev src_node \<longrightarrow> (\<exists>n'. (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> (\<exists>node. m (mdbNext src_node) = Some (CTE cap node) \<and> mdbPrev_update (\<lambda>_. mdbPrev src_node) node = n')) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> (\<exists>node. (\<exists>nodea. m (mdbNext src_node) = Some (CTE cap nodea) \<and> mdbPrev_update (\<lambda>_. mdbPrev src_node) nodea = node) \<and> mdbNext_update (\<lambda>_. src) node = n')))) \<and> (dest \<noteq> mdbPrev src_node \<longrightarrow> (\<exists>n'. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> (\<exists>node. m (mdbNext src_node) = Some (CTE cap node) \<and> mdbPrev_update (\<lambda>_. dest) node = n')) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> (\<exists>node. (\<exists>nodea. m (mdbNext src_node) = Some (CTE cap nodea) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node) \<and> mdbNext_update (\<lambda>_. src) node = n'))) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> 0 \<longrightarrow> mdbPrev src_node = 0 \<and> mdbPrev src_node \<noteq> 0 \<and> (\<exists>nodea. mdbPrev_update (\<lambda>_. dest) nodea = node)) \<and> (mdbPrev dest_node = 0 \<longrightarrow> mdbPrev src_node = 0 \<and> mdbPrev src_node \<noteq> 0 \<and> (\<exists>nodea. (\<exists>node. mdbPrev_update (\<lambda>_. dest) node = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'))))))) \<and> (p \<noteq> mdbNext src_node \<longrightarrow> (mdbPrev src_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> (\<exists>n'. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (p \<noteq> 0 \<longrightarrow> m p = Some (CTE cap n')) \<and> p \<noteq> 0) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (p \<noteq> 0 \<longrightarrow> m p = Some (CTE cap node)) \<and> p \<noteq> 0 \<and> mdbNext_update (\<lambda>_. src) node = n'))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (p \<noteq> 0 \<longrightarrow> m p = Some (CTE cap node)) \<and> p \<noteq> 0) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (p \<noteq> 0 \<longrightarrow> m p = Some (CTE cap nodea)) \<and> p \<noteq> 0 \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n')))) \<and> ((mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (dest = mdbNext src_node \<longrightarrow> (mdbPrev src_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> p \<noteq> 0) \<and> (\<exists>n'. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap n')) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. mdbNext src_node) node = n'))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. mdbNext src_node) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n')))) \<and> (dest \<noteq> mdbNext src_node \<longrightarrow> (dest = mdbPrev src_node \<longrightarrow> (\<exists>n'. (mdbPrev src_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> m p = Some (CTE cap n')) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. src) node = n'))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. p) nodea = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. p) node = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n')))) \<and> (dest \<noteq> mdbPrev src_node \<longrightarrow> (\<exists>n'. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap n')) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = n'))) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)) \<and> mdbNext_update (\<lambda>_. src) node = n'))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node))) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea)) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'))))))) proof (prove)
goal (4 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (5 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 5. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (6 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 5. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 6. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (5 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 5. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (5 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 5. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (6 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; mdbPrev dest_node = mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; mdbPrev dest_node \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 5. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 6. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (5 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; mdbPrev dest_node \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 5. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (4 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. ((mdbNext dest_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)) \<and> (mdbNext dest_node = 0 \<and> mdbNext src_node = 0 \<longrightarrow> mdbPrev dest_node = 0 \<and> mdbPrev dest_node \<noteq> 0 \<and> (\<exists>node. mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (4 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (5 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0; mdbPrev dest_node = mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0; mdbPrev dest_node \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 5. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (4 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m (mdbNext src_node) = Some (CTE cap n'); p = mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> 0; mdbPrev dest_node \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> mdbNext src_node \<longrightarrow> mdbPrev_update (\<lambda>_. dest) n' = n'a) \<and> (mdbPrev dest_node = mdbNext src_node \<longrightarrow> mdbNext_update (\<lambda>_. src) (mdbPrev_update (\<lambda>_. dest) n') = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (4 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0; mdbNext dest_node = p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (4 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0; mdbNext dest_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = node) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (4 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0; mdbNext dest_node \<noteq> p; mdbPrev dest_node = p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> 0; mdbPrev src_node = 0; mdbNext src_node = 0; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev dest_node = p \<longrightarrow> mdbNext_update (\<lambda>_. src) n' = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (4 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (4 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 4. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbPrev src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (3 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 3. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node))
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node = p; mdbPrev dest_node \<noteq> p; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbNext dest_node \<noteq> p \<longrightarrow> (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a))) \<and> (mdbNext dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = nodea) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)) \<and> mdbPrev_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node)
 2. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev dest_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a)) \<and> (mdbPrev dest_node = p \<longrightarrow> (\<exists>node. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = node) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = node) \<and> mdbNext_update (\<lambda>_. src) node = n'a)) proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a) proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> dest; p \<noteq> src; m p = Some (CTE cap n'); p \<noteq> mdbNext src_node; mdbNext src_node \<noteq> 0; dest \<noteq> mdbNext src_node; dest \<noteq> mdbPrev src_node; mdbNext dest_node \<noteq> p; mdbPrev dest_node \<noteq> p; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>n'a. (mdbPrev src_node \<noteq> p \<longrightarrow> n' = n'a) \<and> (mdbPrev src_node = p \<longrightarrow> mdbNext_update (\<lambda>_. dest) n' = n'a) proof (prove)
goal:
No subgoals!