theory CSpace_I

lemma sameObjectAs_def2:
 "sameObjectAs cap cap' = (\<lambda>cap cap'.
     (cap = cap'
          \<and> (\<not> isNullCap cap \<and> \<not> isZombie cap
              \<and> \<not> isUntypedCap cap)
          \<and> (\<not> isNullCap cap' \<and> \<not> isZombie cap'
              \<and> \<not> isUntypedCap cap')
          \<and> (isArchPageCap cap \<longrightarrow> capRange cap \<noteq> {})
          \<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {})))
           (capMasterCap cap) (capMasterCap cap')" apply (simp add: sameObjectAs_def sameRegionAs_def2
                   isCap_simps capMasterCap_def
            split: capability.split) apply (clarsimp simp: ARM_H.sameObjectAs_def isCap_simps
                 split: arch_capability.split cong: if_cong) apply (clarsimp simp: ARM_H.sameRegionAs_def isCap_simps
             split del: if_split cong: if_cong) apply (simp add: capRange_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameObjectAs cap cap' = (capMasterCap cap = capMasterCap cap' \<and> (\<not> isNullCap (capMasterCap cap) \<and> \<not> isZombie (capMasterCap cap) \<and> \<not> isUntypedCap (capMasterCap cap)) \<and> (\<not> isNullCap (capMasterCap cap') \<and> \<not> isZombie (capMasterCap cap') \<and> \<not> isUntypedCap (capMasterCap cap')) \<and> (isArchPageCap (capMasterCap cap) \<longrightarrow> capRange (capMasterCap cap) \<noteq> {}) \<and> (isArchPageCap (capMasterCap cap') \<longrightarrow> capRange (capMasterCap cap') \<noteq> {})) proof (prove)
goal (1 subgoal):
 1. \<forall>x8. cap' = capability.ArchObjectCap x8 \<longrightarrow> (\<forall>x8a. cap = capability.ArchObjectCap x8a \<longrightarrow> Arch.sameObjectAs x8a x8 = ((case x8a of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> x8a | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = (case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> x8 | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) \<and> ((\<exists>d ref rghts sz data. (case x8a of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> x8a | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageCap d ref rghts sz data) \<longrightarrow> capRange (capability.ArchObjectCap (case x8a of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> x8a | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None)) \<noteq> {}) \<and> ((\<exists>d ref rghts sz data. (case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> x8 | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageCap d ref rghts sz data) \<longrightarrow> capRange (capability.ArchObjectCap (case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> x8 | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None)) \<noteq> {}))) proof (prove)
goal (1 subgoal):
 1. \<And>x8. (\<forall>x11 x12. x8 = arch_capability.ASIDPoolCap x11 x12 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> (\<forall>x8. (\<forall>x11a x12a. x8 = arch_capability.ASIDPoolCap x11a x12a \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11a x12a) \<longrightarrow> Arch.sameRegionAs (arch_capability.ASIDPoolCap x11a x12a) (arch_capability.ASIDPoolCap x11 x12) = (x11a = x11)) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> cap = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> \<not> Arch.sameRegionAs arch_capability.ASIDControlCap (arch_capability.ASIDPoolCap x11 x12)) \<and> (\<forall>x31 x32 x33 x34 x35. x8 = arch_capability.PageCap x31 x32 x33 x34 x35 \<longrightarrow> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> x31) \<and> (cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.ASIDPoolCap x11 x12))) \<and> (\<forall>x41 x42. x8 = arch_capability.PageTableCap x41 x42 \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) (arch_capability.ASIDPoolCap x11 x12)) \<and> (\<forall>x51 x52. x8 = arch_capability.PageDirectoryCap x51 x52 \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) (arch_capability.ASIDPoolCap x11 x12)))) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> cap' = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> (\<forall>x8. (\<forall>x11 x12. x8 = arch_capability.ASIDPoolCap x11 x12 \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.ASIDPoolCap x11 x12) arch_capability.ASIDControlCap) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> cap = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> Arch.sameRegionAs arch_capability.ASIDControlCap arch_capability.ASIDControlCap) \<and> (\<forall>x31 x32 x33 x34 x35. x8 = arch_capability.PageCap x31 x32 x33 x34 x35 \<longrightarrow> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> x31) \<and> (cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) arch_capability.ASIDControlCap)) \<and> (\<forall>x41 x42. x8 = arch_capability.PageTableCap x41 x42 \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) arch_capability.ASIDControlCap) \<and> (\<forall>x51 x52. x8 = arch_capability.PageDirectoryCap x51 x52 \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) arch_capability.ASIDControlCap))) \<and> (\<forall>x31 x32 x33 x34 x35. x8 = arch_capability.PageCap x31 x32 x33 x34 x35 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> (\<forall>x8. (\<forall>x11 x12. x8 = arch_capability.ASIDPoolCap x11 x12 \<longrightarrow> (cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.ASIDPoolCap x11 x12) (arch_capability.PageCap x31 x32 x33 x34 x35)) \<and> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> x31)) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> (cap = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> \<not> Arch.sameRegionAs arch_capability.ASIDControlCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<and> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> x31)) \<and> (\<forall>x31a x32a x33a x34a x35a. x8 = arch_capability.PageCap x31a x32a x33a x34a x35a \<longrightarrow> (cap = capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33a x34a x35a) \<longrightarrow> (x32a = x32 \<and> x34a = x34 \<and> x32a \<le> x32a + 2 ^ pageBitsForSize x34a - 1 \<and> x31a = x31) = (x31a = x31 \<and> x32a = x32 \<and> x34a = x34 \<and> capRange (capability.ArchObjectCap (arch_capability.PageCap x31a x32a VMReadWrite x34a None)) \<noteq> {} \<and> capRange (capability.ArchObjectCap (arch_capability.PageCap x31 x32 VMReadWrite x34 None)) \<noteq> {})) \<and> ((\<forall>d. x31a = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33a x34a x35a) \<longrightarrow> Arch.sameRegionAs (arch_capability.PageCap x31a x32a x33a x34a x35a) (arch_capability.PageCap x31 x32 x33 x34 x35) = (x31a = x31 \<and> x32a = x32 \<and> x34a = x34 \<and> x31a)) \<and> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33a x34a x35a) \<longrightarrow> Arch.sameRegionAs (arch_capability.PageCap x31a x32a x33a x34a x35a) (arch_capability.PageCap x31 x32 x33 x34 x35) = (x31a = x31 \<and> x32a = x32 \<and> x34a = x34 \<and> x31))) \<and> (\<forall>x41 x42. x8 = arch_capability.PageTableCap x41 x42 \<longrightarrow> (cap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) (arch_capability.PageCap x31 x32 x33 x34 x35)) \<and> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> x31)) \<and> (\<forall>x51 x52. x8 = arch_capability.PageDirectoryCap x51 x52 \<longrightarrow> (cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) (arch_capability.PageCap x31 x32 x33 x34 x35)) \<and> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> x31)))) \<and> (\<forall>x41 x42. x8 = arch_capability.PageTableCap x41 x42 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> (\<forall>x8. (\<forall>x11 x12. x8 = arch_capability.ASIDPoolCap x11 x12 \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.ASIDPoolCap x11 x12) (arch_capability.PageTableCap x41 x42)) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> cap = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> \<not> Arch.sameRegionAs arch_capability.ASIDControlCap (arch_capability.PageTableCap x41 x42)) \<and> (\<forall>x31 x32 x33 x34 x35. x8 = arch_capability.PageCap x31 x32 x33 x34 x35 \<longrightarrow> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> x31) \<and> (cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageTableCap x41 x42))) \<and> (\<forall>x41a x42a. x8 = arch_capability.PageTableCap x41a x42a \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageTableCap x41a x42a) \<longrightarrow> Arch.sameRegionAs (arch_capability.PageTableCap x41a x42a) (arch_capability.PageTableCap x41 x42) = (x41a = x41)) \<and> (\<forall>x51 x52. x8 = arch_capability.PageDirectoryCap x51 x52 \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageDirectoryCap x51 x52) (arch_capability.PageTableCap x41 x42)))) \<and> (\<forall>x51 x52. x8 = arch_capability.PageDirectoryCap x51 x52 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> (\<forall>x8. (\<forall>x11 x12. x8 = arch_capability.ASIDPoolCap x11 x12 \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.ASIDPoolCap x11 x12) (arch_capability.PageDirectoryCap x51 x52)) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> cap = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> \<not> Arch.sameRegionAs arch_capability.ASIDControlCap (arch_capability.PageDirectoryCap x51 x52)) \<and> (\<forall>x31 x32 x33 x34 x35. x8 = arch_capability.PageCap x31 x32 x33 x34 x35 \<longrightarrow> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> x31) \<and> (cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageCap x31 x32 x33 x34 x35) (arch_capability.PageDirectoryCap x51 x52))) \<and> (\<forall>x41 x42. x8 = arch_capability.PageTableCap x41 x42 \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> \<not> Arch.sameRegionAs (arch_capability.PageTableCap x41 x42) (arch_capability.PageDirectoryCap x51 x52)) \<and> (\<forall>x51a x52a. x8 = arch_capability.PageDirectoryCap x51a x52a \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51a x52a) \<longrightarrow> Arch.sameRegionAs (arch_capability.PageDirectoryCap x51a x52a) (arch_capability.PageDirectoryCap x51 x52) = (x51a = x51)))) proof (prove)
