theory Retype_R

lemma obj_relation_retype_addrs_eq:
  assumes not_unt:"ty \<noteq> Inr (APIObjectType ArchTypes_H.Untyped)"
  assumes  amp: "m = 2^ ((obj_bits_api (APIType_map2 ty) us) - (objBitsKO ko)) * n"
  assumes  orr: "obj_relation_retype (default_object (APIType_map2 ty) dev us) ko"
  shows  "\<lbrakk> range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n \<rbrakk> \<Longrightarrow>
   (\<Union>x \<in> set (retype_addrs ptr (APIType_map2 ty) n us).
            fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x)
      = set (new_cap_addrs m ptr ko)" apply (rule set_eqI, rule iffI) apply (clarsimp simp: retype_addrs_def) apply (rename_tac p a b) apply (drule obj_relation_retype_cutsD[OF _ orr]) apply (cut_tac obj_relation_retype_default_leD[OF orr not_unt]) apply (clarsimp simp: new_cap_addrs_def image_def
                  dest!: less_two_pow_divD) apply (rule_tac x="p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y"
                 in rev_bexI) apply (simp add: amp obj_bits_api_default_object not_unt obj_bits_dev_irr) apply (rule less_le_trans[OF nat_add_left_cancel_less[THEN iffD2]]) apply (erule unat_mono) apply (subst unat_power_lower) apply (rule le_less_trans[OF diff_le_self]) apply (clarsimp simp: range_cover_def
        split: Structures_A.apiobject_type.splits) apply (simp add:field_simps,subst mult_Suc[symmetric]) apply (rule mult_le_mono1) apply simp apply (simp add: ptr_add_def shiftl_t2n field_simps
                    objBits_def[symmetric] word_unat_power[symmetric]) apply (simp add: power_add[symmetric]) apply (clarsimp simp: new_cap_addrs_def retype_addrs_def
                 dest!: less_two_pow_divD) apply (rename_tac p) apply (cut_tac obj_relation_retype_default_leD[OF orr not_unt]) apply (cut_tac obj_relation_retype_leD[OF orr]) apply (case_tac "n = 0") apply (simp add:amp) apply (case_tac "p = 0") apply simp apply (rule_tac x = 0 in rev_bexI) apply simp+ apply (rule obj_relation_cuts_trivial) apply (rule_tac x="p div (2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko))"
           in rev_bexI) apply (simp add:amp) apply (rule td_gal_lt[THEN iffD1]) apply (simp add:field_simps)+ using orr apply (clarsimp simp: obj_relation_retype_def ptr_add_def) apply (thin_tac "\<forall>x. P x" for P) apply (rule_tac x="of_nat (p mod (2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)))" in exI) apply (simp only: word_unat_power Abs_fnat_homs shiftl_t2n) apply (rule conjI) apply (rule arg_cong[where f=of_nat]) apply (subst mult_div_rearrange) apply simp apply (subst minus_mod_eq_mult_div[symmetric]) apply (simp add:diff_mult_distrib2) apply (rule of_nat_mono_maybe) apply (rule power_strict_increasing) apply (rule le_less_trans[OF diff_le_self]) apply (clarsimp simp: range_cover_def obj_bits_api_default_object obj_bits_dev_irr
                        not_unt word_bits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n \<Longrightarrow> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) = set (new_cap_addrs m ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x)\<rbrakk> \<Longrightarrow> x \<in> set (new_cap_addrs m ptr ko)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (2 subgoals):
 1. \<And>xa a b. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; xa < n; (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (xa * 2 ^ obj_bits_api (APIType_map2 ty) us))\<rbrakk> \<Longrightarrow> a \<in> set (new_cap_addrs m ptr ko)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (2 subgoals):
 1. \<And>p a b. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us))\<rbrakk> \<Longrightarrow> a \<in> set (new_cap_addrs m ptr ko)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (2 subgoals):
 1. \<And>p a b. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; \<exists>y. a = ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko \<and> y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko) \<and> b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> a \<in> set (new_cap_addrs m ptr ko)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (2 subgoals):
 1. \<And>p a b. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; \<exists>y. a = ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko \<and> y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko) \<and> b (default_object (APIType_map2 ty) dev us) ko; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us\<rbrakk> \<Longrightarrow> a \<in> set (new_cap_addrs m ptr ko)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (2 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<m}. ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat x << objBitsKO ko)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (3 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y \<in> {0..<m}
 2. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 3. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (3 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n
 2. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 3. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (4 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> unat y < ?n37 p b y
 2. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + ?n37 p b y \<le> 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n
 3. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 4. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (3 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat (2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) \<le> 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n
 2. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 3. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (4 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> obj_bits_api (APIType_map2 ty) us - objBitsKO ko < LENGTH(32)
 2. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) \<le> 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n
 3. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 4. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (4 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> obj_bits_api (APIType_map2 ty) us < LENGTH(32)
 2. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) \<le> 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n
 3. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 4. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (3 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) \<le> 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n
 2. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 3. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (3 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> Suc p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) \<le> n * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)
 2. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 3. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (3 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> Suc p \<le> n
 2. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 3. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (2 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us) + y * 2 ^ objBitsKO ko = ptr + (word_of_nat (p * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) + unat y) << objBitsKO ko)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (2 subgoals):
 1. \<And>p b y. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; y < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko); b (default_object (APIType_map2 ty) dev us) ko\<rbrakk> \<Longrightarrow> word_of_nat p * 2 ^ obj_bits_api (APIType_map2 ty) us = word_of_nat p * (2 ^ objBitsKO ko * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko))
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; xa < m\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat xa << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us)\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n = 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us))
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p = 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us))
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; 0 < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; p = 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us))
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; 0 < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; p = 0\<rbrakk> \<Longrightarrow> 0 \<in> {0..<n}
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; 0 < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; p = 0\<rbrakk> \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (0 * 2 ^ obj_bits_api (APIType_map2 ty) us))
 3. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; 0 < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; p = 0\<rbrakk> \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) ptr
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n}. ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (x * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) \<in> {0..<n}
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) < n
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> 0 < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> p < n * 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)
 3. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); n \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * 2 ^ obj_bits_api (APIType_map2 ty) us)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (2 ^ obj_bits_api (APIType_map2 ty) us * (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)))) proof (prove)
