theory Untyped_R

lemma retype_region_caps_overlap_reserved_ret:
  "\<lbrace>valid_pspace and valid_mdb and caps_no_overlap ptr sz and
    pspace_no_overlap_range_cover ptr sz and
    caps_overlap_reserved
      {ptr..ptr + of_nat n * 2^obj_bits_api (APIType_map2 (Inr ao')) us - 1} and
    (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and
    K (APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us) and
    K (range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n)\<rbrace>
   retype_region ptr n us (APIType_map2 (Inr ao')) dev
   \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. caps_overlap_reserved (untyped_range (default_cap
                            (APIType_map2 (Inr ao')) y us d)) s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:valid_def) apply (frule retype_region_ret[unfolded valid_def,simplified,THEN spec,THEN bspec]) apply clarsimp apply (erule use_valid[OF _ retype_region_caps_overlap_reserved]) apply clarsimp apply (intro conjI,simp_all) apply fastforce apply (case_tac ao') apply (simp_all add:APIType_map2_def) apply (rename_tac apiobject_type) apply (case_tac apiobject_type) apply (simp_all add:obj_bits_api_def ptr_add_def) apply (drule(1) range_cover_subset) apply (clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace and valid_mdb and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and K (APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n)\<rbrace> retype_region ptr n us (APIType_map2 (Inr ao')) dev \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. caps_overlap_reserved (untyped_range (default_cap (APIType_map2 (Inr ao')) y us d)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_pspace and valid_mdb and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and K (APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> retype_region ptr n us (APIType_map2 (Inr ao')) dev \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. caps_overlap_reserved (untyped_range (default_cap (APIType_map2 (Inr ao')) y us d)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b y aa ba. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us (APIType_map2 (Inr ao')) dev s); y \<in> set a; valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n\<rbrakk> \<Longrightarrow> caps_overlap_reserved (untyped_range (default_cap (APIType_map2 (Inr ao')) y us d)) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b y aa ba. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us (APIType_map2 (Inr ao')) dev s); y \<in> set a; valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; case (a, b) of (r, s') \<Rightarrow> r = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) [0..<n]\<rbrakk> \<Longrightarrow> caps_overlap_reserved (untyped_range (default_cap (APIType_map2 (Inr ao')) y us d)) b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba x. \<lbrakk>(map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) [0..<n], b) \<in> fst (retype_region ptr n us (APIType_map2 (Inr ao')) dev s); valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n\<rbrakk> \<Longrightarrow> caps_overlap_reserved (untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d)) b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n\<rbrakk> \<Longrightarrow> (valid_pspace and valid_mdb and pspace_no_overlap (up_aligned_area ptr (?sz26 s b aa ba x)) and caps_no_overlap ptr (?sz26 s b aa ba x) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} and (\<lambda>sa. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr (?sz26 s b aa ba x) \<subseteq> cap_range c \<and> cap_is_device c = dev) slot sa) and K (APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr (?sz26 s b aa ba x) (obj_bits_api (APIType_map2 (Inr ao')) us) n) and K (untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1})) s proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr (?sz26 s b aa ba x)) s \<and> caps_no_overlap ptr (?sz26 s b aa ba x) s \<and> (\<exists>a bb. cte_wp_at (\<lambda>c. up_aligned_area ptr (?sz26 s b aa ba x) \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, bb) s) \<and> range_cover ptr (?sz26 s b aa ba x) (obj_bits_api (APIType_map2 (Inr ao')) us) n \<and> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s
 2. \<And>s aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n\<rbrakk> \<Longrightarrow> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n\<rbrakk> \<Longrightarrow> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} proof (prove)
goal (7 subgoals):
 1. \<And>s aa ba x x1. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n; ao' = APIObjectType x1\<rbrakk> \<Longrightarrow> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}
 2. \<And>s aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n; ao' = SmallPageObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}
 3. \<And>s aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n; ao' = LargePageObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}
 4. \<And>s aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n; ao' = SectionObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}
 5. \<And>s aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n; ao' = SuperSectionObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}
 6. \<And>s aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n; ao' = PageTableObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}
 7. \<And>s aa ba x. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; x < n; ao' = PageDirectoryObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (APIType_map2 (Inr ao')) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba x x1. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us) n; x < n; ao' = APIObjectType x1\<rbrakk> \<Longrightarrow> untyped_range (default_cap (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) (ptr_add ptr (x * 2 ^ obj_bits_api (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba x apiobject_type. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us) n; x < n; ao' = APIObjectType apiobject_type\<rbrakk> \<Longrightarrow> untyped_range (default_cap (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) (ptr_add ptr (x * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} proof (prove)
goal (5 subgoals):
 1. \<And>s aa ba x apiobject_type. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us) n; x < n; ao' = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> untyped_range (default_cap (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) (ptr_add ptr (x * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1}
 2. \<And>s aa ba x apiobject_type. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us) n; x < n; ao' = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) (ptr_add ptr (x * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1}
 3. \<And>s aa ba x apiobject_type. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us) n; x < n; ao' = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) (ptr_add ptr (x * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1}
 4. \<And>s aa ba x apiobject_type. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us) n; x < n; ao' = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) (ptr_add ptr (x * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1}
 5. \<And>s aa ba x apiobject_type. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us) n; x < n; ao' = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> untyped_range (default_cap (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) (ptr_add ptr (x * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us)) us d) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> Structures_A.apiobject_type.Untyped | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Structures_A.apiobject_type.TCBObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Structures_A.apiobject_type.EndpointObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Structures_A.apiobject_type.NotificationObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Structures_A.apiobject_type.CapTableObject) us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba x apiobject_type. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; range_cover ptr sz us n; x < n; ao' = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ us \<le> ptr + word_of_nat x * 2 ^ us + 2 ^ us - 1 \<longrightarrow> ptr \<le> ptr + word_of_nat x * 2 ^ us \<and> ptr + word_of_nat x * 2 ^ us + 2 ^ us - 1 \<le> ptr + word_of_nat n * 2 ^ us - 1 proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba x apiobject_type. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; x < n; ao' = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s aa ba x apiobject_type. \<lbrakk>valid_pspace s; valid_mdb s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ us - 1} s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) s; x < n; ao' = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped; {ptr + word_of_nat x * 2 ^ us..ptr + word_of_nat x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ us \<le> ptr + word_of_nat x * 2 ^ us + 2 ^ us - 1 \<longrightarrow> ptr \<le> ptr + word_of_nat x * 2 ^ us \<and> ptr + word_of_nat x * 2 ^ us + 2 ^ us - 1 \<le> ptr + word_of_nat n * 2 ^ us - 1 proof (prove)
goal:
No subgoals!