theory ArchRetype_AI

lemma valid_untyped_helper [Retype_AI_assms]:
  assumes valid_c : "s  \<turnstile> c"
  and   cte_at  : "cte_wp_at ((=) c) q s"
  and     tyunt: "ty \<noteq> Untyped"
  and   cover  : "range_cover ptr sz (obj_bits_api ty us) n"
  and   range  : "is_untyped_cap c \<Longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + of_nat (n * 2 ^ (obj_bits_api ty us)) - 1} = {}"
  and     pn   : "pspace_no_overlap_range_cover ptr sz s"
  and     cn   : "caps_no_overlap ptr sz s"
  and     vp   : "valid_pspace s"
  shows "valid_cap c
           (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)"
  (is "valid_cap c ?ns") proof - have obj_at_pres: "\<And>P x. obj_at P x s \<Longrightarrow> obj_at P x ?ns" by (clarsimp simp: obj_at_def dest: domI)
   (erule pspace_no_overlapC [OF pn _ _ cover vp]) note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
        Int_atLeastAtMost atLeastatMost_empty_iff have cover':"range_cover ptr sz (obj_bits (default_object ty dev us)) n" using cover tyunt by (clarsimp simp: obj_bits_dev_irr) show ?thesis using cover valid_c range usable_range_emptyD[where cap = c] cte_at apply (clarsimp simp: valid_cap_def elim!: obj_at_pres
                 split: cap.splits option.splits arch_cap.splits) defer apply (fastforce elim!: obj_at_pres) apply (fastforce elim!: obj_at_pres) apply (fastforce elim!: obj_at_pres) apply (rename_tac word nat1 nat2) apply (clarsimp simp: valid_untyped_def is_cap_simps obj_at_def split: if_split_asm) apply (thin_tac "\<forall>x. Q x" for Q) apply (frule retype_addrs_obj_range_subset_strong[where dev = dev,OF _ _ tyunt]) apply (simp add: obj_bits_dev_irr tyunt) apply (frule usable_range_subseteq) apply (simp add: is_cap_simps) apply (clarsimp simp: cap_aligned_def split: if_split_asm) apply (frule aligned_ranges_subset_or_disjoint) apply (erule retype_addrs_aligned[where sz = sz]) apply (simp add: range_cover_def) apply (simp add: range_cover_def word_bits_def) apply (simp add: range_cover_def) apply (clarsimp simp: default_obj_range Int_ac tyunt
                     split: if_split_asm) apply (elim disjE) apply (drule(2) subset_trans[THEN disjoint_subset2]) apply (drule Int_absorb2)+ apply (simp add: is_cap_simps free_index_of_def) apply simp apply (drule(1) disjoint_subset2[rotated]) apply (simp add: Int_ac) apply (thin_tac "\<forall>x. Q x" for Q) apply (frule retype_addrs_obj_range_subset[OF _ cover' tyunt]) apply (clarsimp simp: cap_aligned_def) apply (frule aligned_ranges_subset_or_disjoint) apply (erule retype_addrs_aligned[where sz = sz]) apply (simp add: range_cover_def) apply (simp add: range_cover_def word_bits_def) apply (simp add: range_cover_def) apply (clarsimp simp: default_obj_range Int_ac tyunt
                     split: if_split_asm) apply (erule disjE) apply (simp add: cte_wp_at_caps_of_state) apply (drule cn[unfolded caps_no_overlap_def,THEN bspec,OF ranI]) apply (simp add: p_assoc_help[symmetric]) apply (erule impE) apply blast  (* set arith *)
     apply blast  (* set arith *)
   apply blast  (* set arith  *)
   done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> c proof (state)
goal (1 subgoal):
 1. s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> c proof (prove)
goal (1 subgoal):
 1. \<And>P x. obj_at P x s \<Longrightarrow> obj_at P x (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (state)
this:
obj_at ?P ?x s \<Longrightarrow> obj_at ?P ?x (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)

goal (1 subgoal):
 1. s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> c proof (state)
this:
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)

goal (1 subgoal):
 1. s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> c proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits (default_object ty dev us)) n proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n
ty \<noteq> Untyped

goal (1 subgoal):
 1. range_cover ptr sz (obj_bits (default_object ty dev us)) n proof (state)
this:
range_cover ptr sz (obj_bits (default_object ty dev us)) n

goal (1 subgoal):
 1. s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> c proof (prove)
goal (1 subgoal):
 1. s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> c proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n
s \<turnstile> c
is_untyped_cap c \<Longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api ty us) - 1} = {}
\<lbrakk>cap_aligned c; is_untyped_cap c; usable_untyped_range c = {}\<rbrakk> \<Longrightarrow> 2 ^ cap_bits c \<le> free_index_of c
cte_wp_at ((=) c) q s