using this:
obj_relation_retype (default_object (APIType_map2 ty) dev us) ko

goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> ptr + (word_of_nat p << objBitsKO ko) \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) (ptr_add ptr (2 ^ obj_bits_api (APIType_map2 ty) us * (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)))) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p; \<forall>p. fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) p = {p + x * 2 ^ objBitsKO ko |x. x < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko)} \<and> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) p. snd x (default_object (APIType_map2 ty) dev us) ko)\<rbrakk> \<Longrightarrow> \<exists>x. word_of_nat p << objBitsKO ko = 2 ^ obj_bits_api (APIType_map2 ty) us * word_of_nat (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) + x * 2 ^ objBitsKO ko \<and> x < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> \<exists>x. word_of_nat p << objBitsKO ko = 2 ^ obj_bits_api (APIType_map2 ty) us * word_of_nat (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) + x * 2 ^ objBitsKO ko \<and> x < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> word_of_nat p << objBitsKO ko = 2 ^ obj_bits_api (APIType_map2 ty) us * word_of_nat (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) + word_of_nat (p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) * 2 ^ objBitsKO ko \<and> word_of_nat (p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ objBitsKO ko * p) = word_of_nat (2 ^ obj_bits_api (APIType_map2 ty) us * (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) + p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * 2 ^ objBitsKO ko) \<and> word_of_nat (p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) < word_of_nat (2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ objBitsKO ko * p) = word_of_nat (2 ^ obj_bits_api (APIType_map2 ty) us * (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) + p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * 2 ^ objBitsKO ko)
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> word_of_nat (p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) < word_of_nat (2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> 2 ^ objBitsKO ko * p = 2 ^ obj_bits_api (APIType_map2 ty) us * (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) + p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * 2 ^ objBitsKO ko
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> word_of_nat (p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) < word_of_nat (2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko)) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> obj_bits_api (APIType_map2 ty) us - objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> 2 ^ objBitsKO ko * p = 2 ^ (obj_bits_api (APIType_map2 ty) us - (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) * (2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko))) + p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * 2 ^ objBitsKO ko
 3. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> word_of_nat (p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) < word_of_nat (2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> 2 ^ objBitsKO ko * p = 2 ^ (obj_bits_api (APIType_map2 ty) us - (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) * (2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * (p div 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko))) + p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * 2 ^ objBitsKO ko
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> word_of_nat (p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) < word_of_nat (2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> 2 ^ objBitsKO ko * p = 2 ^ (obj_bits_api (APIType_map2 ty) us - (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) * (p - p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) + p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * 2 ^ objBitsKO ko
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> word_of_nat (p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) < word_of_nat (2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> word_of_nat (p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko)) < word_of_nat (2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko) < 2 ^ LENGTH(32)
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko < LENGTH(32)
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> obj_bits (default_object (APIType_map2 ty) dev us) < LENGTH(32)
 2. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<And>p. \<lbrakk>range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n; p < m; objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us; objBitsKO ko \<le> obj_bits (default_object (APIType_map2 ty) dev us); 0 < n; 0 < p\<rbrakk> \<Longrightarrow> p mod 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) < 2 ^ (obj_bits (default_object (APIType_map2 ty) dev us) - objBitsKO ko) proof (prove)
goal:
No subgoals!