theory Retype_R

lemma range_cover_new_cap_addrs_compare:
  assumes not_0: "n \<noteq> 0"
  and     cover: "range_cover ptr sz (objBitsKO val + gbits) n"
  and    ptr_in: "p \<in> set (new_cap_addrs (unat (((of_nat n)::word32) << gbits)) ptr val)"
  shows  "p \<le> ptr + of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)" proof - note unat_of_nat_shift = range_cover.unat_of_nat_n_shift[OF cover,where gbits=gbits,simplified] have cover' :"range_cover ptr sz (objBitsKO val) (n*2^gbits)" by (rule range_cover_rel[OF cover],simp+) have upbound:" unat ((((of_nat n)::word32) * 2 ^ gbits)) * unat ((2::word32) ^ objBitsKO val) < 2 ^ word_bits" using range_cover.range_cover_le_n_less[OF cover' le_refl] cover' apply - apply (drule nat_less_power_trans) apply (simp add:range_cover_def) apply (fold word_bits_def) using unat_of_nat_shift not_0 apply (simp add:field_simps shiftl_t2n) done have not_0': "(2::word32) ^ (objBitsKO val + gbits) * of_nat n \<noteq> 0" apply (rule range_cover_not_zero_shift[OF not_0,unfolded shiftl_t2n,OF _ le_refl]) apply (rule range_cover_rel[OF cover]; simp) done have "gbits < word_bits" using cover by (simp add:range_cover_def word_bits_def) thus ?thesis apply - apply (insert not_0 cover ptr_in) apply (frule range_cover.range_cover_le_n_less[OF _ le_refl]) apply (fold word_bits_def) apply (simp add:shiftL_nat ) apply (simp add:range_cover.unat_of_nat_n_shift) apply (clarsimp simp:new_cap_addrs_def shiftl_t2n) apply (rename_tac pa) apply (rule word_plus_mono_right) apply (rule order_trans) apply (subst mult.commute) apply (rule word_mult_le_iff[THEN iffD2]) apply (clarsimp simp:p2_gt_0 range_cover_def word_bits_def) apply (drule range_cover_rel[where sbit' = "0"]) apply (simp+)[2] apply (erule less_le_trans[OF range_cover.range_cover_le_n_less(2)]) apply (clarsimp simp:field_simps power_add) apply (rule unat_le_helper) apply (rule of_nat_mono_maybe_le[THEN iffD1]) using range_cover.range_cover_le_n_less[OF cover' le_refl] apply (simp_all only:word_bits_def[symmetric]) apply simp apply (drule nat_less_power_trans) apply (simp add:range_cover_def word_bits_def) apply (rule less_le_trans[OF mult_less_mono1]) apply (rule unat_mono) apply (rule_tac y1= "pa" in  of_nat_mono_maybe'[THEN iffD1,rotated -1]) apply (assumption) apply (simp add:word_bits_def) apply (simp add:word_bits_def) apply simp using unat_of_nat_shift apply (simp add:field_simps shiftl_t2n) apply simp apply (rule word_less_sub_1) apply (simp add:power_add field_simps) apply (subst mult.assoc[symmetric]) apply (rule word_mult_less_mono1) apply (rule word_of_nat_less) using unat_of_nat_shift apply (simp add:shiftl_t2n field_simps) apply (meson less_exp objBitsKO_bounded2 of_nat_less_pow_32 word_gt_a_gt_0) using upbound apply (simp add:word_bits_def) apply (rule machine_word_plus_mono_right_split[where sz = sz]) apply (rule less_le_trans[rotated -1]) apply (rule range_cover.range_cover_compare_bound[OF cover']) apply (simp add: unat_minus_one[OF not_0']) using range_cover.unat_of_nat_n_shift[OF cover le_refl] apply (simp add:shiftl_t2n power_add field_simps) apply (simp add:range_cover_def word_bits_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (state)
goal (1 subgoal):
 1. p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (state)
this:
unat (word_of_nat n << gbits) = n * 2 ^ gbits

goal (1 subgoal):
 1. p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits) proof (state)
this:
range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits)

goal (1 subgoal):
 1. p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ word_bits proof (prove)
using this:
n * 2 ^ gbits < 2 ^ LENGTH(32)
n * 2 ^ gbits < 2 ^ (LENGTH(32) - objBitsKO val)
range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits)

