theory CNodeInv_R

lemma (in mdb_move) m'_next:
  "m' \<turnstile> p \<leadsto> p' \<Longrightarrow>
  if p = src then p' = 0
  else if p = dest then m \<turnstile> src \<leadsto> p'
  else if p' = dest then m \<turnstile> p \<leadsto> src
  else m \<turnstile> p \<leadsto> p'" using src dest src_0 dest_0 dlist neq src_neq_prev apply (simp add: m'_def n_def) apply (simp add: mdb_next_unfold) apply (elim exE conjE) apply (case_tac z) apply (rename_tac cap node) apply simp apply (simp add: modify_map_cases) apply (cases "mdbPrev src_node = p") apply clarsimp apply (erule_tac p=src in valid_dlistEp, assumption) apply clarsimp apply clarsimp apply simp apply (cases "p=src", simp) apply clarsimp apply (case_tac "mdbNext node = p") apply clarsimp apply clarsimp apply (erule_tac p=p in valid_dlistEn, assumption) apply clarsimp apply (clarsimp simp: prev) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto> p' \<Longrightarrow> if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p' = dest then m \<turnstile> p \<leadsto> src else m \<turnstile> p \<leadsto> p' proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE capability.NullCap old_dest_node)
src \<noteq> 0
dest \<noteq> 0
valid_dlist m
src \<noteq> dest
src \<noteq> mdbPrev src_node

goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto> p' \<Longrightarrow> if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p' = dest then m \<turnstile> p \<leadsto> src else m \<turnstile> p \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> p \<leadsto> p'; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest\<rbrakk> \<Longrightarrow> (p' = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> m \<turnstile> p \<leadsto> src))) \<and> (p' \<noteq> dest \<longrightarrow> (p = dest \<longrightarrow> m \<turnstile> src \<leadsto> p') \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> p' = 0) \<and> (p \<noteq> src \<longrightarrow> m \<turnstile> p \<leadsto> p'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>z. modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) p = Some z \<and> p' = mdbNext (cteMDBNode z); m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest\<rbrakk> \<Longrightarrow> (p' = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (p' \<noteq> dest \<longrightarrow> (p = dest \<longrightarrow> p' = mdbNext src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> p' = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> p' = mdbNext (cteMDBNode z))))) proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) p = Some z; p' = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> (p' = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (p' \<noteq> dest \<longrightarrow> (p = dest \<longrightarrow> p' = mdbNext src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> p' = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> p' = mdbNext (cteMDBNode z))))) proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) p = Some z; p' = mdbNext (cteMDBNode z); z = CTE x1 x2\<rbrakk> \<Longrightarrow> (p' = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (p' \<noteq> dest \<longrightarrow> (p = dest \<longrightarrow> p' = mdbNext src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> p' = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> p' = mdbNext (cteMDBNode z))))) proof (prove)
goal (1 subgoal):
 1. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) p = Some z; p' = mdbNext (cteMDBNode z); z = CTE cap node\<rbrakk> \<Longrightarrow> (p' = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (p' \<noteq> dest \<longrightarrow> (p = dest \<longrightarrow> p' = mdbNext src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> p' = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> p' = mdbNext (cteMDBNode z))))) proof (prove)
goal (1 subgoal):
 1. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) p = Some (CTE cap node); p' = mdbNext node; z = CTE cap node\<rbrakk> \<Longrightarrow> (mdbNext node = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (mdbNext node \<noteq> dest \<longrightarrow> (p = dest \<longrightarrow> mdbNext node = mdbNext src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbNext node = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> mdbNext node = mdbNext (cteMDBNode z))))) proof (prove)
goal (1 subgoal):
 1. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = node) \<and> nullMDBNode = nodea)) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); p' = mdbNext node; z = CTE cap node\<rbrakk> \<Longrightarrow> (mdbNext node = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbNext node = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> mdbNext node = mdbNext (cteMDBNode z)))) proof (prove)
goal (2 subgoals):
 1. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = node) \<and> nullMDBNode = nodea)) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node = p\<rbrakk> \<Longrightarrow> (mdbNext node = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbNext node = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> mdbNext node = mdbNext (cteMDBNode z))))
 2. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = node) \<and> nullMDBNode = nodea)) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> (mdbNext node = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbNext node = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> mdbNext node = mdbNext (cteMDBNode z)))) proof (prove)