goal (1 subgoal):
 1. s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> c proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>(if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {} \<Longrightarrow> 2 ^ x23 \<le> free_index_of (UntypedCap x21 x22 x23 x24); cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); valid_untyped (UntypedCap x21 x22 x23 x24) s; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap x21 x22 x23 x24) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 2. \<And>x31 x32 x33 x34 x35 x31a x32a x33a x34a. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base\<rbrakk> \<Longrightarrow> (x31a \<longrightarrow> x31 \<and> x32 = x32a \<and> x33 = x33a \<and> x34 = x34a \<longrightarrow> (x35 = None \<longrightarrow> typ_at (AArch (ADeviceData x34a)) x32a (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> x33a \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> typ_at (AArch (ADeviceData x34a)) x32a (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> x33a \<in> valid_vm_rights \<and> vmsz_aligned b x34a)) \<and> (\<not> x31a \<longrightarrow> \<not> x31 \<and> x32 = x32a \<and> x33 = x33a \<and> x34 = x34a \<longrightarrow> (x35 = None \<longrightarrow> typ_at (AArch (AUserData x34a)) x32a (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> x33a \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> typ_at (AArch (AUserData x34a)) x32a (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> x33a \<in> valid_vm_rights \<and> vmsz_aligned b x34a))
 3. \<And>x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); (\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s; \<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20\<rbrakk> \<Longrightarrow> (x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)) \<and> ((\<exists>a b. x42 = Some (a, b)) \<longrightarrow> typ_at (AArch APageTable) x41 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>))
 4. \<And>x51 x52. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap x51 x52))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); (\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s; \<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> (x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)) \<and> ((\<exists>x2. x52 = Some x2) \<longrightarrow> typ_at (AArch APageDirectory) x51 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x31a x32a x33a x34a. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base\<rbrakk> \<Longrightarrow> (x31a \<longrightarrow> x31 \<and> x32 = x32a \<and> x33 = x33a \<and> x34 = x34a \<longrightarrow> (x35 = None \<longrightarrow> typ_at (AArch (ADeviceData x34a)) x32a (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> x33a \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> typ_at (AArch (ADeviceData x34a)) x32a (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> x33a \<in> valid_vm_rights \<and> vmsz_aligned b x34a)) \<and> (\<not> x31a \<longrightarrow> \<not> x31 \<and> x32 = x32a \<and> x33 = x33a \<and> x34 = x34a \<longrightarrow> (x35 = None \<longrightarrow> typ_at (AArch (AUserData x34a)) x32a (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> x33a \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> typ_at (AArch (AUserData x34a)) x32a (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> x33a \<in> valid_vm_rights \<and> vmsz_aligned b x34a))
 2. \<And>x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); (\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s; \<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20\<rbrakk> \<Longrightarrow> (x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)) \<and> ((\<exists>a b. x42 = Some (a, b)) \<longrightarrow> typ_at (AArch APageTable) x41 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>))
 3. \<And>x51 x52. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap x51 x52))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); (\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s; \<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> (x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)) \<and> ((\<exists>x2. x52 = Some x2) \<longrightarrow> typ_at (AArch APageDirectory) x51 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>))
 4. \<And>x21 x22 x23 x24. \<lbrakk>(if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {} \<Longrightarrow> 2 ^ x23 \<le> free_index_of (UntypedCap x21 x22 x23 x24); cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); valid_untyped (UntypedCap x21 x22 x23 x24) s; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap x21 x22 x23 x24) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); (\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s; \<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20\<rbrakk> \<Longrightarrow> (x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)) \<and> ((\<exists>a b. x42 = Some (a, b)) \<longrightarrow> typ_at (AArch APageTable) x41 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>))
 2. \<And>x51 x52. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap x51 x52))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); (\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s; \<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> (x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)) \<and> ((\<exists>x2. x52 = Some x2) \<longrightarrow> typ_at (AArch APageDirectory) x51 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>))
 3. \<And>x21 x22 x23 x24. \<lbrakk>(if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {} \<Longrightarrow> 2 ^ x23 \<le> free_index_of (UntypedCap x21 x22 x23 x24); cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); valid_untyped (UntypedCap x21 x22 x23 x24) s; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap x21 x22 x23 x24) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x51 x52. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap x51 x52))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); (\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s; \<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> (x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)) \<and> ((\<exists>x2. x52 = Some x2) \<longrightarrow> typ_at (AArch APageDirectory) x51 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>))
 2. \<And>x21 x22 x23 x24. \<lbrakk>(if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {} \<Longrightarrow> 2 ^ x23 \<le> free_index_of (UntypedCap x21 x22 x23 x24); cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); valid_untyped (UntypedCap x21 x22 x23 x24) s; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap x21 x22 x23 x24) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. \<lbrakk>(if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {} \<Longrightarrow> 2 ^ x23 \<le> free_index_of (UntypedCap x21 x22 x23 x24); cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); valid_untyped (UntypedCap x21 x22 x23 x24) s; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap x21 x22 x23 x24) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x21 word nat1 nat2. \<lbrakk>(if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; cap_aligned (UntypedCap x21 word nat1 nat2); valid_untyped (UntypedCap x21 word nat1 nat2) s; untyped_min_bits \<le> nat1; nat2 \<le> 2 ^ nat1; word \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap x21 word nat1 nat2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; cap_aligned (UntypedCap x21 word nat1 nat2); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p obj = {}; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; cap_aligned (UntypedCap x21 word nat1 nat2); untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; cap_aligned (UntypedCap x21 word nat1 nat2); untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> range_cover ptr (?sz473 x21 word nat1 nat2 p) (obj_bits_api ty us) n
 2. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; cap_aligned (UntypedCap x21 word nat1 nat2); untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; cap_aligned (UntypedCap x21 word nat1 nat2); untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; cap_aligned (UntypedCap x21 word nat1 nat2); untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap x21 word nat1 nat2)
 2. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; cap_aligned (UntypedCap x21 word nat1 nat2); untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; usable_untyped_range (UntypedCap x21 word nat1 nat2) \<subseteq> untyped_range (UntypedCap x21 word nat1 nat2)\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; cap_aligned (UntypedCap x21 word nat1 nat2); untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; usable_untyped_range (UntypedCap x21 word nat1 nat2) \<subseteq> untyped_range (UntypedCap x21 word nat1 nat2)\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> is_aligned (?p'482 x21 word nat1 nat2 p) (?n'482 x21 word nat1 nat2 p)
 2. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {?p'482 x21 word nat1 nat2 p..?p'482 x21 word nat1 nat2 p + 2 ^ ?n'482 x21 word nat1 nat2 p - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {?p'482 x21 word nat1 nat2 p..?p'482 x21 word nat1 nat2 p + 2 ^ ?n'482 x21 word nat1 nat2 p - 1} \<or> {?p'482 x21 word nat1 nat2 p..?p'482 x21 word nat1 nat2 p + 2 ^ ?n'482 x21 word nat1 nat2 p - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (5 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> is_aligned ptr (obj_bits_api ty us)
 2. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> sz < word_bits
 3. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> sz
 4. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 5. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (4 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> sz
 3. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 4. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> sz
 2. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 2. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {word..word + 2 ^ nat1 - 1} = {}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 2. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; is_aligned word nat1; nat1 < word_bits; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {word..word + 2 ^ nat1 - 1} = {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {p..p + 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {word..word + 2 ^ nat1 - 1} = {word + word_of_nat nat2..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 2. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1} \<and> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 nat2 p. \<lbrakk>{word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {} \<Longrightarrow> 2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 nat2); cte_wp_at ((=) (UntypedCap x21 word nat1 nat2)) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 nat2; untyped_min_bits \<le> nat1; word \<noteq> 0; nat2 < 2 ^ nat1; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} = {}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {word..word + 2 ^ nat1 - 1}; untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); cap_aligned (UntypedCap x21 word nat1 (2 ^ nat1)); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> is_aligned (?p'511 x21 word nat1 p x) (?n'511 x21 word nat1 p x)
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {?p'511 x21 word nat1 p x..?p'511 x21 word nat1 p x + 2 ^ ?n'511 x21 word nat1 p x - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {?p'511 x21 word nat1 p x..?p'511 x21 word nat1 p x + 2 ^ ?n'511 x21 word nat1 p x - 1} \<or> {?p'511 x21 word nat1 p x..?p'511 x21 word nat1 p x + 2 ^ ?n'511 x21 word nat1 p x - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (4 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> is_aligned ptr (obj_bits_api ty us)
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> sz < word_bits
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> sz
 4. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> sz
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> sz
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {word..word + 2 ^ nat1 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} = {} \<or> {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<or> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); caps_of_state s q = Some (UntypedCap x21 word nat1 (2 ^ nat1)); range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}; untyped_range (UntypedCap x21 word nat1 (2 ^ nat1)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range (UntypedCap x21 word nat1 (2 ^ nat1))\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}; {word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> {word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1}
 3. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; is_aligned word nat1; nat1 < word_bits; {word..word + 2 ^ nat1 - 1} \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1}
 2. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x21 word nat1 p x. \<lbrakk>2 ^ nat1 \<le> free_index_of (UntypedCap x21 word nat1 (2 ^ nat1)); cte_wp_at ((=) (UntypedCap x21 word nat1 (2 ^ nat1))) q s; range_cover ptr sz (obj_bits_api ty us) n; c = UntypedCap x21 word nat1 (2 ^ nat1); untyped_min_bits \<le> nat1; word \<noteq> 0; p \<in> set (retype_addrs ptr ty n us); {word..word + 2 ^ nat1 - 1} \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<noteq> {}; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> up_aligned_area ptr sz; is_aligned word nat1; nat1 < word_bits; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals! proof (state)
this:
s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> c

goal:
No subgoals!