theory Detype_R

lemma new_caps_addrs_append:
  "\<lbrakk>range_cover ptr sz (objBitsKO va + us) (Suc n)\<rbrakk> \<Longrightarrow>
   new_cap_addrs (unat (of_nat n + (1::word32) << us)) ptr val =
   new_cap_addrs (unat (((of_nat n)::word32) << us)) ptr val @
   new_cap_addrs (unat ((2::word32) ^ us))
                 ((((of_nat n)::word32) << objBitsKO val + us) + ptr) val" apply (subst add.commute) apply (clarsimp simp:new_cap_addrs_def) apply (subst upt_add_eq_append'[where j="unat (((of_nat n)::word32) << us)"]) prefer 3 apply simp apply (subst upt_lhs_sub_map) apply (simp add:Fun.comp_def field_simps) apply (subst unat_sub[symmetric]) apply (simp add:shiftl_t2n) apply (subst mult.commute) apply (subst mult.commute[where a = "2 ^ us"])+ apply (rule word_mult_le_mono1) apply (simp add:word_le_nat_alt) apply (subst of_nat_Suc[symmetric]) apply (frule range_cover.unat_of_nat_n) apply (drule range_cover.unat_of_nat_n[OF range_cover_le[where n = n]]) apply simp apply simp apply (simp add: p2_gt_0) apply (simp add:range_cover_def word_bits_def) apply (subst word_bits_def[symmetric]) apply (subst of_nat_Suc[symmetric]) apply (subst range_cover.unat_of_nat_n) apply simp apply (subst unat_power_lower) apply (simp add:range_cover_def) apply (frule range_cover.range_cover_n_le(2)) apply (subst mult.commute) apply (rule le_less_trans[OF nat_le_power_trans[where m = sz]]) apply (erule le_trans) apply simp apply (simp add:range_cover_def) apply (simp add:range_cover_def[where 'a=32, folded word_bits_def]) apply (clarsimp simp: power_add [symmetric] shiftl_t2n field_simps) apply simp apply (frule range_cover_le[where n = n]) apply simp apply (drule range_cover_rel[where sbit'= "objBitsKO va"]) apply simp+ apply (drule range_cover_rel[where sbit'= "objBitsKO va"]) apply simp+ apply (drule range_cover.unat_of_nat_n)+ apply (simp add:shiftl_t2n) apply (clarsimp simp: power_add[symmetric] shiftl_t2n field_simps ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> new_cap_addrs (unat (word_of_nat n + 1 << us)) ptr val = new_cap_addrs (unat (word_of_nat n << us)) ptr val @ new_cap_addrs (unat (2 ^ us)) ((word_of_nat n << objBitsKO val + us) + ptr) val proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val = new_cap_addrs (unat (word_of_nat n << us)) ptr val @ new_cap_addrs (unat (2 ^ us)) ((word_of_nat n << objBitsKO val + us) + ptr) val proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> map (\<lambda>p. ptr + (word_of_nat p << objBitsKO val)) [0..<unat (1 + word_of_nat n << us)] = map (\<lambda>p. ptr + (word_of_nat p << objBitsKO val)) [0..<unat (word_of_nat n << us)] @ map (\<lambda>p. (word_of_nat n << objBitsKO val + us) + ptr + (word_of_nat p << objBitsKO val)) [0..<unat (2 ^ us)] proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 2. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us)
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> map (\<lambda>p. ptr + (word_of_nat p << objBitsKO val)) ([0..<unat (word_of_nat n << us)] @ [unat (word_of_nat n << us)..<unat (1 + word_of_nat n << us)]) = map (\<lambda>p. ptr + (word_of_nat p << objBitsKO val)) [0..<unat (word_of_nat n << us)] @ map (\<lambda>p. (word_of_nat n << objBitsKO val + us) + ptr + (word_of_nat p << objBitsKO val)) [0..<unat (2 ^ us)] proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> map (\<lambda>p. ptr + (word_of_nat p << objBitsKO val)) ([0..<unat (word_of_nat n << us)] @ [unat (word_of_nat n << us)..<unat (1 + word_of_nat n << us)]) = map (\<lambda>p. ptr + (word_of_nat p << objBitsKO val)) [0..<unat (word_of_nat n << us)] @ map (\<lambda>p. (word_of_nat n << objBitsKO val + us) + ptr + (word_of_nat p << objBitsKO val)) [0..<unat (2 ^ us)]
 2. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> map (\<lambda>p. ptr + (word_of_nat p << objBitsKO val)) [unat (word_of_nat n << us)..<unat (1 + word_of_nat n << us)] = map (\<lambda>p. (word_of_nat n << objBitsKO val + us) + ptr + (word_of_nat p << objBitsKO val)) [0..<unat (2 ^ us)]
 2. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> map (\<lambda>p. ptr + (word_of_nat p << objBitsKO val)) (map ((+) (unat (word_of_nat n << us))) [0..<unat (1 + word_of_nat n << us) - unat (word_of_nat n << us)]) = map (\<lambda>p. (word_of_nat n << objBitsKO val + us) + ptr + (word_of_nat p << objBitsKO val)) [0..<unat (2 ^ us)]
 2. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat (1 + word_of_nat n << us) - unat (word_of_nat n << us)] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 2. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> word_of_nat n << us \<le> 1 + word_of_nat n << us
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> 2 ^ us * word_of_nat n \<le> 2 ^ us * (1 + word_of_nat n)
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> word_of_nat n * 2 ^ us \<le> 2 ^ us * (1 + word_of_nat n)
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> word_of_nat n * 2 ^ us \<le> (1 + word_of_nat n) * 2 ^ us
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (6 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> word_of_nat n \<le> 1 + word_of_nat n
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> 0 < 2 ^ us
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ LENGTH(32)
 4. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 6. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (6 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (word_of_nat n) \<le> unat (1 + word_of_nat n)
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> 0 < 2 ^ us
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ LENGTH(32)
 4. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 6. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (6 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (word_of_nat n) \<le> unat (word_of_nat (Suc n))
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> 0 < 2 ^ us
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ LENGTH(32)
 4. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 6. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); unat (word_of_nat (Suc n)) = Suc n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> unat (word_of_nat (Suc n))
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> 0 < 2 ^ us
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ LENGTH(32)
 4. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 6. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (7 subgoals):
 1. unat (word_of_nat (Suc n)) = Suc n \<Longrightarrow> n \<le> Suc n
 2. \<lbrakk>unat (word_of_nat (Suc n)) = Suc n; unat (word_of_nat n) = n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> unat (word_of_nat (Suc n))
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> 0 < 2 ^ us
 4. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ LENGTH(32)
 5. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 6. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 7. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>unat (word_of_nat (Suc n)) = Suc n; unat (word_of_nat n) = n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> unat (word_of_nat (Suc n))
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> 0 < 2 ^ us
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ LENGTH(32)
 4. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 6. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (5 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> 0 < 2 ^ us
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ LENGTH(32)
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (5 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> us < 32
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ LENGTH(32)
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ LENGTH(32)
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (1 + word_of_nat n) * unat (2 ^ us) < 2 ^ word_bits
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> unat (word_of_nat (Suc n)) * unat (2 ^ us) < 2 ^ word_bits
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (5 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> range_cover ?ptr24 ?sz24 ?sbit24 (Suc n)
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> Suc n * unat (2 ^ us) < 2 ^ word_bits
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> Suc n * unat (2 ^ us) < 2 ^ word_bits
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (5 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> us < LENGTH(32)
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> Suc n * 2 ^ us < 2 ^ word_bits
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> Suc n * 2 ^ us < 2 ^ word_bits
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> Suc n * 2 ^ us < 2 ^ word_bits
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> 2 ^ us * Suc n < 2 ^ word_bits
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> Suc n \<le> 2 ^ (sz - us)
 2. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> us \<le> sz
 3. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ word_bits
 4. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 6. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (6 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> 2 ^ (sz - (us + objBitsKO va)) \<le> 2 ^ (sz - us)
 2. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> us \<le> sz
 3. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ word_bits
 4. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 6. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> us \<le> sz
 2. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ word_bits
 3. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 5. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO va) (Suc n); Suc n \<le> 2 ^ (sz - (us + objBitsKO va))\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ word_bits
 2. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 4. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (us + objBitsKO va) (Suc n) \<Longrightarrow> map (\<lambda>x. ptr + (word_of_nat x + (word_of_nat n << us) << objBitsKO val)) [0..<unat ((1 + word_of_nat n << us) - (word_of_nat n << us))] = map (\<lambda>p. ptr + ((word_of_nat p << objBitsKO val) + (word_of_nat n << us + objBitsKO val))) [0..<unat (2 ^ us)]
 2. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 3. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> 0 \<le> unat (word_of_nat n << us)
 2. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (objBitsKO va + us) (Suc n) \<Longrightarrow> n \<le> Suc n
 2. \<lbrakk>range_cover ptr sz (objBitsKO va + us) (Suc n); range_cover ptr sz (objBitsKO va + us) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO va + us) (Suc n); range_cover ptr sz (objBitsKO va + us) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO va + us) n \<Longrightarrow> objBitsKO va \<le> objBitsKO va + us
 2. range_cover ptr sz (objBitsKO va + us) n \<Longrightarrow> ?m93 = 2 ^ (objBitsKO va + us - objBitsKO va) * Suc n
 3. \<lbrakk>range_cover ptr sz (objBitsKO va + us) n; range_cover ptr sz (objBitsKO va) ?m93\<rbrakk> \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO va + us) n; range_cover ptr sz (objBitsKO va) (2 ^ us + 2 ^ us * n)\<rbrakk> \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO va) (2 ^ us + 2 ^ us * n) \<Longrightarrow> objBitsKO va \<le> objBitsKO va + us
 2. range_cover ptr sz (objBitsKO va) (2 ^ us + 2 ^ us * n) \<Longrightarrow> ?m98 = 2 ^ (objBitsKO va + us - objBitsKO va) * n
 3. \<lbrakk>range_cover ptr sz (objBitsKO va) (2 ^ us + 2 ^ us * n); range_cover ptr sz (objBitsKO va) ?m98\<rbrakk> \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO va) (2 ^ us + 2 ^ us * n); range_cover ptr sz (objBitsKO va) (2 ^ us * n)\<rbrakk> \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (word_of_nat (2 ^ us + 2 ^ us * n)) = 2 ^ us + 2 ^ us * n; unat (word_of_nat (2 ^ us * n)) = 2 ^ us * n\<rbrakk> \<Longrightarrow> unat (word_of_nat n << us) \<le> unat (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (2 ^ us + 2 ^ us * word_of_nat n) = 2 ^ us + 2 ^ us * n; unat (2 ^ us * word_of_nat n) = 2 ^ us * n\<rbrakk> \<Longrightarrow> 2 ^ us * n \<le> unat (2 ^ us * (1 + word_of_nat n)) proof (prove)
goal:
No subgoals!