theory Retype_R

lemma new_cap_addrs_distinct:
  assumes cover: "range_cover ptr sz (objBitsKO ko) n"
  shows "distinct (new_cap_addrs n ptr ko)" unfolding new_cap_addrs_def apply (simp add: distinct_map) apply (rule comp_inj_on[where f=of_nat, unfolded o_def]) apply (rule subset_inj_on) apply (rule word_unat.Abs_inj_on) apply (clarsimp simp only: unats_def atLeastLessThan_iff
                  dest!: less_two_pow_divD) apply (insert cover) apply (erule less_le_trans) apply (insert range_cover.range_cover_n_le[OF cover]) apply (erule le_trans) apply (cases "objBitsKO ko = 0") apply (simp add:word_bits_def) apply (rule less_imp_le) apply (rule power_strict_increasing) apply (simp add:word_bits_def) apply simp apply (rule inj_onI) apply clarsimp apply (drule arg_cong[where f="\<lambda>x. x >> objBitsKO ko"]) apply (cases "objBitsKO ko = 0") apply simp apply (subst(asm) shiftl_shiftr_id, simp add: range_cover_def) apply (subst word_unat_power, rule of_nat_mono_maybe) apply (rule power_strict_increasing) apply (simp add: word_bits_def) apply simp apply (erule order_less_le_trans) apply simp apply (subst(asm) shiftl_shiftr_id, simp add: range_cover_def) apply (subst word_unat_power, rule of_nat_mono_maybe) apply (rule power_strict_increasing) apply (simp add: word_bits_def) apply simp apply (erule order_less_le_trans) apply simp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (new_cap_addrs n ptr ko) proof (prove)
goal (1 subgoal):
 1. distinct (map (\<lambda>p. ptr + (word_of_nat p << objBitsKO ko)) [0..<n]) proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>p. ptr + (word_of_nat p << objBitsKO ko)) {0..<n} proof (prove)
goal (2 subgoals):
 1. inj_on word_of_nat {0..<n}
 2. inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (3 subgoals):
 1. inj_on word_of_nat ?B4
 2. {0..<n} \<subseteq> ?B4
 3. inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (2 subgoals):
 1. {0..<n} \<subseteq> unats LENGTH(32)
 2. inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; x < n\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH(32)
 2. inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; x < n; range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH(32)
 2. range_cover ptr sz (objBitsKO ko) n \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> n \<le> 2 ^ LENGTH(32)
 2. range_cover ptr sz (objBitsKO ko) n \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> n \<le> 2 ^ LENGTH(32)
 2. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - objBitsKO ko) \<le> 2 ^ LENGTH(32)
 2. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (sz - objBitsKO ko); objBitsKO ko = 0\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - objBitsKO ko) \<le> 2 ^ LENGTH(32)
 2. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (sz - objBitsKO ko); objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - objBitsKO ko) \<le> 2 ^ LENGTH(32)
 3. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (sz - objBitsKO ko); objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - objBitsKO ko) \<le> 2 ^ LENGTH(32)
 2. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (sz - objBitsKO ko); objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - objBitsKO ko) < 2 ^ LENGTH(32)
 2. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (sz - objBitsKO ko); objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> LENGTH(32) - objBitsKO ko < LENGTH(32)
 2. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (sz - objBitsKO ko); objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>0 \<le> x; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (sz - objBitsKO ko); objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko)\<rbrakk> \<Longrightarrow> inj_on (\<lambda>a. ptr + (a << objBitsKO ko)) (word_of_nat ` {0..<n}) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (LENGTH(32) - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); x \<in> word_of_nat ` {0..<n}; y \<in> word_of_nat ` {0..<n}; ptr + (x << objBitsKO ko) = ptr + (y << objBitsKO ko)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); word_of_nat xa << objBitsKO ko = word_of_nat xb << objBitsKO ko; xa < n; xb < n\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa << objBitsKO ko >> objBitsKO ko = word_of_nat xb << objBitsKO ko >> objBitsKO ko\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa << objBitsKO ko >> objBitsKO ko = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko = 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb
 2. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa << objBitsKO ko >> objBitsKO ko = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa << objBitsKO ko >> objBitsKO ko = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> word_of_nat xa < 2 ^ (LENGTH(32) - objBitsKO ko)
 2. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (3 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - objBitsKO ko) < 2 ^ LENGTH(32)
 2. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> xa < 2 ^ (LENGTH(32) - objBitsKO ko)
 3. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (4 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> LENGTH(32) - objBitsKO ko < LENGTH(32)
 2. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> xa < 2 ^ (LENGTH(32) - objBitsKO ko)
 4. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (3 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> xa < 2 ^ (LENGTH(32) - objBitsKO ko)
 3. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> xa < 2 ^ (LENGTH(32) - objBitsKO ko)
 2. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xb < n\<rbrakk> \<Longrightarrow> n \<le> 2 ^ (LENGTH(32) - objBitsKO ko)
 2. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb << objBitsKO ko >> objBitsKO ko; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> word_of_nat xb < 2 ^ (LENGTH(32) - objBitsKO ko)
 2. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (3 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH(32) - objBitsKO ko) < 2 ^ LENGTH(32)
 2. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> xb < 2 ^ (LENGTH(32) - objBitsKO ko)
 3. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (4 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> LENGTH(32) - objBitsKO ko < LENGTH(32)
 2. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> xb < 2 ^ (LENGTH(32) - objBitsKO ko)
 4. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (3 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> xb < 2 ^ (LENGTH(32) - objBitsKO ko)
 3. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n\<rbrakk> \<Longrightarrow> xb < 2 ^ (LENGTH(32) - objBitsKO ko)
 2. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>objBitsKO ko \<noteq> 0; range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n\<rbrakk> \<Longrightarrow> n \<le> 2 ^ (LENGTH(32) - objBitsKO ko)
 2. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; n \<le> 2 ^ (32 - objBitsKO ko); n \<le> 2 ^ (sz - objBitsKO ko); xa < n; xb < n; word_of_nat xa = word_of_nat xb; objBitsKO ko \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xb proof (prove)
goal:
No subgoals!