theory Retype_R

lemma new_range_subset:
  assumes
        cover: "range_cover ptr sz (objBitsKO ko) n"
    and addr: "x \<in> set (new_cap_addrs n ptr ko)"
  shows       "{x .. x + 2 ^ (objBitsKO ko) - 1} \<subseteq> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}"
  (is "?lhs \<subseteq> ?rhs") proof - have base_in: "x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}" by (rule set_mp[OF new_cap_addrs_subset[OF cover] addr]) have aligned: "is_aligned x (objBitsKO ko)" apply (insert cover) apply (clarsimp simp:range_cover_def) apply (drule new_cap_addrs_aligned) apply (erule bspec[OF _ addr]) done show ?thesis using base_in aligned addr apply (intro range_subsetI) apply (clarsimp simp:ptr_add_def field_simps)+ apply (simp add:x_power_minus_1) apply (clarsimp simp:new_cap_addrs_def) apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz"]) apply (subst add.commute) apply (subst add.assoc) apply (subst add.assoc) apply (rule word_plus_mono_right) apply (simp add:mask_2pm1[symmetric]) apply (rule iffD2[OF shiftr_mask_cmp[where c = "objBitsKO ko"]]) apply (insert cover) apply (simp add:range_cover_def) apply (simp add:range_cover_def word_bits_def) apply (subst aligned_shift') apply (simp add:mask_lt_2pn range_cover_def word_bits_def ) apply (drule is_aligned_addD1) apply (simp add:range_cover_def) apply (rule aligned_add_aligned) apply (rule aligned_already_mask) apply (fastforce simp:range_cover_def) apply (simp_all add: range_cover_def)[3] apply (subst shiftr_mask2[symmetric]) apply (simp add:range_cover_def word_bits_def) apply (rule le_shiftr) apply (subst le_mask_iff_lt_2n[THEN iffD1]) apply (simp add:range_cover_def word_bits_def) apply (clarsimp simp:word_less_nat_alt) apply (rule le_less_trans[OF unat_plus_gt]) apply (frule(1) range_cover.range_cover_compare) apply (clarsimp simp:shiftl_t2n mult.commute range_cover_def) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask]) apply (rule le_refl) apply (simp add:range_cover_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (state)
goal (1 subgoal):
 1. {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)} proof (state)
this:
x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}

goal (1 subgoal):
 1. {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. is_aligned x (objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO ko) n \<Longrightarrow> is_aligned x (objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO ko); sz < 32; objBitsKO ko \<le> sz; n + unat (ptr && mask sz >> objBitsKO ko) \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < 32; objBitsKO ko \<le> sz; n + unat (ptr && mask sz >> objBitsKO ko) \<le> 2 ^ (sz - objBitsKO ko); \<forall>x\<in>set (new_cap_addrs ?n4 ptr ko). is_aligned x (objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO ko) proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned x (objBitsKO ko)

goal (1 subgoal):
 1. {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
using this:
x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}
is_aligned x (objBitsKO ko)
x \<in> set (new_cap_addrs n ptr ko)

goal (1 subgoal):
 1. {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; is_aligned x (objBitsKO ko); x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ptr \<le> x
 2. \<lbrakk>x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; is_aligned x (objBitsKO ko); x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> x + 2 ^ objBitsKO ko - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x (objBitsKO ko); x \<in> set (new_cap_addrs n ptr ko); ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> x + 2 ^ objBitsKO ko - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x (objBitsKO ko); x \<in> set (new_cap_addrs n ptr ko); ptr \<le> x; x \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> x + (2 ^ objBitsKO ko - 1) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> ptr + (word_of_nat xa << objBitsKO ko) + (2 ^ objBitsKO ko - 1) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (ptr && ~~ mask sz) + (word_of_nat xa << objBitsKO ko) + (2 ^ objBitsKO ko - 1) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) + (2 ^ objBitsKO ko - 1) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat xa << objBitsKO ko)) + (2 ^ objBitsKO ko - 1) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat xa << objBitsKO ko) + (2 ^ objBitsKO ko - 1)) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) + (2 ^ objBitsKO ko - 1) \<le> 2 ^ sz - 1
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) + mask (objBitsKO ko) \<le> mask sz
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> sz
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> sz \<le> LENGTH(32)
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) + mask (objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 4. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> sz
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> sz \<le> LENGTH(32)
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) + mask (objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 4. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> sz \<le> LENGTH(32)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) + mask (objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) + mask (objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> mask (objBitsKO ko) < 2 ^ objBitsKO ko
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> is_aligned ((ptr && mask sz) + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko)
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> LENGTH(32)
 4. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 5. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> is_aligned ((ptr && mask sz) + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> LENGTH(32)
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 4. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO ko)
 2. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned ((ptr && mask sz) + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko)
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> LENGTH(32)
 4. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 5. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned ((ptr && mask sz) + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> LENGTH(32)
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 4. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (6 subgoals):
 1. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask sz) (?n31 xa)
 2. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)
 3. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> ?n31 xa
 4. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> LENGTH(32)
 5. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 6. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (6 subgoals):
 1. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned ptr (?n31 xa)
 2. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)
 3. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> ?n31 xa
 4. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> LENGTH(32)
 5. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 6. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)
 2. \<And>xa. \<lbrakk>ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; is_aligned (word_of_nat xa << objBitsKO ko) (objBitsKO ko)\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> objBitsKO ko
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> LENGTH(32)
 4. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 5. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask (sz - objBitsKO ko)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> sz \<le> LENGTH(32)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask sz >> objBitsKO ko
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) >> objBitsKO ko \<le> mask sz >> objBitsKO ko
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) \<le> mask sz
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) < 2 ^ sz
 3. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (word_of_nat xa << objBitsKO ko) < 2 ^ sz
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat xa << objBitsKO ko)) < unat (2 ^ sz)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat xa << objBitsKO ko) < unat (2 ^ sz)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + mask sz; xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ objBitsKO ko) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat xa << objBitsKO ko) < unat (2 ^ sz)
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> ?sz60 xa \<le> sz
 2. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> 2 ^ sz - 1 < 2 ^ ?sz60 xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned (ptr + (word_of_nat xa << objBitsKO ko)) (objBitsKO ko); ptr \<le> ptr + (word_of_nat xa << objBitsKO ko); ptr + (word_of_nat xa << objBitsKO ko) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); xa < n; x = ptr + (word_of_nat xa << objBitsKO ko); range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> 2 ^ sz - 1 < 2 ^ sz proof (prove)
goal:
No subgoals! proof (state)
this:
{x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}

goal:
No subgoals!