theory Untyped_DR

lemma retype_transform_ref_subseteq_strong:
  "\<lbrakk>p \<in> set (retype_addrs ptr ty n us);range_cover ptr sz (obj_bits_api ty us) n \<rbrakk>
  \<Longrightarrow> retype_transform_obj_ref ty us p \<subseteq> {ptr..ptr + of_nat n * (2::word32) ^ obj_bits_api ty us - 1}" apply (subgoal_tac "{p .. p + 2 ^ obj_bits_api ty us - 1}
     \<subseteq> {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}") apply (erule subset_trans[rotated]) apply (clarsimp simp:retype_transform_obj_ref_def) apply (rule conjI) apply (clarsimp simp:obj_bits_api_def) apply clarsimp apply (rule is_aligned_no_overflow) apply (erule retype_addrs_aligned) apply (erule range_cover.aligned) apply (drule range_cover.sz,simp add:word_bits_def) apply (erule range_cover.sz) apply (case_tac "n = 0") apply (clarsimp simp:retype_addrs_def) apply (frule(1) retype_addrs_range_subset) apply clarsimp proof - assume cover:"range_cover ptr sz (obj_bits_api ty us) n"
      and  mem_p:"p \<in> set (retype_addrs ptr ty n us)"
      and  not_0:"0 < n" note n_less = range_cover.range_cover_n_less[OF cover] have unat_of_nat_m1: "unat (of_nat n - (1::word32)) < n" using not_0 n_less by (simp add:unat_of_nat_minus_1) have decomp:"of_nat n * 2 ^ obj_bits_api ty us = of_nat (n - 1) * 2 ^ obj_bits_api ty us
      + (2 :: word32) ^ obj_bits_api ty us" apply (simp add:distrib_right[where b = "1::'a::len word",simplified,symmetric]) using not_0 n_less apply (simp add:unat_of_nat_minus_1 obj_bits_api_def3) done show  "p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + of_nat n * 2 ^ obj_bits_api ty us - 1" apply (subst decomp) apply (simp add:add.assoc[symmetric]) apply (simp add:p_assoc_help) apply (rule order_trans[OF word_plus_mono_left word_plus_mono_right]) using mem_p not_0 apply (clarsimp simp:retype_addrs_def ptr_add_def shiftl_t2n) apply (rule word_plus_mono_right) apply (rule word_mult_le_mono1[OF word_of_nat_le]) using n_less not_0 apply (subst unat_of_nat_minus_1) apply simp apply simp apply (simp add:Set_Interval.ord_class.atLeastLessThan_def) apply (rule p2_gt_0[THEN iffD2]) using cover apply (simp add:word_bits_def range_cover_def) apply (simp only: word_bits_def[symmetric]) using not_0 n_less apply (clarsimp simp: unat_of_nat_minus_1) apply (subst unat_power_lower) using cover apply (simp add:range_cover_def) apply (rule nat_less_power_trans2[OF range_cover.range_cover_le_n_less(2),OF cover, folded word_bits_def]) apply (simp add:unat_of_nat_m1 less_imp_le) using cover apply (simp add:range_cover_def word_bits_def) apply (rule machine_word_plus_mono_right_split[where sz = sz]) using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"] apply (clarsimp simp:unat_of_nat_m1) using cover apply (simp add:range_cover_def word_bits_def) apply (rule olen_add_eqv[THEN iffD2]) apply (subst add.commute[where a = "2^(obj_bits_api ty us) - 1"]) apply (subst p_assoc_help[symmetric]) apply (rule is_aligned_no_overflow) apply (insert cover) apply (clarsimp simp:range_cover_def) apply (erule aligned_add_aligned[OF _  is_aligned_mult_triv2]) apply (simp add:range_cover_def)+ by (metis is_aligned_add is_aligned_mult_triv2 is_aligned_no_overflow_mask mask_2pm1) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us p \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us p \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}
 2. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us p \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1}
 2. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> (ty = apiobject_type.Untyped \<longrightarrow> p \<le> p + 2 ^ us - 1 \<longrightarrow> p + 2 ^ us - 1 \<le> p + 2 ^ obj_bits_api apiobject_type.Untyped us - 1) \<and> (ty \<noteq> apiobject_type.Untyped \<longrightarrow> p \<le> p + 2 ^ obj_bits_api ty us - 1)
 2. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ty = apiobject_type.Untyped \<longrightarrow> p \<le> p + 2 ^ us - 1 \<longrightarrow> p + 2 ^ us - 1 \<le> p + 2 ^ obj_bits_api apiobject_type.Untyped us - 1
 2. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> p \<le> p + 2 ^ obj_bits_api ty us - 1
 3. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> p \<le> p + 2 ^ obj_bits_api ty us - 1
 2. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> p \<le> p + 2 ^ obj_bits_api ty us - 1
 2. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> is_aligned p (obj_bits_api ty us)
 2. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> is_aligned ptr (obj_bits_api ty us)
 2. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> ?sz17 < word_bits
 3. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> ?sz17
 4. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> ?sz17 < word_bits
 2. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> ?sz17
 3. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> sz
 2. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; n = 0\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}
 2. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; n \<noteq> 0; {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; 0 < n; p \<le> p + 2 ^ obj_bits_api ty us - 1; ptr \<le> p; p + 2 ^ obj_bits_api ty us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1 proof (state)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; 0 < n; p \<le> p + 2 ^ obj_bits_api ty us - 1; ptr \<le> p; p + 2 ^ obj_bits_api ty us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1 proof (state)
this:
range_cover ptr sz (obj_bits_api ty us) n
p \<in> set (retype_addrs ptr ty n us)
0 < n

goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; 0 < n; p \<le> p + 2 ^ obj_bits_api ty us - 1; ptr \<le> p; p + 2 ^ obj_bits_api ty us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1 proof (state)
this:
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - obj_bits_api ty us)

goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; 0 < n; p \<le> p + 2 ^ obj_bits_api ty us - 1; ptr \<le> p; p + 2 ^ obj_bits_api ty us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1 proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n - 1) < n proof (prove)
using this:
0 < n
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - obj_bits_api ty us)

goal (1 subgoal):
 1. unat (word_of_nat n - 1) < n proof (state)
this:
unat (word_of_nat n - 1) < n

goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; 0 < n; p \<le> p + 2 ^ obj_bits_api ty us - 1; ptr \<le> p; p + 2 ^ obj_bits_api ty us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1 proof (prove)
goal (1 subgoal):
 1. word_of_nat n * 2 ^ obj_bits_api ty us = word_of_nat (n - 1) * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us proof (prove)
goal (1 subgoal):
 1. word_of_nat n * 2 ^ obj_bits_api ty us = (word_of_nat (n - Suc 0) + 1) * 2 ^ obj_bits_api ty us proof (prove)
using this:
0 < n
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - obj_bits_api ty us)

goal (1 subgoal):
 1. word_of_nat n * 2 ^ obj_bits_api ty us = (word_of_nat (n - Suc 0) + 1) * 2 ^ obj_bits_api ty us proof (prove)
goal:
No subgoals! proof (state)
this:
word_of_nat n * 2 ^ obj_bits_api ty us = word_of_nat (n - 1) * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us

goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; 0 < n; p \<le> p + 2 ^ obj_bits_api ty us - 1; ptr \<le> p; p + 2 ^ obj_bits_api ty us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1 proof (prove)
goal (1 subgoal):
 1. p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1 proof (prove)
goal (1 subgoal):
 1. p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + (word_of_nat (n - 1) * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us) - 1 proof (prove)
goal (1 subgoal):
 1. p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1 proof (prove)
goal (1 subgoal):
 1. p + (2 ^ obj_bits_api ty us - 1) \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (4 subgoals):
 1. p \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 4. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
using this:
p \<in> set (retype_addrs ptr ty n us)
0 < n

goal (4 subgoals):
 1. p \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 4. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 4. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> word_of_nat x * 2 ^ obj_bits_api ty us \<le> (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> x \<le> unat (word_of_nat n - 1)
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> 0 < 2 ^ obj_bits_api ty us
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ LENGTH(32)
 4. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 5. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 6. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 7. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
using this:
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - obj_bits_api ty us)
0 < n

