theory CSpace1_R

lemma mdb_inv_preserve_modify_map:
  "mdb_inv_preserve m m' \<Longrightarrow>
   mdb_inv_preserve (modify_map m slot (cteMDBNode_update f))
                    (modify_map m' slot (cteMDBNode_update f))" apply (clarsimp simp:mdb_inv_preserve_def split:if_splits) apply (intro conjI) apply (clarsimp simp:modify_map_dom) apply (clarsimp simp:modify_map_def split:if_splits)+ apply (clarsimp simp:option_map_def o_def split:option.splits if_splits) apply (drule_tac x = p in spec)+ apply (intro allI conjI impI) apply (clarsimp simp:mdb_next_def split:if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_inv_preserve m m' \<Longrightarrow> mdb_inv_preserve (modify_map m slot (cteMDBNode_update f)) (modify_map m' slot (cteMDBNode_update f)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> (\<forall>x. (x \<in> dom (modify_map m slot (cteMDBNode_update f))) = (x \<in> dom (modify_map m' slot (cteMDBNode_update f)))) \<and> (\<forall>x cte. modify_map m slot (cteMDBNode_update f) x = Some cte \<longrightarrow> (\<forall>cte'. modify_map m' slot (cteMDBNode_update f) x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte')) \<and> (\<forall>x cte. modify_map m slot (cteMDBNode_update f) x = Some cte \<longrightarrow> (\<forall>cte'. modify_map m' slot (cteMDBNode_update f) x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte')))) \<and> (\<forall>p. mdb_next (modify_map m slot (cteMDBNode_update f)) p = mdb_next (modify_map m' slot (cteMDBNode_update f)) p) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> \<forall>x. (x \<in> dom (modify_map m slot (cteMDBNode_update f))) = (x \<in> dom (modify_map m' slot (cteMDBNode_update f)))
 2. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> \<forall>x cte. modify_map m slot (cteMDBNode_update f) x = Some cte \<longrightarrow> (\<forall>cte'. modify_map m' slot (cteMDBNode_update f) x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte')
 3. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> \<forall>x cte. modify_map m slot (cteMDBNode_update f) x = Some cte \<longrightarrow> (\<forall>cte'. modify_map m' slot (cteMDBNode_update f) x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte')))
 4. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> \<forall>p. mdb_next (modify_map m slot (cteMDBNode_update f)) p = mdb_next (modify_map m' slot (cteMDBNode_update f)) p proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> \<forall>x cte. modify_map m slot (cteMDBNode_update f) x = Some cte \<longrightarrow> (\<forall>cte'. modify_map m' slot (cteMDBNode_update f) x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte')
 2. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> \<forall>x cte. modify_map m slot (cteMDBNode_update f) x = Some cte \<longrightarrow> (\<forall>cte'. modify_map m' slot (cteMDBNode_update f) x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte')))
 3. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> \<forall>p. mdb_next (modify_map m slot (cteMDBNode_update f)) p = mdb_next (modify_map m' slot (cteMDBNode_update f)) p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> mdb_next (m(slot := map_option (cteMDBNode_update f) (m slot))) p = mdb_next (m'(slot := map_option (cteMDBNode_update f) (m' slot))) p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. (x \<in> dom m) = (x \<in> dom m'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>x cte. m x = Some cte \<longrightarrow> (\<forall>cte'. m' x = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); \<forall>p. mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> (m slot = None \<longrightarrow> (\<forall>x2. m' slot = Some x2 \<longrightarrow> mdb_next m' p = mdb_next (m'(slot \<mapsto> cteMDBNode_update f x2)) p)) \<and> (\<forall>x2. m slot = Some x2 \<longrightarrow> (m' slot = None \<longrightarrow> mdb_next (m(slot \<mapsto> cteMDBNode_update f x2)) p = mdb_next m' p) \<and> (\<forall>x2a. m' slot = Some x2a \<longrightarrow> mdb_next (m(slot \<mapsto> cteMDBNode_update f x2)) p = mdb_next (m'(slot \<mapsto> cteMDBNode_update f x2a)) p)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>(p \<in> dom m) = (p \<in> dom m'); \<forall>cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m' p = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m' p = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> (m slot = None \<longrightarrow> (\<forall>x2. m' slot = Some x2 \<longrightarrow> mdb_next m' p = mdb_next (m'(slot \<mapsto> cteMDBNode_update f x2)) p)) \<and> (\<forall>x2. m slot = Some x2 \<longrightarrow> (m' slot = None \<longrightarrow> mdb_next (m(slot \<mapsto> cteMDBNode_update f x2)) p = mdb_next m' p) \<and> (\<forall>x2a. m' slot = Some x2a \<longrightarrow> mdb_next (m(slot \<mapsto> cteMDBNode_update f x2)) p = mdb_next (m'(slot \<mapsto> cteMDBNode_update f x2a)) p)) proof (prove)
goal (3 subgoals):
 1. \<And>p x2. \<lbrakk>(p \<in> dom m) = (p \<in> dom m'); \<forall>cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m' p = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m' p = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); mdb_next m p = mdb_next m' p; m slot = None; m' slot = Some x2\<rbrakk> \<Longrightarrow> mdb_next m' p = mdb_next (m'(slot \<mapsto> cteMDBNode_update f x2)) p
 2. \<And>p x2. \<lbrakk>(p \<in> dom m) = (p \<in> dom m'); \<forall>cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m' p = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m' p = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); mdb_next m p = mdb_next m' p; m slot = Some x2; m' slot = None\<rbrakk> \<Longrightarrow> mdb_next (m(slot \<mapsto> cteMDBNode_update f x2)) p = mdb_next m' p
 3. \<And>p x2 x2a. \<lbrakk>(p \<in> dom m) = (p \<in> dom m'); \<forall>cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m' p = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> (cteCap cte = capability.NullCap) = (cteCap cte' = capability.NullCap) \<and> isReplyCap (cteCap cte) = isReplyCap (cteCap cte') \<and> (isReplyCap (cteCap cte) \<longrightarrow> capReplyMaster (cteCap cte) = capReplyMaster (cteCap cte')) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte') \<and> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'); \<forall>cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m' p = Some cte' \<longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))); mdb_next m p = mdb_next m' p; m slot = Some x2; m' slot = Some x2a\<rbrakk> \<Longrightarrow> mdb_next (m(slot \<mapsto> cteMDBNode_update f x2)) p = mdb_next (m'(slot \<mapsto> cteMDBNode_update f x2a)) p proof (prove)
goal:
No subgoals!