goal (1 subgoal):
 1. \<And>x8. (\<forall>x11 x12. x8 = arch_capability.ASIDPoolCap x11 x12 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> (\<forall>x31. (\<forall>d. x31 = (\<not> d)) \<longrightarrow> (\<exists>x32 x33 x34 x35. cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<longrightarrow> x31)) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> cap' = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> (\<forall>x31. (\<forall>d. x31 = (\<not> d)) \<longrightarrow> (\<exists>x32 x33 x34 x35. cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<longrightarrow> x31)) \<and> (\<forall>x31 x32 x33 x34 x35. x8 = arch_capability.PageCap x31 x32 x33 x34 x35 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> (\<forall>x8. (\<forall>x11 x12. x8 = arch_capability.ASIDPoolCap x11 x12 \<longrightarrow> (\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> x31) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> (\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> x31) \<and> (\<forall>x31a x32a x33 x34a x35. x8 = arch_capability.PageCap x31a x32a x33 x34a x35 \<longrightarrow> (cap = capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33 x34a x35) \<longrightarrow> (x32a = x32 \<and> x34a = x34 \<and> x32a \<le> x32a + 2 ^ pageBitsForSize x34a - 1 \<and> x31a = x31) = (x31a = x31 \<and> x32a = x32 \<and> x34a = x34 \<and> capRange (capability.ArchObjectCap (arch_capability.PageCap x31a x32a VMReadWrite x34a None)) \<noteq> {} \<and> capRange (capability.ArchObjectCap (arch_capability.PageCap x31 x32 VMReadWrite x34 None)) \<noteq> {})) \<and> ((\<forall>d. x31a = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33 x34a x35) \<longrightarrow> (let topB = x32 + 2 ^ pageBitsForSize x34 - 1 in x32a \<le> x32 \<and> topB \<le> x32a + 2 ^ pageBitsForSize x34a - 1 \<and> x32 \<le> topB) = (x31a = x31 \<and> x32a = x32 \<and> x34a = x34 \<and> x31a)) \<and> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33 x34a x35) \<longrightarrow> (let topB = x32 + 2 ^ pageBitsForSize x34 - 1 in x32a \<le> x32 \<and> topB \<le> x32a + 2 ^ pageBitsForSize x34a - 1 \<and> x32 \<le> topB) = (x31a = x31 \<and> x32a = x32 \<and> x34a = x34 \<and> x31))) \<and> (\<forall>x41 x42. x8 = arch_capability.PageTableCap x41 x42 \<longrightarrow> (\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> x31) \<and> (\<forall>x51 x52. x8 = arch_capability.PageDirectoryCap x51 x52 \<longrightarrow> (\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> x31))) \<and> (\<forall>x41 x42. x8 = arch_capability.PageTableCap x41 x42 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> (\<forall>x31. (\<forall>d. x31 = (\<not> d)) \<longrightarrow> (\<exists>x32 x33 x34 x35. cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<longrightarrow> x31)) \<and> (\<forall>x51 x52. x8 = arch_capability.PageDirectoryCap x51 x52 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> (\<forall>x31. (\<forall>d. x31 = (\<not> d)) \<longrightarrow> (\<exists>x32 x33 x34 x35. cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<longrightarrow> x31)) proof (prove)
goal (1 subgoal):
 1. \<And>x8. (\<forall>x11 x12. x8 = arch_capability.ASIDPoolCap x11 x12 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> (\<forall>x31. (\<forall>d. x31 = (\<not> d)) \<longrightarrow> (\<exists>x32 x33 x34 x35. cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<longrightarrow> x31)) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> cap' = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> (\<forall>x31. (\<forall>d. x31 = (\<not> d)) \<longrightarrow> (\<exists>x32 x33 x34 x35. cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<longrightarrow> x31)) \<and> (\<forall>x31 x32 x33 x34 x35. x8 = arch_capability.PageCap x31 x32 x33 x34 x35 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> (\<forall>x8. (\<forall>x11 x12. x8 = arch_capability.ASIDPoolCap x11 x12 \<longrightarrow> (\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> x31) \<and> (x8 = arch_capability.ASIDControlCap \<longrightarrow> (\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap arch_capability.ASIDControlCap \<longrightarrow> x31) \<and> (\<forall>x31a x32a x33 x34a x35. x8 = arch_capability.PageCap x31a x32a x33 x34a x35 \<longrightarrow> (cap = capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33 x34a x35) \<longrightarrow> (x32a = x32 \<and> x34a = x34 \<and> x32a \<le> x32a + 2 ^ pageBitsForSize x34a - 1 \<and> x31a = x31) = (x31a = x31 \<and> x32a = x32 \<and> x34a = x34 \<and> x32a \<le> x32a + 2 ^ pageBitsForSize x34a - 1 \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1)) \<and> ((\<forall>d. x31a = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33 x34a x35) \<longrightarrow> (let topB = x32 + 2 ^ pageBitsForSize x34 - 1 in x32a \<le> x32 \<and> topB \<le> x32a + 2 ^ pageBitsForSize x34a - 1 \<and> x32 \<le> topB) = (x31a = x31 \<and> x32a = x32 \<and> x34a = x34 \<and> x31a)) \<and> ((\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap x31a x32a x33 x34a x35) \<longrightarrow> (let topB = x32 + 2 ^ pageBitsForSize x34 - 1 in x32a \<le> x32 \<and> topB \<le> x32a + 2 ^ pageBitsForSize x34a - 1 \<and> x32 \<le> topB) = (x31a = x31 \<and> x32a = x32 \<and> x34a = x34 \<and> x31))) \<and> (\<forall>x41 x42. x8 = arch_capability.PageTableCap x41 x42 \<longrightarrow> (\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> x31) \<and> (\<forall>x51 x52. x8 = arch_capability.PageDirectoryCap x51 x52 \<longrightarrow> (\<forall>d. x31 = (\<not> d)) \<longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> x31))) \<and> (\<forall>x41 x42. x8 = arch_capability.PageTableCap x41 x42 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42) \<longrightarrow> (\<forall>x31. (\<forall>d. x31 = (\<not> d)) \<longrightarrow> (\<exists>x32 x33 x34 x35. cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<longrightarrow> x31)) \<and> (\<forall>x51 x52. x8 = arch_capability.PageDirectoryCap x51 x52 \<longrightarrow> cap' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> (\<forall>x31. (\<forall>d. x31 = (\<not> d)) \<longrightarrow> (\<exists>x32 x33 x34 x35. cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<longrightarrow> x31)) proof (prove)
goal:
No subgoals!