goal (7 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> x \<le> unat (word_of_nat n - 1)
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> 0 < 2 ^ obj_bits_api ty us
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ LENGTH(32)
 4. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 5. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 6. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 7. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (9 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 2 ^ LENGTH(32); n < 2 ^ (LENGTH(32) - obj_bits_api ty us); 0 < n\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH(32)
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 2 ^ LENGTH(32); n < 2 ^ (LENGTH(32) - obj_bits_api ty us); 0 < n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 2 ^ LENGTH(32); n < 2 ^ (LENGTH(32) - obj_bits_api ty us); 0 < n\<rbrakk> \<Longrightarrow> x \<le> n - 1
 4. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> 0 < 2 ^ obj_bits_api ty us
 5. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ LENGTH(32)
 6. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 7. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 8. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 9. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (8 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 2 ^ LENGTH(32); n < 2 ^ (LENGTH(32) - obj_bits_api ty us); 0 < n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 2 ^ LENGTH(32); n < 2 ^ (LENGTH(32) - obj_bits_api ty us); 0 < n\<rbrakk> \<Longrightarrow> x \<le> n - 1
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> 0 < 2 ^ obj_bits_api ty us
 4. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ LENGTH(32)
 5. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 6. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 7. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 8. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 2 ^ LENGTH(32); n < 2 ^ (LENGTH(32) - obj_bits_api ty us); 0 < n\<rbrakk> \<Longrightarrow> x \<le> n - 1
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> 0 < 2 ^ obj_bits_api ty us
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ LENGTH(32)
 4. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 5. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 6. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 7. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> 0 < 2 ^ obj_bits_api ty us
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ LENGTH(32)
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 5. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 6. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> obj_bits_api ty us < LENGTH(32)
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ LENGTH(32)
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 5. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 6. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n

goal (6 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> obj_bits_api ty us < LENGTH(32)
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ LENGTH(32)
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 5. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 6. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ LENGTH(32)
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ word_bits
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
using this:
0 < n
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - obj_bits_api ty us)

goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ obj_bits_api ty us) < 2 ^ word_bits
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> (n - Suc 0) * unat (2 ^ obj_bits_api ty us) < 2 ^ word_bits
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> obj_bits_api ty us < LENGTH(32)
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> (n - Suc 0) * 2 ^ obj_bits_api ty us < 2 ^ word_bits
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 5. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 6. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n

goal (6 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> obj_bits_api ty us < LENGTH(32)
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> (n - Suc 0) * 2 ^ obj_bits_api ty us < 2 ^ word_bits
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 5. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 6. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> (n - Suc 0) * 2 ^ obj_bits_api ty us < 2 ^ word_bits
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> n - Suc 0 \<le> n
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> word_bits
 3. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 5. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 6. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> word_bits
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n

goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; n < 4294967296; n < 2 ^ (32 - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> word_bits
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ obj_bits_api ty us
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 4. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat ((word_of_nat n - 1) * 2 ^ obj_bits_api ty us) < 2 ^ sz
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> sz < word_bits
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
using this:
unat (word_of_nat n - 1) < n \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat (unat (word_of_nat n - 1)) * 2 ^ obj_bits_api ty us) < 2 ^ sz

goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat ((word_of_nat n - 1) * 2 ^ obj_bits_api ty us) < 2 ^ sz
 2. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> sz < word_bits
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 4. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 5. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> sz < word_bits
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 4. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n

goal (4 subgoals):
 1. \<And>x. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> sz < word_bits
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 3. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 4. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (3 subgoals):
 1. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 3. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (3 subgoals):
 1. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> 2 ^ obj_bits_api ty us - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us)
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 3. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (3 subgoals):
 1. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1)
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 3. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (3 subgoals):
 1. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 3. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (3 subgoals):
 1. is_aligned (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us) (obj_bits_api ty us)
 2. 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 3. ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> is_aligned (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us) (obj_bits_api ty us)
 2. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 3. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr (obj_bits_api ty us); sz < 32; obj_bits_api ty us \<le> sz; n + unat (ptr && mask sz >> obj_bits_api ty us) \<le> 2 ^ (sz - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us) (obj_bits_api ty us)
 2. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 3. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>sz < 32; obj_bits_api ty us \<le> sz; n + unat (ptr && mask sz >> obj_bits_api ty us) \<le> 2 ^ (sz - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> obj_bits_api ty us
 2. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> 2 ^ obj_bits_api ty us - 1 \<le> 2 ^ obj_bits_api ty us - 1
 3. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr (obj_bits_api ty us) \<and> sz < 32 \<and> obj_bits_api ty us \<le> sz \<and> n + unat (ptr && mask sz >> obj_bits_api ty us) \<le> 2 ^ (sz - obj_bits_api ty us) \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ obj_bits_api ty us + (2 ^ obj_bits_api ty us - 1) proof (state)
this:
p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1

goal:
No subgoals!