theory CSpace_C

lemma Arch_sameObjectAs_spec:
  "\<forall>capa capb. \<Gamma> \<turnstile> \<lbrace>ccap_relation (ArchObjectCap capa) \<acute>cap_a \<and>
                     ccap_relation (ArchObjectCap capb) \<acute>cap_b \<and>
                     capAligned (ArchObjectCap capa) \<and>
                     capAligned (ArchObjectCap capb) \<rbrace>
  Call Arch_sameObjectAs_'proc
  \<lbrace> \<acute>ret__unsigned_long = from_bool (Arch.sameObjectAs capa capb) \<rbrace>" apply vcg apply (clarsimp simp: ARM_H.sameObjectAs_def) apply (case_tac capa, simp_all add: cap_get_tag_isCap_unfolded_H_cap
                                      isCap_defs cap_tag_defs) apply fastforce+ apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap
                                        isCap_defs cap_tag_defs) apply fastforce+ apply (rename_tac vmpage_size opt d w r vmpage_sizea opt') apply (case_tac "vmpage_size = ARMSmallPage",
             simp_all add: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs)[1] apply (rename_tac vmpage_sizea optiona) apply (case_tac "vmpage_sizea = ARMSmallPage",
              simp_all add: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs)[1] apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(16), simp) apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(16), simp) apply (simp add: ccap_relation_def map_option_case) apply (simp add: cap_small_frame_cap_lift) apply (clarsimp simp: cap_to_H_def capAligned_def to_bool_def
                      split: if_split bool.split
                      dest!: is_aligned_no_overflow) apply (case_tac "vmpage_sizea = ARMSmallPage",
             simp_all add: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs)[1] apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(17), simp) apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(17), simp) apply (simp add: ccap_relation_def map_option_case) apply (simp add: cap_frame_cap_lift) apply (clarsimp simp: cap_to_H_def capAligned_def
                            c_valid_cap_def cl_valid_cap_def
                            Kernel_C.ARMSmallPage_def
                     split: if_split bool.split vmpage_size.split_asm
                     dest!: is_aligned_no_overflow) apply (simp add: framesize_to_H_eq capFSize_range to_bool_def
                       cap_frame_cap_lift [symmetric]) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>capa capb. \<Gamma>\<turnstile> \<lbrace>ccap_relation (capability.ArchObjectCap capa) \<acute>cap_a \<and> ccap_relation (capability.ArchObjectCap capb) \<acute>cap_b \<and> capAligned (capability.ArchObjectCap capa) \<and> capAligned (capability.ArchObjectCap capb)\<rbrace> Call Arch_sameObjectAs_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (Arch.sameObjectAs capa capb)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>capa capb cap_b cap_a. \<lbrakk>ccap_relation (capability.ArchObjectCap capa) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap capa); capAligned (capability.ArchObjectCap capb)\<rbrakk> \<Longrightarrow> \<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_a \<longrightarrow> (cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_b \<longrightarrow> (cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> ((if cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = SCAST(32 signed \<rightarrow> 32) 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = SCAST(32 signed \<rightarrow> 32) 0 then 1 else 0) then 1 else 0) = from_bool (Arch.sameObjectAs capa capb)))) \<and> ((if cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) then 1 else 0) = 0 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = from_bool (Arch.sameObjectAs capa capb))))) \<and> (cap_get_tag cap_b \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_b \<longrightarrow> (cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (Arch.sameObjectAs capa capb)) \<and> (cap_get_tag cap_b \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_b \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_b \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (Arch.sameRegionAs capaa capba) \<longrightarrow> from_bool (Arch.sameRegionAs capaa capba) = from_bool (Arch.sameObjectAs capa capb))))))) \<and> (SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (Arch.sameRegionAs capaa capba) \<longrightarrow> from_bool (Arch.sameRegionAs capaa capba) = from_bool (Arch.sameObjectAs capa capb))))))))))) \<and> (cap_get_tag cap_a \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_a \<longrightarrow> (cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_b \<longrightarrow> (cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> ((if cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capFSize_CL (cap_frame_cap_lift cap_a) \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> ((if capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = SCAST(32 signed \<rightarrow> 32) 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = SCAST(32 signed \<rightarrow> 32) 0 then 1 else 0) then 1 else 0) = from_bool (Arch.sameObjectAs capa capb)))) \<and> ((if capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) then 1 else 0) = 0 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = from_bool (Arch.sameObjectAs capa capb))))) \<and> ((if cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) then 1 else 0) = 0 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = from_bool (Arch.sameObjectAs capa capb))))) \<and> (cap_get_tag cap_b \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap_b \<longrightarrow> (cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (Arch.sameObjectAs capa capb)) \<and> (cap_get_tag cap_b \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (Arch.sameRegionAs capaa capba) \<longrightarrow> from_bool (Arch.sameRegionAs capaa capba) = from_bool (Arch.sameObjectAs capa capb))))))))) \<and> (cap_get_tag cap_a \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = from_bool (Arch.sameRegionAs capaa capba) \<longrightarrow> from_bool (Arch.sameRegionAs capaa capba) = from_bool (Arch.sameObjectAs capa capb))))))) proof (prove)