goal (2 subgoals):
 1. \<And>cap nodea. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; p' = dest; p = mdbPrev src_node; m (mdbPrev src_node) = Some (CTE cap nodea)\<rbrakk> \<Longrightarrow> src = mdbNext nodea
 2. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = node) \<and> nullMDBNode = nodea)) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> (mdbNext node = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbNext node = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> mdbNext node = mdbNext (cteMDBNode z)))) proof (prove)
goal (3 subgoals):
 1. \<And>cap nodea. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; src \<noteq> dest; p' = dest; p = mdbPrev src_node; m (mdbPrev src_node) = Some (CTE cap nodea)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (CTE src_cap src_node)) \<noteq> 0
 2. \<And>cap nodea cte'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; src \<noteq> dest; p' = dest; p = mdbPrev src_node; m (mdbPrev src_node) = Some (CTE cap nodea); m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> src = mdbNext nodea
 3. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = node) \<and> nullMDBNode = nodea)) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> (mdbNext node = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbNext node = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> mdbNext node = mdbNext (cteMDBNode z)))) proof (prove)
goal (2 subgoals):
 1. \<And>cap nodea cte'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; src \<noteq> dest; p' = dest; p = mdbPrev src_node; m (mdbPrev src_node) = Some (CTE cap nodea); m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> src = mdbNext nodea
 2. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = node) \<and> nullMDBNode = nodea)) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> (mdbNext node = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbNext node = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> mdbNext node = mdbNext (cteMDBNode z)))) proof (prove)
goal (1 subgoal):
 1. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = node) \<and> nullMDBNode = nodea)) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> (mdbNext node = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> src = mdbNext (cteMDBNode z))))) \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbNext node = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> mdbNext node = mdbNext (cteMDBNode z)))) proof (prove)
goal (1 subgoal):
 1. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> dest \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext node = 0) proof (prove)
goal (2 subgoals):
 1. \<And>z cap. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; capability.NullCap = cap; p' = nullPointer; z = CTE capability.NullCap nullMDBNode; p = src\<rbrakk> \<Longrightarrow> nullPointer \<noteq> dest
 2. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> dest \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext node = 0) proof (prove)
goal (1 subgoal):
 1. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> dest \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext node = 0) proof (prove)
goal (2 subgoals):
 1. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p; p \<noteq> src; mdbNext node = p\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> dest \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext node = 0)
 2. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p; p \<noteq> src; mdbNext node \<noteq> p\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> dest \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext node = 0) proof (prove)
goal (1 subgoal):
 1. \<And>z cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> nullMDBNode = node)); p' = mdbNext node; z = CTE cap node; mdbPrev src_node \<noteq> p; p \<noteq> src; mdbNext node \<noteq> p\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> dest \<and> (mdbNext node \<noteq> dest \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext node = 0) proof (prove)
goal (1 subgoal):
 1. \<And>cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m (mdbNext node) = Some (CTE capability.NullCap old_dest_node); mdbNext node \<noteq> 0; valid_dlist m; src \<noteq> mdbNext node; p' = mdbNext node; mdbPrev src_node \<noteq> p; p \<noteq> src; mdbNext node \<noteq> p; dest = mdbNext node; m p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cap node. \<lbrakk>m src = Some (CTE src_cap src_node); m (mdbNext node) = Some (CTE capability.NullCap old_dest_node); mdbNext node \<noteq> 0; src \<noteq> mdbNext node; p' = mdbNext node; mdbPrev src_node \<noteq> p; p \<noteq> src; mdbNext node \<noteq> p; dest = mdbNext node; m p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (CTE cap node)) \<noteq> 0
 2. \<And>cap node cte'. \<lbrakk>m src = Some (CTE src_cap src_node); m (mdbNext node) = Some (CTE capability.NullCap old_dest_node); mdbNext node \<noteq> 0; src \<noteq> mdbNext node; p' = mdbNext node; mdbPrev src_node \<noteq> p; p \<noteq> src; mdbNext node \<noteq> p; dest = mdbNext node; m p = Some (CTE cap node); m (mdbNext (cteMDBNode (CTE cap node))) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap node cte'. \<lbrakk>m src = Some (CTE src_cap src_node); m (mdbNext node) = Some (CTE capability.NullCap old_dest_node); mdbNext node \<noteq> 0; src \<noteq> mdbNext node; p' = mdbNext node; mdbPrev src_node \<noteq> p; p \<noteq> src; mdbNext node \<noteq> p; dest = mdbNext node; m p = Some (CTE cap node); m (mdbNext (cteMDBNode (CTE cap node))) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!