goal (1 subgoal):
 1. unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n * 2 ^ gbits < 2 ^ LENGTH(32); n * 2 ^ gbits < 2 ^ (LENGTH(32) - objBitsKO val); range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits)\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ word_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n * 2 ^ gbits < 2 ^ LENGTH(32); range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits)\<rbrakk> \<Longrightarrow> objBitsKO val \<le> LENGTH(32)
 2. \<lbrakk>n * 2 ^ gbits < 2 ^ LENGTH(32); range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits); 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n * 2 ^ gbits < 2 ^ LENGTH(32); range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits); 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n * 2 ^ gbits < 2 ^ word_bits; range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits); 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ word_bits proof (prove)
using this:
unat (word_of_nat n << gbits) = n * 2 ^ gbits
n \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>n * 2 ^ gbits < 2 ^ word_bits; range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits); 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ word_bits proof (prove)
goal:
No subgoals! proof (state)
this:
unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ word_bits

goal (1 subgoal):
 1. p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
goal (1 subgoal):
 1. 2 ^ (objBitsKO val + gbits) * word_of_nat n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. range_cover ?ptr ?sz (objBitsKO val + gbits) n proof (prove)
goal:
No subgoals! proof (state)
this:
2 ^ (objBitsKO val + gbits) * word_of_nat n \<noteq> 0

goal (1 subgoal):
 1. p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
goal (1 subgoal):
 1. gbits < word_bits proof (prove)
using this:
range_cover ptr sz (objBitsKO val + gbits) n

goal (1 subgoal):
 1. gbits < word_bits proof (state)
this:
gbits < word_bits

goal (1 subgoal):
 1. p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
using this:
gbits < word_bits

goal (1 subgoal):
 1. p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
