theory CSpace_C

lemma sameObjectAs_spec:
  "\<forall>capa capb. \<Gamma> \<turnstile> \<lbrace>ccap_relation capa \<acute>cap_a \<and>
                     ccap_relation capb \<acute>cap_b \<and>
                     capAligned capa \<and> capAligned capb \<and> (\<exists>s. s \<turnstile>' capa)\<rbrace>
  Call sameObjectAs_'proc
  \<lbrace> \<acute>ret__unsigned_long = from_bool (sameObjectAs capa capb) \<rbrace>" apply vcg apply (clarsimp simp: sameObjectAs_def isArchCap_tag_def2) apply (case_tac capa, simp_all add: cap_get_tag_isCap_unfolded_H_cap
                                      isCap_simps cap_tag_defs) apply fastforce+
     \<comment> \<open>capa is an arch cap\<close> apply (frule cap_get_tag_isArchCap_unfolded_H_cap) apply (simp add: isArchCap_tag_def2) apply (rule conjI, rule impI, clarsimp, rule impI)+ apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap
                                         isCap_simps cap_tag_defs)[1] apply ((fastforce)+)[7]
         \<comment> \<open>capb is an arch cap\<close> apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) apply (fastforce simp: isArchCap_tag_def2 linorder_not_less [symmetric])+
  \<comment> \<open>capa is an irq handler cap\<close> apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap
                                      isCap_simps cap_tag_defs) apply fastforce+
      \<comment> \<open>capb is an arch cap\<close> apply (frule cap_get_tag_isArchCap_unfolded_H_cap) apply (fastforce simp: isArchCap_tag_def2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>capa capb. \<Gamma>\<turnstile> \<lbrace>ccap_relation capa \<acute>cap_a \<and> ccap_relation capb \<acute>cap_b \<and> capAligned capa \<and> capAligned capb \<and> (\<exists>s. valid_cap' capa s)\<rbrace> Call sameObjectAs_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (global.sameObjectAs capa capb)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>capa capb cap_b cap_a. \<lbrakk>ccap_relation capa cap_a; ccap_relation capb cap_b; capAligned capa; capAligned capb; Ex (valid_cap' capa)\<rbrakk> \<Longrightarrow> \<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_a \<longrightarrow> (cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (global.sameObjectAs capa capb)) \<and> (cap_get_tag cap_a \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_a \<longrightarrow> ((if cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_b \<longrightarrow> ((if cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then 1 else 0) \<noteq> 0 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (global.sameObjectAs capa capb)) \<and> ((if cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then 1 else 0) = 0 \<longrightarrow> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag cap_a)) \<longrightarrow> ((if from_bool (isArchCap_tag (cap_get_tag cap_a)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag cap_b)) \<longrightarrow> ((if from_bool (isArchCap_tag (cap_get_tag cap_b)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> capAligned (capability.ArchObjectCap capaa) \<and> capAligned (capability.ArchObjectCap capba) \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (Arch.sameObjectAs capaa capba) \<longrightarrow> from_bool (Arch.sameObjectAs capaa capba) = from_bool (global.sameObjectAs capa capb))))) \<and> ((if from_bool (isArchCap_tag (cap_get_tag cap_b)) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> (\<exists>capaa. ccap_relation capaa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capaa) \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (global.sameRegionAs capaa capba) \<longrightarrow> from_bool (global.sameRegionAs capaa capba) = from_bool (global.sameObjectAs capa capb))))))) \<and> ((if from_bool (isArchCap_tag (cap_get_tag cap_a)) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> (\<exists>capaa. ccap_relation capaa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capaa) \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (global.sameRegionAs capaa capba) \<longrightarrow> from_bool (global.sameRegionAs capaa capba) = from_bool (global.sameObjectAs capa capb))))))))) \<and> ((if cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then 1 else 0) = 0 \<longrightarrow> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag cap_a)) \<longrightarrow> ((if from_bool (isArchCap_tag (cap_get_tag cap_a)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag cap_b)) \<longrightarrow> ((if from_bool (isArchCap_tag (cap_get_tag cap_b)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> capAligned (capability.ArchObjectCap capaa) \<and> capAligned (capability.ArchObjectCap capba) \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (Arch.sameObjectAs capaa capba) \<longrightarrow> from_bool (Arch.sameObjectAs capaa capba) = from_bool (global.sameObjectAs capa capb))))) \<and> ((if from_bool (isArchCap_tag (cap_get_tag cap_b)) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> (\<exists>capaa. ccap_relation capaa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capaa) \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (global.sameRegionAs capaa capba) \<longrightarrow> from_bool (global.sameRegionAs capaa capba) = from_bool (global.sameObjectAs capa capb))))))) \<and> ((if from_bool (isArchCap_tag (cap_get_tag cap_a)) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> (\<exists>capaa. ccap_relation capaa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capaa) \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (global.sameRegionAs capaa capba) \<longrightarrow> from_bool (global.sameRegionAs capaa capba) = from_bool (global.sameObjectAs capa capb))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capa cap_a; ccap_relation capb cap_b; capAligned capa; capAligned capb; valid_cap' capa x\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> \<not> (case capa of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` capb | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` capb | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` capb | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` capb | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` capb | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` capb | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` capb | capability.ArchObjectCap a \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` capb | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` capb | capability.IRQControlCap \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_a \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap \<longrightarrow> (cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> \<not> (case capa of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` capb | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` capb | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` capb | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` capb | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` capb | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` capb | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` capb | capability.ArchObjectCap a \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` capb | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` capb | capability.IRQControlCap \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap && 1 = 1 \<longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> capAligned (capability.ArchObjectCap capaa) \<and> capAligned (capability.ArchObjectCap capba) \<and> Arch.sameObjectAs capaa capba = (case capa of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` capb | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` capb | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` capb | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` capb | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` capb | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` capb | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` capb | capability.ArchObjectCap a \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` capb | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` capb | capability.IRQControlCap \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capaa. ccap_relation capaa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capaa) \<and> global.sameRegionAs capaa capba = (case capa of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` capb | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` capb | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` capb | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` capb | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` capb | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` capb | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` capb | capability.ArchObjectCap a \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` capb | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` capb | capability.IRQControlCap \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap))))) \<and> (SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap && 1 = 0 \<longrightarrow> (\<exists>capaa. ccap_relation capaa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capaa) \<and> global.sameRegionAs capaa capba = (case capa of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` capb | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` capb | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` capb | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` capb | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` capb | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` capb | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` capb | capability.ArchObjectCap a \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` capb | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` capb | capability.IRQControlCap \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))))) \<and> (cap_get_tag cap_a \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap \<longrightarrow> (cap_get_tag cap_a && 1 = 1 \<longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> capAligned (capability.ArchObjectCap capaa) \<and> capAligned (capability.ArchObjectCap capba) \<and> Arch.sameObjectAs capaa capba = (case capa of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` capb | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` capb | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` capb | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` capb | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` capb | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` capb | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` capb | capability.ArchObjectCap a \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` capb | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` capb | capability.IRQControlCap \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capaa. ccap_relation capaa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capaa) \<and> global.sameRegionAs capaa capba = (case capa of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` capb | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` capb | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` capb | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` capb | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` capb | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` capb | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` capb | capability.ArchObjectCap a \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` capb | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` capb | capability.IRQControlCap \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap))))) \<and> (cap_get_tag cap_a && 1 = 0 \<longrightarrow> (\<exists>capaa. ccap_relation capaa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capaa) \<and> global.sameRegionAs capaa capba = (case capa of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` capb | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` capb | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` capb | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` capb | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` capb | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` capb | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` capb | capability.ArchObjectCap a \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` capb | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` capb | capability.IRQControlCap \<Rightarrow> case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))))) proof (prove)
goal (11 subgoals):
 1. \<And>capa capb cap_b cap_a x x1. \<lbrakk>ccap_relation (capability.ThreadCap x1) cap_a; ccap_relation capb cap_b; capAligned (capability.ThreadCap x1); capAligned capb; valid_cap' (capability.ThreadCap x1) x; capa = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.ThreadCap x1) capb)
 2. \<And>capa capb cap_b cap_a. \<lbrakk>ccap_relation capability.NullCap cap_a; ccap_relation capb cap_b; capAligned capb; capa = capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> \<not> global.sameRegionAs capa capb)
 3. \<And>capa capb cap_b cap_a x x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) cap_a; ccap_relation capb cap_b; capAligned (capability.NotificationCap x31 x32 x33 x34); capAligned capb; valid_cap' (capability.NotificationCap x31 x32 x33 x34) x; capa = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.NotificationCap x31 x32 x33 x34) capb)
 4. \<And>capa capb cap_b cap_a x x4. \<lbrakk>ccap_relation (capability.IRQHandlerCap x4) cap_a; ccap_relation capb cap_b; capAligned (capability.IRQHandlerCap x4); capAligned capb; valid_cap' (capability.IRQHandlerCap x4) x; capa = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.IRQHandlerCap x4) capb)
 5. \<And>capa capb cap_b cap_a x x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap_a; ccap_relation capb cap_b; capAligned (capability.EndpointCap x51 x52 x53 x54 x55 x56); capAligned capb; valid_cap' (capability.EndpointCap x51 x52 x53 x54 x55 x56) x; capa = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) capb)
 6. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.DomainCap cap_a; ccap_relation capb cap_b; capAligned capability.DomainCap; capAligned capb; valid_cap' capability.DomainCap x; capa = capability.DomainCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs capability.DomainCap capb)
 7. \<And>capa capb cap_b cap_a x x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) cap_a; ccap_relation capb cap_b; capAligned (capability.Zombie x71 x72 x73); capAligned capb; valid_cap' (capability.Zombie x71 x72 x73) x; capa = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> \<not> global.sameRegionAs capa capb)
 8. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation capb cap_b; capAligned (capability.ArchObjectCap x8); capAligned capb; valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = 2 \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_a \<noteq> 2 \<longrightarrow> (cap_get_tag cap_a = 0xE \<longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))) \<and> (cap_get_tag cap_a \<noteq> 0xE \<longrightarrow> (cap_get_tag cap_a && 1 = 1 \<longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> capAligned (capability.ArchObjectCap capa) \<and> capAligned (capability.ArchObjectCap capba) \<and> Arch.sameObjectAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))) \<and> (cap_get_tag cap_a && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))))
 9. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap_a; ccap_relation capb cap_b; capAligned (capability.ReplyCap x91 x92 x93); capAligned capb; valid_cap' (capability.ReplyCap x91 x92 x93) x; capa = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.ReplyCap x91 x92 x93) capb)
 10. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_a; ccap_relation capb cap_b; capAligned (capability.CNodeCap x111 x112 x113 x114); capAligned capb; valid_cap' (capability.CNodeCap x111 x112 x113 x114) x; capa = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.CNodeCap x111 x112 x113 x114) capb)
