theory Untyped_R

lemma reset_addrs_same:
  "idx \<le> 2 ^ sz \<Longrightarrow> resetChunkBits \<le> sz
    \<Longrightarrow> ptr \<noteq> 0 \<Longrightarrow> is_aligned ptr sz \<Longrightarrow> sz < word_bits
    \<Longrightarrow> [ptr , ptr + 2 ^ resetChunkBits .e. getFreeRef ptr idx - 1]
    = (map (\<lambda>i. getFreeRef ptr (i * 2 ^ resetChunkBits))
        ([i\<leftarrow>[0..<2 ^ (sz - resetChunkBits)].
            i * 2 ^ resetChunkBits < idx]))" apply (simp add: upto_enum_step_def getFreeRef_def reset_ineq_eq_idx_0) apply (clarsimp simp: upto_enum_word o_def unat_div simp del: upt.simps) apply (subst unat_of_nat_minus_1) apply (rule_tac y="2 ^ sz" in order_le_less_trans, simp) apply (rule power_strict_increasing, simp_all add: word_bits_def)[1] apply simp apply (rule_tac f="map f" for f in arg_cong) apply (rule filter_upt_eq[symmetric]) apply clarsimp apply (erule order_le_less_trans[rotated]) apply simp apply (rule notI) apply (drule order_less_le_trans[where x="a * b" for a b],
      rule_tac m="2 ^ resetChunkBits" and n=idx in alignUp_ge_nat) apply simp+ apply (simp add: field_simps) apply (simp only: mult_Suc_right[symmetric]) apply (subst(asm) div_add_self1[where 'a=nat, simplified, symmetric]) apply simp apply (simp only: field_simps) apply simp apply clarsimp apply (rule order_le_less_trans, rule div_mult_le, simp) apply (simp add: Suc_le_eq td_gal_lt[symmetric] power_add[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> [ptr , ptr + 2 ^ resetChunkBits .e. getFreeRef ptr idx - 1] = map (\<lambda>i. getFreeRef ptr (i * 2 ^ resetChunkBits)) (filter (\<lambda>i. i * 2 ^ resetChunkBits < idx) [0..<2 ^ (sz - resetChunkBits)]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> 0 < idx \<longrightarrow> map (\<lambda>x. ptr + x * 2 ^ resetChunkBits) [0 .e. (word_of_nat idx - 1) div 2 ^ resetChunkBits] = map (\<lambda>i. ptr + word_of_nat i * 2 ^ resetChunkBits) (filter (\<lambda>i. i * 2 ^ resetChunkBits < idx) [0..<2 ^ (sz - resetChunkBits)]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> map (\<lambda>x. ptr + word_of_nat x * 2 ^ resetChunkBits) [0..<Suc (unat (word_of_nat idx - 1) div 2 ^ resetChunkBits)] = map (\<lambda>i. ptr + word_of_nat i * 2 ^ resetChunkBits) (filter (\<lambda>i. i * 2 ^ resetChunkBits < idx) [0..<2 ^ (sz - resetChunkBits)]) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx < 2 ^ LENGTH(32)
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx \<noteq> 0
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> map (\<lambda>x. ptr + word_of_nat x * 2 ^ resetChunkBits) [0..<Suc ((idx - 1) div 2 ^ resetChunkBits)] = map (\<lambda>i. ptr + word_of_nat i * 2 ^ resetChunkBits) (filter (\<lambda>i. i * 2 ^ resetChunkBits < idx) [0..<2 ^ (sz - resetChunkBits)]) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH(32)
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx \<noteq> 0
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> map (\<lambda>x. ptr + word_of_nat x * 2 ^ resetChunkBits) [0..<Suc ((idx - 1) div 2 ^ resetChunkBits)] = map (\<lambda>i. ptr + word_of_nat i * 2 ^ resetChunkBits) (filter (\<lambda>i. i * 2 ^ resetChunkBits < idx) [0..<2 ^ (sz - resetChunkBits)]) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx \<noteq> 0
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> map (\<lambda>x. ptr + word_of_nat x * 2 ^ resetChunkBits) [0..<Suc ((idx - 1) div 2 ^ resetChunkBits)] = map (\<lambda>i. ptr + word_of_nat i * 2 ^ resetChunkBits) (filter (\<lambda>i. i * 2 ^ resetChunkBits < idx) [0..<2 ^ (sz - resetChunkBits)]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> map (\<lambda>x. ptr + word_of_nat x * 2 ^ resetChunkBits) [0..<Suc ((idx - 1) div 2 ^ resetChunkBits)] = map (\<lambda>i. ptr + word_of_nat i * 2 ^ resetChunkBits) (filter (\<lambda>i. i * 2 ^ resetChunkBits < idx) [0..<2 ^ (sz - resetChunkBits)]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> [0..<Suc ((idx - 1) div 2 ^ resetChunkBits)] = filter (\<lambda>i. i * 2 ^ resetChunkBits < idx) [0..<2 ^ (sz - resetChunkBits)] proof (prove)
goal (4 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> \<forall>a b. a \<le> b \<longrightarrow> b * 2 ^ resetChunkBits < idx \<longrightarrow> a * 2 ^ resetChunkBits < idx
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> \<not> Suc ((idx - 1) div 2 ^ resetChunkBits) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 4. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; a \<le> b; b * 2 ^ resetChunkBits < idx\<rbrakk> \<Longrightarrow> a * 2 ^ resetChunkBits < idx
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> \<not> Suc ((idx - 1) div 2 ^ resetChunkBits) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 4. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; a \<le> b\<rbrakk> \<Longrightarrow> a * 2 ^ resetChunkBits \<le> b * 2 ^ resetChunkBits
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> \<not> Suc ((idx - 1) div 2 ^ resetChunkBits) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 4. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> \<not> Suc ((idx - 1) div 2 ^ resetChunkBits) * 2 ^ resetChunkBits < idx
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx; Suc ((idx - 1) div 2 ^ resetChunkBits) * 2 ^ resetChunkBits < idx\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> 0 < 2 ^ resetChunkBits
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx; Suc ((idx - 1) div 2 ^ resetChunkBits) * 2 ^ resetChunkBits < (idx + 2 ^ resetChunkBits - 1) div 2 ^ resetChunkBits * 2 ^ resetChunkBits\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 4. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx; 2 ^ resetChunkBits + (idx - Suc 0) div 2 ^ resetChunkBits * 2 ^ resetChunkBits < (idx + 2 ^ resetChunkBits - Suc 0) div 2 ^ resetChunkBits * 2 ^ resetChunkBits\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx; 2 ^ resetChunkBits + 2 ^ resetChunkBits * ((idx - Suc 0) div 2 ^ resetChunkBits) < 2 ^ resetChunkBits * ((idx + 2 ^ resetChunkBits - Suc 0) div 2 ^ resetChunkBits)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx; 2 ^ resetChunkBits * Suc ((idx - Suc 0) div 2 ^ resetChunkBits) < 2 ^ resetChunkBits * ((idx + 2 ^ resetChunkBits - Suc 0) div 2 ^ resetChunkBits)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> 0 < 2 ^ resetChunkBits
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx; 2 ^ resetChunkBits * ((2 ^ resetChunkBits + (idx - Suc 0)) div 2 ^ resetChunkBits) < 2 ^ resetChunkBits * ((idx + 2 ^ resetChunkBits - Suc 0) div 2 ^ resetChunkBits)\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 4. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx; 2 ^ resetChunkBits * ((2 ^ resetChunkBits + (idx - Suc 0)) div 2 ^ resetChunkBits) < 2 ^ resetChunkBits * ((idx + 2 ^ resetChunkBits - Suc 0) div 2 ^ resetChunkBits)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx; 2 ^ resetChunkBits * ((idx - Suc 0 + 2 ^ resetChunkBits) div 2 ^ resetChunkBits) < 2 ^ resetChunkBits * ((idx + 2 ^ resetChunkBits - Suc 0) div 2 ^ resetChunkBits)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 3. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<noteq> 0 \<longrightarrow> (Suc ((idx - 1) div 2 ^ resetChunkBits) - 1) * 2 ^ resetChunkBits < idx
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> (idx - Suc 0) div 2 ^ resetChunkBits * 2 ^ resetChunkBits < idx
 2. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; resetChunkBits \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> Suc ((idx - 1) div 2 ^ resetChunkBits) \<le> 2 ^ (sz - resetChunkBits) proof (prove)
goal:
No subgoals!