goal (1 subgoal):
 1. gbits < word_bits \<Longrightarrow> p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gbits < word_bits; n \<noteq> 0; range_cover ptr sz (objBitsKO val + gbits) n; p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val)\<rbrakk> \<Longrightarrow> p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gbits < word_bits; n \<noteq> 0; range_cover ptr sz (objBitsKO val + gbits) n; p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); n < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gbits < word_bits; n \<noteq> 0; range_cover ptr sz (objBitsKO val + gbits) n; p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> p \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; p \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> p \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; x < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr + 2 ^ objBitsKO val * word_of_nat x \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr + 2 ^ objBitsKO val * word_of_nat pa \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> 2 ^ objBitsKO val * word_of_nat pa \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> 2 ^ objBitsKO val * word_of_nat pa \<le> ?y13 pa
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?y13 pa \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val \<le> ?y17 pa pa
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?y17 pa pa \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (6 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> 0 < 2 ^ objBitsKO val
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (word_of_nat pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (5 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (word_of_nat pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (7 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> 0 \<le> objBitsKO val + gbits
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?m26 pa = 2 ^ (objBitsKO val + gbits - 0) * n
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; range_cover ptr sz 0 (?m26 pa)\<rbrakk> \<Longrightarrow> unat (word_of_nat pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 7. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (5 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; range_cover ptr sz 0 (2 ^ (objBitsKO val + gbits) * n)\<rbrakk> \<Longrightarrow> unat (word_of_nat pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (6 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (word_of_nat pa) * unat (2 ^ objBitsKO val) \<le> 2 ^ (objBitsKO val + gbits) * n
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - 0) \<le> 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (6 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val\<rbrakk> \<Longrightarrow> unat (word_of_nat pa) \<le> n * 2 ^ gbits
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - 0) \<le> 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (6 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> word_of_nat (n * 2 ^ gbits)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - 0) \<le> 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (8 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val\<rbrakk> \<Longrightarrow> n * 2 ^ gbits < 2 ^ LENGTH(32)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val\<rbrakk> \<Longrightarrow> pa < 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val\<rbrakk> \<Longrightarrow> pa \<le> n * 2 ^ gbits
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - 0) \<le> 2 ^ LENGTH(32)
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 7. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 8. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
using this:
n * 2 ^ gbits < 2 ^ LENGTH(32)
n * 2 ^ gbits < 2 ^ (LENGTH(32) - objBitsKO val)

goal (8 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val\<rbrakk> \<Longrightarrow> n * 2 ^ gbits < 2 ^ LENGTH(32)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val\<rbrakk> \<Longrightarrow> pa < 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val\<rbrakk> \<Longrightarrow> pa \<le> n * 2 ^ gbits
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - 0) \<le> 2 ^ LENGTH(32)
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 7. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 8. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (5 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> 2 ^ (word_bits - 0) \<le> 2 ^ word_bits
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ word_bits
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (4 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ word_bits
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (5 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits\<rbrakk> \<Longrightarrow> objBitsKO val \<le> word_bits
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ word_bits
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (4 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) * unat (2 ^ objBitsKO val) < 2 ^ word_bits
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (6 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (?j21 pa pa) < ?j162 pa
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ objBitsKO val)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> ?j162 pa * unat (2 ^ objBitsKO val) \<le> 2 ^ word_bits
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (6 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> ?j21 pa pa < ?b166 pa
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ objBitsKO val)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (?b166 pa) * unat (2 ^ objBitsKO val) \<le> 2 ^ word_bits
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> ?j21 pa pa
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ?j21 pa pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (8 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> pa < ?x169 pa
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> ?x169 pa < 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> pa < 2 ^ LENGTH(32)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ objBitsKO val)
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat (?x169 pa)) * unat (2 ^ objBitsKO val) \<le> 2 ^ word_bits
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> word_of_nat pa
 7. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 8. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (7 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n * 2 ^ gbits < 2 ^ LENGTH(32)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> pa < 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ objBitsKO val)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat (n * 2 ^ gbits)) * unat (2 ^ objBitsKO val) \<le> 2 ^ word_bits
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> word_of_nat pa
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 7. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (6 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> pa < 2 ^ LENGTH(32)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ objBitsKO val)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat (n * 2 ^ gbits)) * unat (2 ^ objBitsKO val) \<le> 2 ^ word_bits
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> word_of_nat pa
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 6. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (5 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ objBitsKO val)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat (n * 2 ^ gbits)) * unat (2 ^ objBitsKO val) \<le> 2 ^ word_bits
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> word_of_nat pa
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 5. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (4 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat (n * 2 ^ gbits)) * unat (2 ^ objBitsKO val) \<le> 2 ^ word_bits
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> word_of_nat pa
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
using this:
unat (word_of_nat n << gbits) = n * 2 ^ gbits

goal (4 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; 2 ^ objBitsKO val * (n * 2 ^ gbits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat (n * 2 ^ gbits)) * unat (2 ^ objBitsKO val) \<le> 2 ^ word_bits
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> word_of_nat pa
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa \<le> word_of_nat pa
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val \<le> 2 ^ (objBitsKO val + gbits) * word_of_nat n - 1
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val < 2 ^ (objBitsKO val + gbits) * word_of_nat n
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val < word_of_nat n * (2 ^ gbits * 2 ^ objBitsKO val)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa * 2 ^ objBitsKO val < word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (4 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> word_of_nat pa < word_of_nat n * 2 ^ gbits
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> 0 < 2 ^ objBitsKO val
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (4 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> pa < unat (word_of_nat n * 2 ^ gbits)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> 0 < 2 ^ objBitsKO val
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
using this:
unat (word_of_nat n << gbits) = n * 2 ^ gbits

goal (4 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> pa < unat (word_of_nat n * 2 ^ gbits)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> 0 < 2 ^ objBitsKO val
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> 0 < 2 ^ objBitsKO val
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
using this:
unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ word_bits

goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (gbits + objBitsKO val) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + word_of_nat pa * 2 ^ objBitsKO val; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) < 2 ^ sz
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> sz < word_bits proof (prove)
goal (3 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> ?y190 pa \<le> 2 ^ sz
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) < ?y190 pa
 3. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> sz < word_bits proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (2 ^ (objBitsKO val + gbits) * word_of_nat n - 1) < n * 2 ^ gbits * 2 ^ objBitsKO val + unat (ptr && mask sz)
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> sz < word_bits proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (2 ^ (objBitsKO val + gbits) * word_of_nat n) - Suc 0 < n * 2 ^ gbits * 2 ^ objBitsKO val
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> sz < word_bits proof (prove)
using this:
unat (word_of_nat n << objBitsKO val + gbits) = n * 2 ^ (objBitsKO val + gbits)

goal (2 subgoals):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> unat (2 ^ (objBitsKO val + gbits) * word_of_nat n) - Suc 0 < n * 2 ^ gbits * 2 ^ objBitsKO val
 2. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> sz < word_bits proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>gbits < word_bits; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; n < 2 ^ word_bits; pa < n * 2 ^ gbits; p = ptr + 2 ^ objBitsKO val * word_of_nat pa; n * 2 ^ gbits < 2 ^ word_bits; n * 2 ^ gbits < 2 ^ (word_bits - objBitsKO val)\<rbrakk> \<Longrightarrow> sz < word_bits proof (prove)
goal:
No subgoals! proof (state)
this:
p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)

goal:
No subgoals!