theory PageTableDuplicates

lemma page_directory_at_set_list:
  "\<lbrakk>page_directory_at' ptr s;pspace_aligned' s;sz \<le> pdBits;
   p && ~~ mask pdBits = ptr; is_aligned p sz; 2 \<le> sz\<rbrakk> \<Longrightarrow>
  set [p , p + 4 .e. p + mask sz] =
  {x. pde_at' x s \<and> x && ~~ mask sz = p}" apply (clarsimp simp:page_directory_at'_def pdBits_def pdeBits_def) apply (rule set_eqI) apply (rule iffI) apply (subst (asm) upto_enum_step_subtract) apply (simp add:field_simps mask_def) apply (erule is_aligned_no_overflow) apply (clarsimp simp:set_upto_enum_step_4
           image_def pageBits_def) apply (drule_tac x= "((p && mask 14) >> 2) + xb" in spec) apply (erule impE) apply (rule is_aligned_plus_bound[where lz = 12 and sz = "sz - 2" ,simplified]) apply (rule is_aligned_shiftr) apply (rule is_aligned_andI1) apply (subgoal_tac "sz - 2 + 2 = sz") apply simp apply simp apply (simp add:field_simps) apply (simp add:shiftr_mask2) apply (simp add:mask_def not_less word_bits_def) apply (rule shiftr_less_t2n[where m = 12,simplified]) apply (rule le_less_trans[OF _ mask_lt_2pn]) apply (simp add:word_and_le1) apply simp apply (simp add:word_bits_def) apply (simp add:word_shiftl_add_distrib) apply (subst (asm) shiftr_shiftl1) apply simp+ apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) apply (rule is_aligned_weaken) apply (erule is_aligned_andI1) apply simp apply (simp add:mask_out_sub_mask field_simps) apply (clarsimp simp:typ_at'_def mask_add_aligned
     ko_wp_at'_def dom_def) apply (rule less_mask_eq[symmetric]) apply (subst (asm) shiftr_mask2) apply simp apply (simp add:shiftl_less_t2n word_shiftl_add_distrib
     word_bits_def mask_def shiftr_mask2) apply (clarsimp simp:objBits_simps pageBits_def archObjSize_def
     split:Structures_H.kernel_object.splits arch_kernel_object.splits) apply (subst upto_enum_step_subtract) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask]) apply (rule le_refl) apply (simp add:mask_lt_2pn word_bits_def) apply (simp add:image_def) apply (rule_tac x = "x && mask sz" in bexI) apply (simp add:mask_out_sub_mask) apply (simp add:set_upto_enum_step_4 image_def) apply (rule_tac x = "x && mask sz >> 2" in bexI) apply (subst shiftr_shiftl1) apply simp apply simp apply (subst is_aligned_neg_mask_eq) apply (rule is_aligned_andI1) apply (clarsimp simp: typ_at'_def ko_wp_at'_def
      dest!: koTypeOf_pde) apply (drule pspace_alignedD') apply simp apply (simp add:objBits_simps archObjSize_def pdeBits_def) apply simp apply clarsimp apply (rule le_shiftr) apply (simp add:word_and_le1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_directory_at' ptr s; pspace_aligned' s; sz \<le> pdBits; p && ~~ mask pdBits = ptr; is_aligned p sz; 2 \<le> sz\<rbrakk> \<Longrightarrow> set [p , p + 4 .e. p + mask sz] = {x. pde_at' x s \<and> x && ~~ mask sz = p} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s\<rbrakk> \<Longrightarrow> set [p , p + 4 .e. p + mask sz] = {x. pde_at' x s \<and> x && ~~ mask sz = p} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s\<rbrakk> \<Longrightarrow> (x \<in> set [p , p + 4 .e. p + mask sz]) = (x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> set [p , p + 4 .e. p + mask sz]\<rbrakk> \<Longrightarrow> x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s\<rbrakk> \<Longrightarrow> p \<le> p + mask sz
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> set (map ((+) p) [0 , p + 4 - p .e. p + mask sz - p])\<rbrakk> \<Longrightarrow> x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && 0xFFFFC000; \<forall>y<0x1000. pde_at' ((y << 2) + (p && 0xFFFFC000)) s\<rbrakk> \<Longrightarrow> p \<le> p + 2 ^ sz - 1
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> set (map ((+) p) [0 , p + 4 - p .e. p + mask sz - p])\<rbrakk> \<Longrightarrow> x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> set (map ((+) p) [0 , p + 4 - p .e. p + mask sz - p])\<rbrakk> \<Longrightarrow> x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; (p && mask 14 >> 2) + xb < 0x1000 \<longrightarrow> pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (3 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> (p && mask 14 >> 2) + xb < 0x1000
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (7 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> is_aligned (p && mask 14 >> 2) (sz - 2)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 \<le> 12
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> xb < 2 ^ (sz - 2)
 4. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 >> 2 < 0x1000
 5. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 6. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 7. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (7 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> is_aligned (p && mask 14) (sz - 2 + 2)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 \<le> 12
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> xb < 2 ^ (sz - 2)
 4. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 >> 2 < 0x1000
 5. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 6. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 7. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (7 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> is_aligned p (sz - 2 + 2)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 \<le> 12
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> xb < 2 ^ (sz - 2)
 4. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 >> 2 < 0x1000
 5. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 6. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 7. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (8 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; sz - 2 + 2 = sz\<rbrakk> \<Longrightarrow> is_aligned p (sz - 2 + 2)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 + 2 = sz
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 \<le> 12
 4. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> xb < 2 ^ (sz - 2)
 5. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 >> 2 < 0x1000
 6. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 7. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 8. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (7 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 + 2 = sz
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 \<le> 12
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> xb < 2 ^ (sz - 2)
 4. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 >> 2 < 0x1000
 5. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 6. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 7. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (6 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 \<le> 12
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> xb < 2 ^ (sz - 2)
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 >> 2 < 0x1000
 4. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 5. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 6. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (5 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> xb < 2 ^ (sz - 2)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 >> 2 < 0x1000
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 4. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 5. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (5 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask (sz - 2)\<rbrakk> \<Longrightarrow> xb < 2 ^ (sz - 2)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 >> 2 < 0x1000
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 4. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 5. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (4 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 >> 2 < 0x1000
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 4. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (4 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 < 2 ^ (2 + 12)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 4. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (5 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> p && mask 14 \<le> mask (2 + 12)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> 2 + 12 < LENGTH(32)
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 4. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 5. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (4 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> 2 + 12 < LENGTH(32)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 4. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (3 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> sz - 2 < word_bits
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2) + xb << 2)) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14 >> 2 << 2) + (xb << 2))) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (3 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + (((p && mask 14 >> 2 - 2) && ~~ mask 2) + (xb << 2))) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + (((p && mask 14) && ~~ mask 2) + (xb << 2))) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (3 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> is_aligned (p && mask 14) 2
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14) + (xb << 2))) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (4 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> is_aligned (p && mask 14) (?x124 xb)
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> 2 \<le> ?x124 xb
 3. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14) + (xb << 2))) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 4. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (3 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2\<rbrakk> \<Longrightarrow> 2 \<le> sz
 2. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14) + (xb << 2))) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; xb \<le> mask sz >> 2; pde_at' ((p && ~~ mask 14) + ((p && mask 14) + (xb << 2))) s\<rbrakk> \<Longrightarrow> pde_at' (p + (xb << 2)) s \<and> p + (xb << 2) && ~~ mask sz = p
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr + (p && mask 14) = p; xb \<le> mask sz >> 2; pde_at' (p + (xb << 2)) s\<rbrakk> \<Longrightarrow> xb << 2 = p + (xb << 2) && mask sz
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb ko. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr + (p && mask 14) = p; xb \<le> mask sz >> 2; ksPSpace s (p + (xb << 2)) = Some ko; is_aligned (p + (xb << 2)) (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear (p + (xb << 2)) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> xb << 2 = (xb << 2) && mask sz
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb ko. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr + (p && mask 14) = p; xb \<le> mask sz >> 2; ksPSpace s (p + (xb << 2)) = Some ko; is_aligned (p + (xb << 2)) (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear (p + (xb << 2)) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> xb << 2 < 2 ^ sz
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (3 subgoals):
 1. \<And>xb ko. \<lbrakk>ksPSpace s (p + (xb << 2)) = Some ko; is_aligned (p + (xb << 2)) (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear (p + (xb << 2)) (objBitsKO ko) s; pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr + (p && mask 14) = p\<rbrakk> \<Longrightarrow> sz \<le> LENGTH(32)
 2. \<And>xb ko. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr + (p && mask 14) = p; xb \<le> mask (sz - 2); ksPSpace s (p + (xb << 2)) = Some ko; is_aligned (p + (xb << 2)) (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear (p + (xb << 2)) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> xb << 2 < 2 ^ sz
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>xb ko. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr + (p && mask 14) = p; xb \<le> mask (sz - 2); ksPSpace s (p + (xb << 2)) = Some ko; is_aligned (p + (xb << 2)) (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear (p + (xb << 2)) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> xb << 2 < 2 ^ sz
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; is_aligned p sz; 2 \<le> sz; ptr = p && ~~ mask 14; \<forall>y<0x1000. pde_at' ((p && ~~ mask 14) + (y << 2)) s; x \<in> {x. pde_at' x s \<and> x && ~~ mask sz = p}\<rbrakk> \<Longrightarrow> x \<in> set [p , p + 4 .e. p + mask sz] proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x \<in> set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask sz \<le> (x && ~~ mask sz) + mask sz
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x \<in> set (map ((+) (x && ~~ mask sz)) [0 , (x && ~~ mask sz) + 4 - (x && ~~ mask sz) .e. (x && ~~ mask sz) + mask sz - (x && ~~ mask sz)]) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> ?sz144 x \<le> sz
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> mask sz < 2 ^ ?sz144 x
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x \<in> set (map ((+) (x && ~~ mask sz)) [0 , (x && ~~ mask sz) + 4 - (x && ~~ mask sz) .e. (x && ~~ mask sz) + mask sz - (x && ~~ mask sz)]) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> mask sz < 2 ^ sz
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x \<in> set (map ((+) (x && ~~ mask sz)) [0 , (x && ~~ mask sz) + 4 - (x && ~~ mask sz) .e. (x && ~~ mask sz) + mask sz - (x && ~~ mask sz)]) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x \<in> set (map ((+) (x && ~~ mask sz)) [0 , (x && ~~ mask sz) + 4 - (x && ~~ mask sz) .e. (x && ~~ mask sz) + mask sz - (x && ~~ mask sz)]) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> \<exists>xa\<in>set [0 , 4 .e. mask sz]. x = (x && ~~ mask sz) + xa proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x = (x && ~~ mask sz) + (x && mask sz)
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz \<in> set [0 , 4 .e. mask sz] proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz \<in> set [0 , 4 .e. mask sz] proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{..mask sz >> 2}. x && mask sz = xa << 2 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = x && mask sz >> 2 << 2
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = (x && mask sz >> 2 - 2) && ~~ mask 2
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = (x && mask sz >> 2 - 2) && ~~ mask 2
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = (x && mask sz) && ~~ mask 2
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> is_aligned (x && mask sz) 2
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = x && mask sz
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = x && mask sz
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (3 subgoals):
 1. \<And>x pde. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. \<exists>ko. ksPSpace s (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) = Some ko \<and> is_aligned (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) (objBitsKO ko) s; p = x && ~~ mask sz; ksPSpace s x = Some (KOArch (KOPDE pde)); is_aligned x (objBitsKO (KOArch (KOPDE pde))); ps_clear x (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = x && mask sz
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (4 subgoals):
 1. \<And>x pde. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. \<exists>ko. ksPSpace s (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) = Some ko \<and> is_aligned (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) (objBitsKO ko) s; p = x && ~~ mask sz; is_aligned x (objBitsKO (KOArch (KOPDE pde))); ps_clear x (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<And>x pde. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. \<exists>ko. ksPSpace s (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) = Some ko \<and> is_aligned (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) (objBitsKO ko) s; p = x && ~~ mask sz; is_aligned x (objBitsKO (KOArch (KOPDE pde))); ps_clear x (objBitsKO (KOArch (KOPDE pde))) s; is_aligned x (objBitsKO (KOArch (KOPDE pde)))\<rbrakk> \<Longrightarrow> is_aligned x 2
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = x && mask sz
 4. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (3 subgoals):
 1. \<And>x pde. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. \<exists>ko. ksPSpace s (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) = Some ko \<and> is_aligned (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) (objBitsKO ko) s; p = x && ~~ mask sz; is_aligned x (objBitsKO (KOArch (KOPDE pde))); ps_clear x (objBitsKO (KOArch (KOPDE pde))) s; is_aligned x (objBitsKO (KOArch (KOPDE pde)))\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = x && mask sz
 3. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz = x && mask sz
 2. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<in> {..mask sz >> 2} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz >> 2 \<le> mask sz >> 2 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' s; sz \<le> 14; 2 \<le> sz; ptr = (x && ~~ mask sz) && ~~ mask 14; \<forall>y<0x1000. pde_at' (((x && ~~ mask sz) && ~~ mask 14) + (y << 2)) s; pde_at' x s; p = x && ~~ mask sz\<rbrakk> \<Longrightarrow> x && mask sz \<le> mask sz proof (prove)
goal:
No subgoals!