theory Untyped_DR

lemma free_range_of_untyped_pick_retype_addrs:
  notes [simp del] = atLeastAtMost_iff
  shows "\<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots) ; slots \<noteq> []\<rbrakk> \<Longrightarrow>
  free_range_of_untyped (unat ((ptr && mask sz) + (of_nat (length slots) << obj_bits_api tp us))) sz (ptr && ~~ mask sz) \<inter>
  (\<lambda>a. pick (retype_transform_obj_ref tp us a)) ` set (retype_addrs ptr tp (length slots) us) =
  {}" apply (clarsimp simp:image_def free_range_of_untyped_def) apply (rule disjointI) apply (drule CollectD) apply clarsimp apply (frule retype_transform_obj_ref_not_empty) apply (erule range_cover.aligned) apply simp apply (drule(1) retype_transform_ref_subseteq_strong) apply (drule nonempty_pick_in) apply (drule(1) set_mp[rotated]) apply (clarsimp simp:shiftl_t2n field_simps) apply (erule(1) in_empty_setE) apply clarsimp apply (drule leD[where y = "(ptr && mask sz) + ((ptr && ~~ mask sz)
    + of_nat (length slots) * 2 ^ obj_bits_api tp us)"]) apply (subgoal_tac " ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 <
    (ptr && mask sz) + ((ptr && ~~ mask sz) + of_nat (length slots) * 2 ^ obj_bits_api tp us)") apply simp apply (subst group_add_class.add_diff_eq[symmetric]) apply (frule range_cover_not_zero_shift[rotated,OF _ le_refl]) apply simp apply (thin_tac "\<not>P" for P) apply (subst add.assoc[symmetric]) apply (subst AND_NOT_mask_plus_AND_mask_eq[symmetric,where n = sz]) apply (subst add.commute[where a = "(ptr && mask sz)"]) apply (rule word_plus_strict_mono_right) apply (rule word_leq_le_minus_one) apply simp apply (simp add:shiftl_t2n field_simps) apply (subst add.assoc) apply (rule word_plus_mono_right) apply (simp add:word_le_nat_alt) apply (simp add: range_cover_unat) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask]) apply (rule le_refl) apply (drule le_p2_minus_1) apply (simp add:word_less_nat_alt) apply (subst unat_power_lower32[unfolded word_bits_def]) apply (erule range_cover.sz) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []\<rbrakk> \<Longrightarrow> free_range_of_untyped (unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))) sz (ptr && ~~ mask sz) \<inter> (\<lambda>a. pick (retype_transform_obj_ref tp us a)) ` set (retype_addrs ptr tp (length slots) us) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0\<rbrakk> \<Longrightarrow> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> {y. \<exists>x\<in>set (retype_addrs ptr tp (length slots) us). y = pick (retype_transform_obj_ref tp us x)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; x \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; y \<in> {y. \<exists>x\<in>set (retype_addrs ptr tp (length slots) us). y = pick (retype_transform_obj_ref tp us x)}\<rbrakk> \<Longrightarrow> x \<noteq> y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; x \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>x\<in>set (retype_addrs ptr tp (length slots) us). y = pick (retype_transform_obj_ref tp us x)\<rbrakk> \<Longrightarrow> x \<noteq> y proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> is_aligned ptr (obj_bits_api tp us)
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> ?y17 xa \<in> set (retype_addrs ptr tp (length slots) us)
 3. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<in> set (retype_addrs ptr tp (length slots) us); retype_transform_obj_ref tp us (?y17 xa) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> ?y17 xa \<in> set (retype_addrs ptr tp (length slots) us)
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<in> set (retype_addrs ptr tp (length slots) us); retype_transform_obj_ref tp us (?y17 xa) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<in> set (retype_addrs ptr tp (length slots) us); retype_transform_obj_ref tp us xa \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; retype_transform_obj_ref tp us xa \<noteq> {}; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> retype_transform_obj_ref tp us xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us))..(ptr && ~~ mask sz) + 2 ^ sz - 1}; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; pick (retype_transform_obj_ref tp us xa) \<in> {(ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)..(ptr && ~~ mask sz) + 2 ^ sz - 1}; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}\<rbrakk> \<Longrightarrow> {(ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)\<rbrakk> \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)\<rbrakk> \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)\<rbrakk> \<Longrightarrow> ptr + (word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)\<rbrakk> \<Longrightarrow> length slots \<noteq> 0
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); slots \<noteq> []; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < (ptr && mask sz) + (ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) + (word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < (ptr && mask sz) + (ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) + (word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < (ptr && ~~ mask sz) + (ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < word_of_nat (length slots) * 2 ^ obj_bits_api tp us
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) \<le> (ptr && ~~ mask sz) + (ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat (length slots) * 2 ^ obj_bits_api tp us \<le> word_of_nat (length slots) * 2 ^ obj_bits_api tp us
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat (length slots) * 2 ^ obj_bits_api tp us \<noteq> 0
 3. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) \<le> (ptr && ~~ mask sz) + (ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat (length slots) * 2 ^ obj_bits_api tp us \<noteq> 0
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) \<le> (ptr && ~~ mask sz) + (ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) \<le> (ptr && ~~ mask sz) + (ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && mask sz \<le> (ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; unat ptr \<le> unat ((ptr && ~~ mask sz) + 2 ^ sz - 1); unat ((ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)) \<le> unat ((ptr && ~~ mask sz) + 2 ^ sz - 1); unat ptr \<le> unat (ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1); \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) \<le> unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> ?sz61 xa \<le> sz
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us < 2 ^ ?sz61 xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> 2 ^ sz - Suc 0; retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> unat (ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < unat ((ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < unat (2 ^ sz) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> unat (ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < unat ((ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> unat (ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < unat ((ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots); retype_transform_obj_ref tp us xa \<subseteq> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; pick (retype_transform_obj_ref tp us xa) \<in> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; \<not> unat (ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1) < unat ((ptr && mask sz) + ((ptr && ~~ mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us)); word_of_nat (length slots) << obj_bits_api tp us \<noteq> 0; unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz proof (prove)
goal:
No subgoals!