A total of 11 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation capb cap_b; capAligned (capability.ArchObjectCap x8); capAligned capb; valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = 2 \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_a \<noteq> 2 \<longrightarrow> (cap_get_tag cap_a = 0xE \<longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))) \<and> (cap_get_tag cap_a \<noteq> 0xE \<longrightarrow> (cap_get_tag cap_a && 1 = 1 \<longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> capAligned (capability.ArchObjectCap capa) \<and> capAligned (capability.ArchObjectCap capba) \<and> Arch.sameObjectAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))) \<and> (cap_get_tag cap_a && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))))
 2. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap_a; ccap_relation capb cap_b; capAligned (capability.ReplyCap x91 x92 x93); capAligned capb; valid_cap' (capability.ReplyCap x91 x92 x93) x; capa = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.ReplyCap x91 x92 x93) capb)
 3. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_a; ccap_relation capb cap_b; capAligned (capability.CNodeCap x111 x112 x113 x114); capAligned capb; valid_cap' (capability.CNodeCap x111 x112 x113 x114) x; capa = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.CNodeCap x111 x112 x113 x114) capb)
 4. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capb cap_b; capAligned capability.IRQControlCap; capAligned capb; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))) proof (prove)
goal (4 subgoals):
 1. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation capb cap_b; capAligned (capability.ArchObjectCap x8); capAligned capb; valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; isArchCap_tag (cap_get_tag cap_a)\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = 2 \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_a \<noteq> 2 \<longrightarrow> (cap_get_tag cap_a = 0xE \<longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))) \<and> (cap_get_tag cap_a \<noteq> 0xE \<longrightarrow> (cap_get_tag cap_a && 1 = 1 \<longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> capAligned (capability.ArchObjectCap capa) \<and> capAligned (capability.ArchObjectCap capba) \<and> Arch.sameObjectAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))) \<and> (cap_get_tag cap_a && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))))
 2. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap_a; ccap_relation capb cap_b; capAligned (capability.ReplyCap x91 x92 x93); capAligned capb; valid_cap' (capability.ReplyCap x91 x92 x93) x; capa = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.ReplyCap x91 x92 x93) capb)
 3. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_a; ccap_relation capb cap_b; capAligned (capability.CNodeCap x111 x112 x113 x114); capAligned capb; valid_cap' (capability.CNodeCap x111 x112 x113 x114) x; capa = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.CNodeCap x111 x112 x113 x114) capb)
 4. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capb cap_b; capAligned capability.IRQControlCap; capAligned capb; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))) proof (prove)
