theory CSpace1_R

lemma valid_badges_preserve_oneway:
  assumes dom:"\<And>x. (x \<in> dom m) = (x \<in> dom m')"
  assumes misc:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow>
    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> cteMDBNode cte = cteMDBNode cte'"
  assumes sameRegion:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow>
    sameRegionAs (cteCap cte) = sameRegionAs (cteCap cte')
  \<and> (\<lambda>x. sameRegionAs x (cteCap cte)) = (\<lambda>x. sameRegionAs x (cteCap cte'))"
  assumes mdb_next:"\<And>p. mdb_next m p = mdb_next m' p"
  shows "valid_badges m \<Longrightarrow> valid_badges m'" apply (clarsimp simp:valid_badges_def) apply (drule_tac x = p in spec) apply (drule_tac x = p' in spec) apply (frule iffD2[OF dom,OF domI],rotate_tac) apply (frule iffD2[OF dom,OF domI],rotate_tac) apply clarsimp apply (case_tac y,case_tac ya) apply clarsimp apply (erule impE) apply (simp add: mdb_next mdb_next_rel_def) apply (erule impE) apply (drule(1) sameRegion)+ apply clarsimp apply (drule fun_cong)+ apply fastforce apply (drule(1) misc)+ apply (clarsimp simp:isCap_simps sameRegionAs_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_badges m \<Longrightarrow> valid_badges m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<forall>p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'))\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<forall>cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'))\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>m' p' = Some (CTE cap' node'); m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<forall>cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); p \<in> dom m; m' p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<forall>cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); p \<in> dom m; m' p = Some (CTE cap node); p' \<in> dom m; m' p' = Some (CTE cap' node')\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' y ya. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<forall>cap. (\<exists>node. y = CTE cap node) \<longrightarrow> (\<forall>cap' node'. ya = CTE cap' node' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some y; m p' = Some ya\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' y ya x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<forall>cap. (\<exists>node. y = CTE cap node) \<longrightarrow> (\<forall>cap' node'. ya = CTE cap' node' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs x1 x1a \<longrightarrow> (isEndpointCap x1 \<longrightarrow> capEPBadge x1 \<noteq> capEPBadge x1a \<longrightarrow> capEPBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a) \<and> (isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 \<noteq> capNtfnBadge x1a \<longrightarrow> capNtfnBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a); m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> p'
 2. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a); global.sameRegionAs x1 x1a \<longrightarrow> (isEndpointCap x1 \<longrightarrow> capEPBadge x1 \<noteq> capEPBadge x1a \<longrightarrow> capEPBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a) \<and> (isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 \<noteq> capNtfnBadge x1a \<longrightarrow> capNtfnBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a); global.sameRegionAs x1 x1a \<longrightarrow> (isEndpointCap x1 \<longrightarrow> capEPBadge x1 \<noteq> capEPBadge x1a \<longrightarrow> capEPBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a) \<and> (isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 \<noteq> capNtfnBadge x1a \<longrightarrow> capNtfnBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 x1a
 2. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a); (isEndpointCap x1 \<longrightarrow> capEPBadge x1 \<noteq> capEPBadge x1a \<longrightarrow> capEPBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a) \<and> (isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 \<noteq> capNtfnBadge x1a \<longrightarrow> capNtfnBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); global.sameRegionAs (cteCap (CTE x1 x2)) = global.sameRegionAs (cteCap (CTE cap node)) \<and> (\<lambda>x. global.sameRegionAs x (cteCap (CTE x1 x2))) = (\<lambda>x. global.sameRegionAs x (cteCap (CTE cap node))); global.sameRegionAs (cteCap (CTE x1a x2a)) = global.sameRegionAs (cteCap (CTE cap' node')) \<and> (\<lambda>x. global.sameRegionAs x (cteCap (CTE x1a x2a))) = (\<lambda>x. global.sameRegionAs x (cteCap (CTE cap' node')))\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 x1a
 2. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a); (isEndpointCap x1 \<longrightarrow> capEPBadge x1 \<noteq> capEPBadge x1a \<longrightarrow> capEPBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a) \<and> (isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 \<noteq> capNtfnBadge x1a \<longrightarrow> capNtfnBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap node cap' node' x1 x1a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); global.sameRegionAs x1 = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1a = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap x1a
 2. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a); (isEndpointCap x1 \<longrightarrow> capEPBadge x1 \<noteq> capEPBadge x1a \<longrightarrow> capEPBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a) \<and> (isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 \<noteq> capNtfnBadge x1a \<longrightarrow> capNtfnBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap node cap' node' x1 x1a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); global.sameRegionAs x1 (?x51 p p' cap node cap' node' x1 x1a) = global.sameRegionAs cap (?x51 p p' cap node cap' node' x1 x1a); global.sameRegionAs (?x53 p p' cap node cap' node' x1 x1a) x1 = global.sameRegionAs (?x53 p p' cap node cap' node' x1 x1a) cap; global.sameRegionAs x1a (?x55 p p' cap node cap' node' x1 x1a) = global.sameRegionAs cap' (?x55 p p' cap node cap' node' x1 x1a); global.sameRegionAs (?x57 p p' cap node cap' node' x1 x1a) x1a = global.sameRegionAs (?x57 p p' cap node cap' node' x1 x1a) cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap x1a
 2. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a); (isEndpointCap x1 \<longrightarrow> capEPBadge x1 \<noteq> capEPBadge x1a \<longrightarrow> capEPBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a) \<and> (isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 \<noteq> capNtfnBadge x1a \<longrightarrow> capNtfnBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); m p = Some (CTE x1 x2); m p' = Some (CTE x1a x2a); (isEndpointCap x1 \<longrightarrow> capEPBadge x1 \<noteq> capEPBadge x1a \<longrightarrow> capEPBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a) \<and> (isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 \<noteq> capNtfnBadge x1a \<longrightarrow> capNtfnBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' x1 x2 x1a x2a. \<lbrakk>m' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; m' p = Some (CTE cap node); m' p' = Some (CTE cap' node'); (isEndpointCap x1 \<longrightarrow> capEPBadge x1 \<noteq> capEPBadge x1a \<longrightarrow> capEPBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a) \<and> (isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 \<noteq> capNtfnBadge x1a \<longrightarrow> capNtfnBadge x1a \<noteq> 0 \<longrightarrow> mdbFirstBadged x2a); isNotificationCap (cteCap (CTE x1 x2)) = isNotificationCap (cteCap (CTE cap node)) \<and> (isNotificationCap (cteCap (CTE x1 x2)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1 x2)) = capNtfnBadge (cteCap (CTE cap node))) \<and> isEndpointCap (cteCap (CTE x1 x2)) = isEndpointCap (cteCap (CTE cap node)) \<and> (isEndpointCap (cteCap (CTE x1 x2)) \<longrightarrow> capEPBadge (cteCap (CTE x1 x2)) = capEPBadge (cteCap (CTE cap node))) \<and> cteMDBNode (CTE x1 x2) = cteMDBNode (CTE cap node); isNotificationCap (cteCap (CTE x1a x2a)) = isNotificationCap (cteCap (CTE cap' node')) \<and> (isNotificationCap (cteCap (CTE x1a x2a)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1a x2a)) = capNtfnBadge (cteCap (CTE cap' node'))) \<and> isEndpointCap (cteCap (CTE x1a x2a)) = isEndpointCap (cteCap (CTE cap' node')) \<and> (isEndpointCap (cteCap (CTE x1a x2a)) \<longrightarrow> capEPBadge (cteCap (CTE x1a x2a)) = capEPBadge (cteCap (CTE cap' node'))) \<and> cteMDBNode (CTE x1a x2a) = cteMDBNode (CTE cap' node')\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal:
No subgoals!