goal (1 subgoal):
 1. \<And>capa capb cap_b cap_a. \<lbrakk>ccap_relation (capability.ArchObjectCap capa) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap capa); capAligned (capability.ArchObjectCap capb)\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb) = 0)) \<and> (cap_get_tag cap_b \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> \<not> (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (cap_get_tag cap_b \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capaa capba = (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)))))) \<and> (cap_get_tag cap_a \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb) = 0)) \<and> (cap_get_tag cap_b \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> \<not> (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (cap_get_tag cap_b \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capaa capba = (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)))))) \<and> (cap_get_tag cap_a \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capaa capba = (if isPageCap capa \<and> isPageCap capb then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb))))) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x11 x12. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.ASIDPoolCap x11 x12) capb)
 2. \<And>capa capb cap_b cap_a. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_capability.ASIDControlCap) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap arch_capability.ASIDControlCap); capAligned (capability.ArchObjectCap capb); capa = arch_capability.ASIDControlCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs arch_capability.ASIDControlCap capb)
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = 1 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb) = 0)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> \<not> (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capaa capba = (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)))))) \<and> (cap_get_tag cap_a \<noteq> 1 \<longrightarrow> (cap_get_tag cap_a = 3 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> \<not> (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capaa capba = (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)))))) \<and> (cap_get_tag cap_a \<noteq> 3 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capaa capba = (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)))))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (3 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = 1 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb) = 0)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> \<not> (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capaa capba = (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)))))) \<and> (cap_get_tag cap_a \<noteq> 1 \<longrightarrow> (cap_get_tag cap_a = 3 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> \<not> (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capaa capba = (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)))))) \<and> (cap_get_tag cap_a \<noteq> 3 \<longrightarrow> (\<exists>capaa. ccap_relation (capability.ArchObjectCap capaa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capaa capba = (if case capb of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then let ptrA = capVPBasePtr capa in ptrA = capVPBasePtr capb \<and> capVPSize capa = capVPSize capb \<and> ptrA \<le> ptrA + HaskellLib_H.bit (pageBitsForSize $ capVPSize capa) - 1 \<and> capVPIsDevice capa = capVPIsDevice capb else Arch.sameRegionAs capa capb)))))
 2. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 3. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (7 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x11 x12. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.ASIDPoolCap x11 x12))
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap arch_capability.ASIDControlCap) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap arch_capability.ASIDControlCap); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.ASIDControlCap\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) arch_capability.ASIDControlCap)
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x31a x32a x33a x34a x35a. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33a x34a x35a)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33a x34a x35a)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageCap x31a x32a x33a x34a x35a\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = 1 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a) = 0)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<longrightarrow> x34 = x34a \<longrightarrow> x32 = x32a \<longrightarrow> x31 = (\<not> x31a)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)))))) \<and> (cap_get_tag cap_a \<noteq> 1 \<longrightarrow> (cap_get_tag cap_a = 3 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<longrightarrow> x34 = x34a \<longrightarrow> x32 = x32a \<longrightarrow> x31 = (\<not> x31a)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)))))) \<and> (cap_get_tag cap_a \<noteq> 3 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)))))
 4. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 5. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 6. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 7. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x31a x32a x33a x34a x35a. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33a x34a x35a)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33a x34a x35a)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageCap x31a x32a x33a x34a x35a\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = 1 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a) = 0)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<longrightarrow> x34 = x34a \<longrightarrow> x32 = x32a \<longrightarrow> x31 = (\<not> x31a)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)))))) \<and> (cap_get_tag cap_a \<noteq> 1 \<longrightarrow> (cap_get_tag cap_a = 3 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<longrightarrow> x34 = x34a \<longrightarrow> x32 = x32a \<longrightarrow> x31 = (\<not> x31a)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)))))) \<and> (cap_get_tag cap_a \<noteq> 3 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)))))
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'\<rbrakk> \<Longrightarrow> (cap_get_tag cap_a = 1 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))) \<and> (cap_get_tag cap_a \<noteq> 1 \<longrightarrow> (cap_get_tag cap_a = 3 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))) \<and> (cap_get_tag cap_a \<noteq> 3 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (6 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size = Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> Wellformed_C.ARMSmallPage = vmpage_sizea \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> Wellformed_C.ARMSmallPage = vmpage_sizea \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> x32 \<le> 0xFFF + x32 \<longrightarrow> Wellformed_C.ARMSmallPage = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> Wellformed_C.ARMSmallPage = vmpage_sizea \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d)))))
 2. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 4. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 5. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 6. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (6 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea optiona. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea optiona)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea optiona)); capa = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt; capb = arch_capability.PageCap d w r vmpage_sizea optiona; vmpage_size = Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> Wellformed_C.ARMSmallPage = vmpage_sizea \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> Wellformed_C.ARMSmallPage = vmpage_sizea \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> x32 \<le> 0xFFF + x32 \<longrightarrow> Wellformed_C.ARMSmallPage = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> Wellformed_C.ARMSmallPage = vmpage_sizea \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d)))))
 2. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 4. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 5. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 6. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (6 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea optiona. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona)); capa = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt; capb = arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona; vmpage_size = Wellformed_C.ARMSmallPage; vmpage_sizea = Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 4. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 5. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 6. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (6 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea optiona. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona)); capa = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt; capb = arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona; vmpage_size = Wellformed_C.ARMSmallPage; vmpage_sizea = Wellformed_C.ARMSmallPage; cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 4. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 5. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 6. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (6 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea optiona. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona)); capa = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt; capb = arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona; vmpage_size = Wellformed_C.ARMSmallPage; vmpage_sizea = Wellformed_C.ARMSmallPage; cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 4. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 5. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 6. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (6 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea optiona. \<lbrakk>Some (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)) = (case cap_lift cap_a of None \<Rightarrow> None | Some x \<Rightarrow> Some (cap_to_H x)); Some (capability.ArchObjectCap (arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona)) = (case cap_lift cap_b of None \<Rightarrow> None | Some x \<Rightarrow> Some (cap_to_H x)); capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona)); capa = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt; capb = arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona; vmpage_size = Wellformed_C.ARMSmallPage; vmpage_sizea = Wellformed_C.ARMSmallPage; cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 4. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 5. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 6. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (6 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea optiona. \<lbrakk>capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt) = cap_to_H (Cap_small_frame_cap (cap_small_frame_cap_lift cap_a)); capability.ArchObjectCap (arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona) = cap_to_H (Cap_small_frame_cap (cap_small_frame_cap_lift cap_b)); capAligned (cap_to_H (Cap_small_frame_cap (cap_small_frame_cap_lift cap_a))); capAligned (cap_to_H (Cap_small_frame_cap (cap_small_frame_cap_lift cap_b))); capa = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage opt; capb = arch_capability.PageCap d w r Wellformed_C.ARMSmallPage optiona; vmpage_size = Wellformed_C.ARMSmallPage; vmpage_sizea = Wellformed_C.ARMSmallPage; cap_lift cap_a = Some (Cap_small_frame_cap (cap_small_frame_cap_lift cap_a)); cap_lift cap_b = Some (Cap_small_frame_cap (cap_small_frame_cap_lift cap_b))\<rbrakk> \<Longrightarrow> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d)) \<and> (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_a) \<noteq> cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> x32 \<le> 0xFFF + x32 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 4. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 5. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 6. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_get_tag cap_b = 3 \<longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_get_tag cap_b \<noteq> 3 \<longrightarrow> (cap_get_tag cap_b = 1 \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> vmpage_size = vmpage_sizea \<longrightarrow> x32 = w \<longrightarrow> x31 = (\<not> d)) \<and> (cap_get_tag cap_b \<noteq> 1 \<longrightarrow> (\<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)))))
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage; vmpage_sizea \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage; vmpage_sizea \<noteq> Wellformed_C.ARMSmallPage; cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage; vmpage_sizea \<noteq> Wellformed_C.ARMSmallPage; cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>Some (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)) = (case cap_lift cap_a of None \<Rightarrow> None | Some x \<Rightarrow> Some (cap_to_H x)) \<and> c_valid_cap cap_a; Some (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')) = (case cap_lift cap_b of None \<Rightarrow> None | Some x \<Rightarrow> Some (cap_to_H x)) \<and> c_valid_cap cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt)); capAligned (capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt')); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage; vmpage_sizea \<noteq> Wellformed_C.ARMSmallPage; cap_get_tag cap_a = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_get_tag cap_b = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (5 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 vmpage_size opt d w r vmpage_sizea opt'. \<lbrakk>capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size opt) = cap_to_H (Cap_frame_cap (cap_frame_cap_lift cap_a)) \<and> c_valid_cap cap_a; capability.ArchObjectCap (arch_capability.PageCap d w r vmpage_sizea opt') = cap_to_H (Cap_frame_cap (cap_frame_cap_lift cap_b)) \<and> c_valid_cap cap_b; capAligned (cap_to_H (Cap_frame_cap (cap_frame_cap_lift cap_a))); capAligned (cap_to_H (Cap_frame_cap (cap_frame_cap_lift cap_b))); capa = arch_capability.PageCap x31 x32 x33 vmpage_size opt; capb = arch_capability.PageCap d w r vmpage_sizea opt'; vmpage_size \<noteq> Wellformed_C.ARMSmallPage; vmpage_sizea \<noteq> Wellformed_C.ARMSmallPage; cap_lift cap_a = Some (Cap_frame_cap (cap_frame_cap_lift cap_a)); cap_lift cap_b = Some (Cap_frame_cap (cap_frame_cap_lift cap_b))\<rbrakk> \<Longrightarrow> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (if (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 then 1 else 0) = (if cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 then 1 else 0) then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d)) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)) \<and> (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<noteq> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (x32 = w \<and> vmpage_size = vmpage_sizea \<and> x32 \<le> x32 + 2 ^ pageBitsForSize vmpage_size - 1 \<and> x31 = d) = 0)
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (5 subgoals):
 1. \<And>cap_b cap_a. \<lbrakk>capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> 0; capFSize_CL (cap_frame_cap_lift cap_b) \<noteq> 0; cap_lift cap_a = Some (Cap_frame_cap (cap_frame_cap_lift cap_a)); cap_lift cap_b = Some (Cap_frame_cap (cap_frame_cap_lift cap_b)); pageBitsForSize (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a))) < word_bits; cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) \<le> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) + 2 ^ pageBitsForSize (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a))) - 1; pageBitsForSize (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_b))) < word_bits; cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<le> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) + 2 ^ pageBitsForSize (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_b))) - 1\<rbrakk> \<Longrightarrow> (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) = 0 \<longrightarrow> (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 \<longrightarrow> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a)) = framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_b)) \<and> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<le> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) + 2 ^ pageBitsForSize (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a))) - 1) = 0) \<and> (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) \<noteq> 0 \<longrightarrow> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (\<not> to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b))) = 0) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a)) = framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_b)) \<and> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<le> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) + 2 ^ pageBitsForSize (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a))) - 1 \<and> \<not> to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b))) = 0))) \<and> (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a) \<noteq> 0 \<longrightarrow> (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) = 0 \<longrightarrow> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (\<not> to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a))) = 0) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a)) = framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_b)) \<and> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<le> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) + 2 ^ pageBitsForSize (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a))) - 1 \<and> \<not> to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a))) = 0)) \<and> (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b) \<noteq> 0 \<longrightarrow> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_a) = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<longrightarrow> (capFSize_CL (cap_frame_cap_lift cap_a) = capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a)) = to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b))) \<and> (capFSize_CL (cap_frame_cap_lift cap_a) \<noteq> capFSize_CL (cap_frame_cap_lift cap_b) \<longrightarrow> from_bool (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a)) = framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_b)) \<and> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) \<le> cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap_b) + 2 ^ pageBitsForSize (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap_a))) - 1 \<and> to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_a)) = to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap_b))) = 0)))
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 3. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 4. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 5. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal (4 subgoals):
 1. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))
 2. \<And>capa capb cap_b cap_a x31 x32 x33 x34 x35 x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) cap_a; ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capa = arch_capability.PageCap x31 x32 x33 x34 x35; capb = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capb. ccap_relation (capability.ArchObjectCap capb) cap_b \<and> Arch.sameRegionAs capa capb = Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))
 3. \<And>capa capb cap_b cap_a x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) capb)
 4. \<And>capa capb cap_b cap_a x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap_a; ccap_relation (capability.ArchObjectCap capb) cap_b; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); capAligned (capability.ArchObjectCap capb); capa = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>capa. ccap_relation (capability.ArchObjectCap capa) cap_a \<and> (\<exists>capba. ccap_relation (capability.ArchObjectCap capba) cap_b \<and> Arch.sameRegionAs capa capba = Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) capb) proof (prove)
goal:
No subgoals!