goal (4 subgoals):
 1. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation capb cap_b; capAligned (capability.ArchObjectCap x8); capAligned capb; valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = 2 \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_a \<noteq> 2 \<longrightarrow> (cap_get_tag cap_a = 0xE \<longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))) \<and> (cap_get_tag cap_a \<noteq> 0xE \<longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> capAligned (capability.ArchObjectCap capa) \<and> capAligned (capability.ArchObjectCap capba) \<and> Arch.sameObjectAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))))
 2. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap_a; ccap_relation capb cap_b; capAligned (capability.ReplyCap x91 x92 x93); capAligned capb; valid_cap' (capability.ReplyCap x91 x92 x93) x; capa = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.ReplyCap x91 x92 x93) capb)
 3. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_a; ccap_relation capb cap_b; capAligned (capability.CNodeCap x111 x112 x113 x114); capAligned capb; valid_cap' (capability.CNodeCap x111 x112 x113 x114) x; capa = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.CNodeCap x111 x112 x113 x114) capb)
 4. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capb cap_b; capAligned capability.IRQControlCap; capAligned capb; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))) proof (prove)
goal (4 subgoals):
 1. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation capb cap_b; capAligned (capability.ArchObjectCap x8); capAligned capb; valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> capAligned (capability.ArchObjectCap capa) \<and> capAligned (capability.ArchObjectCap capba) \<and> Arch.sameObjectAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap)))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> x8 `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap x8 `~global.sameRegionAs~` capability.IRQControlCap))))
 2. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap_a; ccap_relation capb cap_b; capAligned (capability.ReplyCap x91 x92 x93); capAligned capb; valid_cap' (capability.ReplyCap x91 x92 x93) x; capa = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.ReplyCap x91 x92 x93) capb)
 3. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_a; ccap_relation capb cap_b; capAligned (capability.CNodeCap x111 x112 x113 x114); capAligned capb; valid_cap' (capability.CNodeCap x111 x112 x113 x114) x; capa = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.CNodeCap x111 x112 x113 x114) capb)
 4. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capb cap_b; capAligned capability.IRQControlCap; capAligned capb; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))) proof (prove)
goal (15 subgoals):
 1. \<And>capa capb cap_b cap_a x x8 x1. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.ThreadCap x1) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.ThreadCap x1); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.ThreadCap x1))
 2. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation capability.NullCap cap_b; capAligned (capability.ArchObjectCap x8); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> \<not> global.sameRegionAs capa capb)
 3. \<And>capa capb cap_b cap_a x x8 x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.NotificationCap x31 x32 x33 x34) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.NotificationCap x31 x32 x33 x34); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.NotificationCap x31 x32 x33 x34))
 4. \<And>capa capb cap_b cap_a x x8 x4. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.IRQHandlerCap x4) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.IRQHandlerCap x4); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.IRQHandlerCap x4))
 5. \<And>capa capb cap_b cap_a x x8 x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.EndpointCap x51 x52 x53 x54 x55 x56); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.EndpointCap x51 x52 x53 x54 x55 x56))
 6. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation capability.DomainCap cap_b; capAligned (capability.ArchObjectCap x8); capAligned capability.DomainCap; valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.DomainCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) capability.DomainCap)
 7. \<And>capa capb cap_b cap_a x x8 x71 x72 x73. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.Zombie x71 x72 x73) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.Zombie x71 x72 x73); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.Zombie x71 x72 x73))
 8. \<And>capa capb cap_b cap_a x x8 x8a. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.ArchObjectCap x8a) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.ArchObjectCap x8a); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.ArchObjectCap x8a\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> capAligned (capability.ArchObjectCap capa) \<and> capAligned (capability.ArchObjectCap capb) \<and> Arch.sameObjectAs capa capb = Arch.sameObjectAs x8 x8a))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = Arch.sameObjectAs x8 x8a)))
 9. \<And>capa capb cap_b cap_a x x8 x91 x92 x93. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.ReplyCap x91 x92 x93) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.ReplyCap x91 x92 x93); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.ReplyCap x91 x92 x93))
 10. \<And>capa capb cap_b cap_a x x8 x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.UntypedCap x101 x102 x103 x104); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.UntypedCap x101 x102 x103 x104))
A total of 15 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>capa capb cap_b cap_a x x8 x8a. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.ArchObjectCap x8a) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.ArchObjectCap x8a); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.ArchObjectCap x8a\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> capAligned (capability.ArchObjectCap capa) \<and> capAligned (capability.ArchObjectCap capb) \<and> Arch.sameObjectAs capa capb = Arch.sameObjectAs x8 x8a))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = Arch.sameObjectAs x8 x8a)))
 2. \<And>capa capb cap_b cap_a x x8 x91 x92 x93. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.ReplyCap x91 x92 x93) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.ReplyCap x91 x92 x93); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.ReplyCap x91 x92 x93))
 3. \<And>capa capb cap_b cap_a x x8 x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.UntypedCap x101 x102 x103 x104); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.UntypedCap x101 x102 x103 x104))
 4. \<And>capa capb cap_b cap_a x x8 x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.CNodeCap x111 x112 x113 x114); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.CNodeCap x111 x112 x113 x114))
 5. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation capability.IRQControlCap cap_b; capAligned (capability.ArchObjectCap x8); capAligned capability.IRQControlCap; valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) capability.IRQControlCap)
 6. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap_a; ccap_relation capb cap_b; capAligned (capability.ReplyCap x91 x92 x93); capAligned capb; valid_cap' (capability.ReplyCap x91 x92 x93) x; capa = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.ReplyCap x91 x92 x93) capb)
 7. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_a; ccap_relation capb cap_b; capAligned (capability.CNodeCap x111 x112 x113 x114); capAligned capb; valid_cap' (capability.CNodeCap x111 x112 x113 x114) x; capa = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.CNodeCap x111 x112 x113 x114) capb)
 8. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capb cap_b; capAligned capability.IRQControlCap; capAligned capb; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))) proof (prove)
goal (8 subgoals):
 1. \<And>capa capb cap_b cap_a x x8 x8a. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.ArchObjectCap x8a) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.ArchObjectCap x8a); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.ArchObjectCap x8a; isArchCap_tag (cap_get_tag cap_b)\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b && 1 = 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> capAligned (capability.ArchObjectCap capa) \<and> capAligned (capability.ArchObjectCap capb) \<and> Arch.sameObjectAs capa capb = Arch.sameObjectAs x8 x8a))) \<and> (cap_get_tag cap_b && 1 = 0 \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = Arch.sameObjectAs x8 x8a)))
 2. \<And>capa capb cap_b cap_a x x8 x91 x92 x93. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.ReplyCap x91 x92 x93) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.ReplyCap x91 x92 x93); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.ReplyCap x91 x92 x93))
 3. \<And>capa capb cap_b cap_a x x8 x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.UntypedCap x101 x102 x103 x104); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.UntypedCap x101 x102 x103 x104))
 4. \<And>capa capb cap_b cap_a x x8 x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_b; capAligned (capability.ArchObjectCap x8); capAligned (capability.CNodeCap x111 x112 x113 x114); valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) (capability.CNodeCap x111 x112 x113 x114))
 5. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap_a; ccap_relation capability.IRQControlCap cap_b; capAligned (capability.ArchObjectCap x8); capAligned capability.IRQControlCap; valid_cap' (capability.ArchObjectCap x8) x; capa = capability.ArchObjectCap x8; cap_get_tag cap_a && 1 = 1; cap_get_tag cap_a \<noteq> 2; cap_get_tag cap_a \<noteq> 0xE; capb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs (capability.ArchObjectCap x8) capability.IRQControlCap)
 6. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap_a; ccap_relation capb cap_b; capAligned (capability.ReplyCap x91 x92 x93); capAligned capb; valid_cap' (capability.ReplyCap x91 x92 x93) x; capa = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.ReplyCap x91 x92 x93) capb)
 7. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_a; ccap_relation capb cap_b; capAligned (capability.CNodeCap x111 x112 x113 x114); capAligned capb; valid_cap' (capability.CNodeCap x111 x112 x113 x114) x; capa = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = global.sameRegionAs (capability.CNodeCap x111 x112 x113 x114) capb)
 8. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capb cap_b; capAligned capability.IRQControlCap; capAligned capb; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))) proof (prove)
goal (1 subgoal):
 1. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capb cap_b; capAligned capability.IRQControlCap; capAligned capb; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capba. ccap_relation capba cap_b \<and> capAligned capba \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capba = (case capb of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)))) proof (prove)
goal (11 subgoals):
 1. \<And>capa capb cap_b cap_a x x1. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.ThreadCap x1) cap_b; capAligned capability.IRQControlCap; capAligned (capability.ThreadCap x1); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.ThreadCap x1))
 2. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capability.NullCap cap_b; capAligned capability.IRQControlCap; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> \<not> global.sameRegionAs capa capb)
 3. \<And>capa capb cap_b cap_a x x31 x32 x33 x34. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.NotificationCap x31 x32 x33 x34) cap_b; capAligned capability.IRQControlCap; capAligned (capability.NotificationCap x31 x32 x33 x34); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.NotificationCap x31 x32 x33 x34))
 4. \<And>capa capb cap_b cap_a x x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap_b; capAligned capability.IRQControlCap; capAligned (capability.EndpointCap x51 x52 x53 x54 x55 x56); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.EndpointCap x51 x52 x53 x54 x55 x56))
 5. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capability.DomainCap cap_b; capAligned capability.IRQControlCap; capAligned capability.DomainCap; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.DomainCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap capability.DomainCap)
 6. \<And>capa capb cap_b cap_a x x71 x72 x73. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.Zombie x71 x72 x73) cap_b; capAligned capability.IRQControlCap; capAligned (capability.Zombie x71 x72 x73); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.Zombie x71 x72 x73))
 7. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.ArchObjectCap x8) cap_b; capAligned capability.IRQControlCap; capAligned (capability.ArchObjectCap x8); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> global.sameRegionAs capability.IRQControlCap (capability.ArchObjectCap x8)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.ArchObjectCap x8))))
 8. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.ReplyCap x91 x92 x93) cap_b; capAligned capability.IRQControlCap; capAligned (capability.ReplyCap x91 x92 x93); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.ReplyCap x91 x92 x93))
 9. \<And>capa capb cap_b cap_a x x101 x102 x103 x104. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap_b; capAligned capability.IRQControlCap; capAligned (capability.UntypedCap x101 x102 x103 x104); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.UntypedCap x101 x102 x103 x104))
 10. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_b; capAligned capability.IRQControlCap; capAligned (capability.CNodeCap x111 x112 x113 x114); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.CNodeCap x111 x112 x113 x114))
A total of 11 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.ArchObjectCap x8) cap_b; capAligned capability.IRQControlCap; capAligned (capability.ArchObjectCap x8); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> global.sameRegionAs capability.IRQControlCap (capability.ArchObjectCap x8)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.ArchObjectCap x8))))
 2. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.ReplyCap x91 x92 x93) cap_b; capAligned capability.IRQControlCap; capAligned (capability.ReplyCap x91 x92 x93); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.ReplyCap x91 x92 x93))
 3. \<And>capa capb cap_b cap_a x x101 x102 x103 x104. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap_b; capAligned capability.IRQControlCap; capAligned (capability.UntypedCap x101 x102 x103 x104); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.UntypedCap x101 x102 x103 x104))
 4. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_b; capAligned capability.IRQControlCap; capAligned (capability.CNodeCap x111 x112 x113 x114); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.CNodeCap x111 x112 x113 x114))
 5. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capability.IRQControlCap cap_b; capAligned capability.IRQControlCap; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap capability.IRQControlCap) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x x8. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.ArchObjectCap x8) cap_b; capAligned capability.IRQControlCap; capAligned (capability.ArchObjectCap x8); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.ArchObjectCap x8; isArchCap_tag (cap_get_tag cap_b)\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 0x1E \<longrightarrow> \<not> global.sameRegionAs capability.IRQControlCap (capability.ArchObjectCap x8)) \<and> (cap_get_tag cap_b \<noteq> 0x1E \<longrightarrow> (\<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.ArchObjectCap x8))))
 2. \<And>capa capb cap_b cap_a x x91 x92 x93. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.ReplyCap x91 x92 x93) cap_b; capAligned capability.IRQControlCap; capAligned (capability.ReplyCap x91 x92 x93); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.ReplyCap x91 x92 x93))
 3. \<And>capa capb cap_b cap_a x x101 x102 x103 x104. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap_b; capAligned capability.IRQControlCap; capAligned (capability.UntypedCap x101 x102 x103 x104); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.UntypedCap x101 x102 x103 x104))
 4. \<And>capa capb cap_b cap_a x x111 x112 x113 x114. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap_b; capAligned capability.IRQControlCap; capAligned (capability.CNodeCap x111 x112 x113 x114); valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap (capability.CNodeCap x111 x112 x113 x114))
 5. \<And>capa capb cap_b cap_a x. \<lbrakk>ccap_relation capability.IRQControlCap cap_a; ccap_relation capability.IRQControlCap cap_b; capAligned capability.IRQControlCap; valid_cap' capability.IRQControlCap x; capa = capability.IRQControlCap; capb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation capa cap_a \<and> (\<exists>capb. ccap_relation capb cap_b \<and> capAligned capb \<and> Ex (valid_cap' capa) \<and> global.sameRegionAs capa capb = global.sameRegionAs capability.IRQControlCap capability.IRQControlCap) proof (prove)
goal:
No subgoals!