theory Untyped_AI

lemma range_cover_stuff:
  notes unat_power_lower_machine = unat_power_lower[where 'a=machine_word_len]
  notes unat_of_nat_machine = unat_of_nat_eq[where 'a=machine_word_len]
  notes is_aligned_neg_mask_eq[simp del]
  notes is_aligned_neg_mask_weaken[simp del]
  shows
  "\<lbrakk>0 < n;n \<le> unat ((2::machine_word) ^ sz - of_nat rv >> bits);
  rv \<le> 2^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow>
   rv \<le> unat (alignUp (w + of_nat rv) bits - w) \<and>
   (alignUp (w + of_nat rv) bits) && ~~ mask sz = w \<and>
   range_cover (alignUp (w + ((of_nat rv)::machine_word)) bits) sz bits n" apply (clarsimp simp: range_cover_def) proof (intro conjI) assume not_0 : "0<n" assume bound : "n \<le> unat ((2::machine_word) ^ sz - of_nat rv >> bits)" "rv\<le> 2^sz"
      "sz < word_bits" assume al: "is_aligned w sz" have space: "(2::machine_word) ^ sz - of_nat rv \<le> 2^ sz" apply (rule word_sub_le[OF word_of_nat_le]) apply (clarsimp simp: bound unat_power_lower_machine) done show cmp: "bits \<le> sz" using not_0 bound apply - apply (rule ccontr) apply (clarsimp simp: not_le) apply (drule le_trans) apply (rule word_le_nat_alt[THEN iffD1]) apply (rule le_shiftr[OF space]) apply (subgoal_tac "(2::machine_word)^sz >> bits = 0") apply simp apply (rule and_mask_eq_iff_shiftr_0[THEN iffD1]) apply (simp add: and_mask_eq_iff_le_mask) apply (case_tac "word_bits \<le> bits") apply (simp add: word_bits_def mask_def power_overflow) apply (subst le_mask_iff_lt_2n[THEN iffD1]) apply (simp add: word_bits_def) apply (simp add: word_less_nat_alt[THEN iffD2] unat_power_lower_machine) done have shiftr_t2n[simp]:"(2::machine_word)^sz >> bits = 2^ (sz - bits)" using bound cmp apply (case_tac "sz = 0",simp) apply (subgoal_tac "(1::machine_word) << sz >> bits = 2^ (sz -bits)") apply simp apply (subst shiftl_shiftr1) apply (simp_all add: word_size) apply (word_eqI_solve simp: word_bits_conv) done have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: machine_word) ^ sz" using bound cmp not_0 apply - apply (case_tac "rv = 0") apply simp apply (clarsimp simp: alignUp_def2) apply (subst mask_eq_x_eq_0[THEN iffD1]) apply (simp add: and_mask_eq_iff_le_mask mask_def) apply (simp add: p2_gt_0[where 'a=machine_word_len, folded word_bits_def]) apply (simp add: alignUp_def3) apply (subgoal_tac "1 \<le> unat (2 ^ sz - of_nat rv >> bits)") prefer 2 apply (erule le_trans[rotated]) apply clarsimp apply (thin_tac "n \<le> M" for M) apply (simp add: shiftr_div_2n') apply (simp add: td_gal[symmetric]) apply (subst (asm) unat_sub) apply (simp add: word_of_nat_le unat_power_lower_machine) apply (simp add: le_diff_conv2 word_of_nat_le unat_le_helper word_less_nat_alt) apply (rule le_less_trans[OF unat_plus_gt]) apply (rule less_le_trans[where y = "2^bits + unat (of_nat rv)"]) apply simp apply (rule le_less_trans[OF _ measure_unat]) apply (rule word_le_nat_alt[THEN iffD1]) apply (rule word_and_le2) apply (erule of_nat_neq_0) apply (subst word_bits_def[symmetric]) apply (erule le_less_trans) apply simp apply simp done show "n + unat (alignUp (w + ((of_nat rv)::machine_word)) bits && mask sz >> bits) \<le> 2 ^ (sz - bits)" using not_0 bound cmp apply - apply (erule le_trans[OF add_le_mono]) apply (rule le_refl) apply (clarsimp simp: power_sub field_simps td_gal[symmetric]) apply (subst (2) mult.commute) apply (subst unat_shiftl_absorb) apply (rule order_trans[OF le_shiftr]) apply (rule word_and_le1) apply (simp add: shiftr_mask2 word_bits_def) apply (simp add: mask_def) apply (rule word_sub_1_le) apply (simp add: word_bits_def)+ apply (simp add: shiftl_t2n[symmetric] field_simps shiftr_shiftl1) apply (subst is_aligned_neg_mask_eq) apply (rule is_aligned_andI1,simp) apply (subst mult.commute) apply (subst unat_shiftl_absorb[where p = "sz - bits"]) apply (rule order_trans[OF le_shiftr]) apply (rule space) apply (simp add: word_bits_def power_minus_is_div)+ apply (simp add: shiftl_t2n[symmetric] field_simps shiftr_shiftl1) apply (subst is_aligned_diff_neg_mask[OF is_aligned_weaken]) apply (rule is_aligned_triv) apply (simp add: word_bits_def)+ apply (subst unat_sub) apply (rule order_trans[OF word_and_le2]) apply (simp add: less_imp_le) apply (subst diff_add_assoc[symmetric]) apply (rule unat_le_helper) apply (rule order_trans[OF word_and_le2]) apply (simp add: less_imp_le[OF cmp2]) apply (clarsimp simp: field_simps word_bits_def is_aligned_neg_mask_eq) apply (simp add: le_diff_conv word_le_nat_alt[symmetric] word_and_le2) apply (simp add: alignUp_plus[OF is_aligned_weaken[OF al]]
                      is_aligned_add_helper[THEN conjunct1, OF al cmp2]) done show "rv \<le> unat (alignUp (w + of_nat rv) bits - w)" using bound not_0 cmp al apply - apply (clarsimp simp: alignUp_plus[OF is_aligned_weaken]) apply (case_tac "rv = 0") apply simp apply (rule le_trans[OF _ word_le_nat_alt[THEN iffD1,OF alignUp_ge]]) apply (subst unat_of_nat_machine) apply (erule le_less_trans) apply (rule power_strict_increasing) apply (simp_all add: word_bits_def)[4] apply (rule alignUp_is_aligned_nz[where x = "2^sz"]) apply (rule is_aligned_weaken[OF is_aligned_triv2]) apply (simp_all add: word_bits_def)[2] apply (subst word_of_nat_le) apply (subst unat_power_lower_machine) apply ((simp add: word_bits_def)+)[3] apply simp apply (erule of_nat_neq_0) apply (erule le_less_trans) apply (rule power_strict_increasing) apply (simp add: word_bits_def)+ done show "alignUp (w + of_nat rv) bits && ~~ mask sz = w" using bound not_0 cmp al apply (clarsimp simp: alignUp_plus[OF is_aligned_weaken]
                          mask_out_add_aligned[symmetric]) apply (clarsimp simp: and_not_mask) apply (subgoal_tac "alignUp ((of_nat rv)::machine_word) bits >> sz = 0") apply simp apply (simp add: le_mask_iff[symmetric] mask_def) done qed (simp add: word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w) \<and> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w \<and> range_cover (alignUp (w + word_of_nat rv) bits) sz bits n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w) \<and> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w \<and> sz < 32 \<and> bits \<le> sz \<and> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (state)
goal (5 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 3. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32
 4. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> bits \<le> sz
 5. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (state)
this:
0 < n

goal (5 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 3. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32
 4. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> bits \<le> sz
 5. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (state)
this:
n \<le> unat (2 ^ sz - word_of_nat rv >> bits)
rv \<le> 2 ^ sz
sz < word_bits

goal (5 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 3. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32
 4. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> bits \<le> sz
 5. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (state)
this:
is_aligned w sz

goal (5 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 3. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32
 4. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> bits \<le> sz
 5. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. 2 ^ sz - word_of_nat rv \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. rv \<le> unat (2 ^ sz) proof (prove)
goal:
No subgoals! proof (state)
this:
2 ^ sz - word_of_nat rv \<le> 2 ^ sz

goal (5 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 3. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32
 4. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> bits \<le> sz
 5. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. bits \<le> sz proof (prove)
using this:
0 < n
n \<le> unat (2 ^ sz - word_of_nat rv >> bits)
rv \<le> 2 ^ sz
sz < word_bits

goal (1 subgoal):
 1. bits \<le> sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits\<rbrakk> \<Longrightarrow> bits \<le> sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; \<not> bits \<le> sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; sz < bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits\<rbrakk> \<Longrightarrow> unat (2 ^ sz - word_of_nat rv >> bits) \<le> ?k6
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> ?k6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits\<rbrakk> \<Longrightarrow> 2 ^ sz - word_of_nat rv >> bits \<le> ?b10
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat ?b10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits); 2 ^ sz >> bits = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits)\<rbrakk> \<Longrightarrow> 2 ^ sz >> bits = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits)\<rbrakk> \<Longrightarrow> 2 ^ sz >> bits = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits)\<rbrakk> \<Longrightarrow> 2 ^ sz && mask bits = 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits)\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> mask bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits); word_bits \<le> bits\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> mask bits
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits); \<not> word_bits \<le> bits\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> mask bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits); \<not> word_bits \<le> bits\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> mask bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits); \<not> word_bits \<le> bits\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits); \<not> word_bits \<le> bits\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; sz < bits; n \<le> unat (2 ^ sz >> bits); \<not> word_bits \<le> bits\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ bits proof (prove)
goal:
No subgoals! proof (state)
this:
bits \<le> sz

goal (4 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 3. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32
 4. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. 2 ^ sz >> bits = 2 ^ (sz - bits) proof (prove)
using this:
n \<le> unat (2 ^ sz - word_of_nat rv >> bits)
rv \<le> 2 ^ sz
sz < word_bits
bits \<le> sz

goal (1 subgoal):
 1. 2 ^ sz >> bits = 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; sz \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ sz >> bits = 2 ^ (sz - bits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; sz \<noteq> 0; 1 << sz >> bits = 2 ^ (sz - bits)\<rbrakk> \<Longrightarrow> 2 ^ sz >> bits = 2 ^ (sz - bits)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; sz \<noteq> 0\<rbrakk> \<Longrightarrow> 1 << sz >> bits = 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; sz \<noteq> 0\<rbrakk> \<Longrightarrow> 1 << sz >> bits = 2 ^ (sz - bits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; sz \<noteq> 0\<rbrakk> \<Longrightarrow> bits \<le> sz
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; sz \<noteq> 0\<rbrakk> \<Longrightarrow> 1 && mask (size 1 - sz) << sz - bits = 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < sz\<rbrakk> \<Longrightarrow> 1 && mask (32 - sz) << sz - bits = 2 ^ (sz - bits) proof (prove)
goal:
No subgoals! proof (state)
this:
2 ^ sz >> bits = 2 ^ (sz - bits)

goal (4 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 3. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32
 4. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. alignUp (word_of_nat rv) bits < 2 ^ sz proof (prove)
using this:
n \<le> unat (2 ^ sz - word_of_nat rv >> bits)
rv \<le> 2 ^ sz
sz < word_bits
bits \<le> sz
0 < n

goal (1 subgoal):
 1. alignUp (word_of_nat rv) bits < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; rv = 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits < 2 ^ sz
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> 2 ^ (sz - bits); sz < word_bits; bits \<le> sz; 0 < n; rv = 0\<rbrakk> \<Longrightarrow> alignUp 0 bits < 2 ^ sz
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> 2 ^ (sz - bits); sz < word_bits; bits \<le> sz; 0 < n; rv = 0\<rbrakk> \<Longrightarrow> 2 ^ bits - 1 && ~~ mask bits < 2 ^ sz
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits < 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<le> 2 ^ (sz - bits); sz < word_bits; bits \<le> sz; 0 < n; rv = 0\<rbrakk> \<Longrightarrow> 2 ^ bits - 1 && mask bits = 2 ^ bits - 1
 2. \<lbrakk>n \<le> 2 ^ (sz - bits); sz < word_bits; bits \<le> sz; 0 < n; rv = 0\<rbrakk> \<Longrightarrow> 0 < 2 ^ sz
 3. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> 2 ^ (sz - bits); sz < word_bits; bits \<le> sz; 0 < n; rv = 0\<rbrakk> \<Longrightarrow> 0 < 2 ^ sz
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 1 \<le> unat (2 ^ sz - word_of_nat rv >> bits)\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv\<rbrakk> \<Longrightarrow> 1 \<le> unat (2 ^ sz - word_of_nat rv >> bits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv\<rbrakk> \<Longrightarrow> 1 \<le> unat (2 ^ sz - word_of_nat rv >> bits)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 1 \<le> unat (2 ^ sz - word_of_nat rv >> bits)\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv\<rbrakk> \<Longrightarrow> 1 \<le> n
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 1 \<le> unat (2 ^ sz - word_of_nat rv >> bits)\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 1 \<le> unat (2 ^ sz - word_of_nat rv >> bits)\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 1 \<le> unat (2 ^ sz - word_of_nat rv >> bits)\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; Suc 0 \<le> unat (2 ^ sz - word_of_nat rv) div 2 ^ bits\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits \<le> unat (2 ^ sz - word_of_nat rv)\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv\<rbrakk> \<Longrightarrow> word_of_nat rv \<le> 2 ^ sz
 2. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits \<le> unat (2 ^ sz) - unat (word_of_nat rv)\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits \<le> unat (2 ^ sz) - unat (word_of_nat rv)\<rbrakk> \<Longrightarrow> 2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> unat (2 ^ bits + (word_of_nat rv - 1 && ~~ mask bits)) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> unat (2 ^ bits) + unat (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> unat (2 ^ bits) + unat (word_of_nat rv - 1 && ~~ mask bits) < 2 ^ bits + unat (word_of_nat rv)
 2. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> unat (word_of_nat rv - 1 && ~~ mask bits) < unat (word_of_nat rv)
 2. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> unat (word_of_nat rv - 1 && ~~ mask bits) \<le> unat (word_of_nat rv - 1)
 2. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0
 3. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> word_of_nat rv - 1 && ~~ mask bits \<le> word_of_nat rv - 1
 2. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0
 3. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0
 2. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> rv < 2 ^ LENGTH(32)
 2. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> rv < 2 ^ word_bits
 2. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < word_bits; bits \<le> sz; 0 < n; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ word_bits
 2. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz; 0 < n; 0 < rv; 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ bits + unat (word_of_nat rv) \<le> 2 ^ sz proof (prove)
goal:
No subgoals! proof (state)
this:
alignUp (word_of_nat rv) bits < 2 ^ sz

goal (4 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 3. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32
 4. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (prove)
using this:
0 < n
n \<le> unat (2 ^ sz - word_of_nat rv >> bits)
rv \<le> 2 ^ sz
sz < word_bits
bits \<le> sz

goal (1 subgoal):
 1. n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> ?l6
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (2 ^ sz - word_of_nat rv >> bits) + ?l6 \<le> 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (2 ^ sz - word_of_nat rv >> bits) + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) + 2 ^ bits * unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) * 2 ^ bits \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && mask sz >> bits \<le> 2 ^ ?p10
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> ?p10 + bits < LENGTH(32)
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) + unat ((alignUp (w + word_of_nat rv) bits && mask sz >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && mask sz \<le> ?v12
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> ?v12 >> bits \<le> 2 ^ ?p10
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> ?p10 + bits < LENGTH(32)
 4. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) + unat ((alignUp (w + word_of_nat rv) bits && mask sz >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> mask sz >> bits \<le> 2 ^ ?p10
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> ?p10 + bits < LENGTH(32)
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) + unat ((alignUp (w + word_of_nat rv) bits && mask sz >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> mask (sz - bits) \<le> 2 ^ ?p10
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> ?p10 + bits < LENGTH(32)
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) + unat ((alignUp (w + word_of_nat rv) bits && mask sz >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ (sz - bits) - 1 \<le> 2 ^ ?p10
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> ?p10 + bits < LENGTH(32)
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) + unat ((alignUp (w + word_of_nat rv) bits && mask sz >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ (sz - bits) \<noteq> 0
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> sz - bits + bits < LENGTH(32)
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < word_bits; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) + unat ((alignUp (w + word_of_nat rv) bits && mask sz >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) + unat ((alignUp (w + word_of_nat rv) bits && mask sz >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat ((alignUp (w + word_of_nat rv) bits && mask sz) && ~~ mask bits) + 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> is_aligned (alignUp (w + word_of_nat rv) bits && mask sz) bits
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + 2 ^ bits * unat (2 ^ sz - word_of_nat rv >> bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat (2 ^ sz - word_of_nat rv >> bits) * 2 ^ bits \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ sz - word_of_nat rv >> bits \<le> 2 ^ (sz - bits)
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> sz - bits + bits < LENGTH(32)
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat ((2 ^ sz - word_of_nat rv >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ sz - word_of_nat rv \<le> ?v47
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> ?v47 >> bits \<le> 2 ^ (sz - bits)
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> sz - bits + bits < LENGTH(32)
 4. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat ((2 ^ sz - word_of_nat rv >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ sz >> bits \<le> 2 ^ (sz - bits)
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> sz - bits + bits < LENGTH(32)
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat ((2 ^ sz - word_of_nat rv >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat ((2 ^ sz - word_of_nat rv >> bits) * 2 ^ bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat (2 ^ sz - word_of_nat rv && ~~ mask bits) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> is_aligned (2 ^ sz) ?x50
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> bits \<le> ?x50
 3. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat (2 ^ sz - (alignUp (word_of_nat rv) bits && ~~ mask bits)) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> bits \<le> sz
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat (2 ^ sz - (alignUp (word_of_nat rv) bits && ~~ mask bits)) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat (2 ^ sz - (alignUp (word_of_nat rv) bits && ~~ mask bits)) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits && ~~ mask bits \<le> 2 ^ sz
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + (unat (2 ^ sz) - unat (alignUp (word_of_nat rv) bits && ~~ mask bits)) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits \<le> 2 ^ sz
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + (unat (2 ^ sz) - unat (alignUp (word_of_nat rv) bits && ~~ mask bits)) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + (unat (2 ^ sz) - unat (alignUp (word_of_nat rv) bits && ~~ mask bits)) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (word_of_nat rv) bits && ~~ mask bits) \<le> unat (2 ^ sz)
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat (2 ^ sz) - unat (alignUp (word_of_nat rv) bits && ~~ mask bits) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits && ~~ mask bits \<le> word_of_nat (unat (2 ^ sz))
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat (2 ^ sz) - unat (alignUp (word_of_nat rv) bits && ~~ mask bits) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits \<le> word_of_nat (unat (2 ^ sz))
 2. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat (2 ^ sz) - unat (alignUp (word_of_nat rv) bits && ~~ mask bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> unat (alignUp (w + word_of_nat rv) bits && mask sz) + unat (2 ^ sz) - unat (alignUp (word_of_nat rv) bits && ~~ mask bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ sz + unat (alignUp (w + word_of_nat rv) bits && mask sz) - unat (alignUp (word_of_nat rv) bits) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rv \<le> 2 ^ sz; sz < 32; bits \<le> sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && mask sz \<le> alignUp (word_of_nat rv) bits proof (prove)
goal:
No subgoals! proof (state)
this:
n + unat (alignUp (w + word_of_nat rv) bits && mask sz >> bits) \<le> 2 ^ (sz - bits)

goal (3 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 3. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32 proof (prove)
goal (1 subgoal):
 1. rv \<le> unat (alignUp (w + word_of_nat rv) bits - w) proof (prove)
using this:
n \<le> unat (2 ^ sz - word_of_nat rv >> bits)
rv \<le> 2 ^ sz
sz < word_bits
0 < n
bits \<le> sz
is_aligned w sz

goal (1 subgoal):
 1. rv \<le> unat (alignUp (w + word_of_nat rv) bits - w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (w + word_of_nat rv) bits - w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (word_of_nat rv) bits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv = 0\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (word_of_nat rv) bits)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (word_of_nat rv) bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> rv \<le> unat (alignUp (word_of_nat rv) bits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> rv \<le> unat (word_of_nat rv)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 3. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> rv < 2 ^ LENGTH(32)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> rv \<le> rv
 3. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 4. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH(32)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> rv \<le> rv
 3. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 4. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits \<noteq> 0 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> rv \<le> rv
 4. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 5. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (2 ^ sz) bits
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 3. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat rv \<le> 2 ^ sz
 4. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> bits \<le> sz
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 3. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat rv \<le> 2 ^ sz
 4. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat rv \<le> 2 ^ sz
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> rv \<le> unat (2 ^ sz)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> True
 3. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> rv \<le> 2 ^ sz
 3. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> True
 4. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; rv \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; 0 < rv\<rbrakk> \<Longrightarrow> word_of_nat rv \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> rv < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> 1 < 2 proof (prove)
goal:
No subgoals! proof (state)
this:
rv \<le> unat (alignUp (w + word_of_nat rv) bits - w)

goal (2 subgoals):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w
 2. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32 proof (prove)
goal (1 subgoal):
 1. alignUp (w + word_of_nat rv) bits && ~~ mask sz = w proof (prove)
using this:
n \<le> unat (2 ^ sz - word_of_nat rv >> bits)
rv \<le> 2 ^ sz
sz < word_bits
0 < n
bits \<le> sz
is_aligned w sz

goal (1 subgoal):
 1. alignUp (w + word_of_nat rv) bits && ~~ mask sz = w proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits && ~~ mask sz = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits >> sz << sz = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz; alignUp (word_of_nat rv) bits >> sz = 0\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits >> sz << sz = 0
 2. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits >> sz = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; 0 < n; bits \<le> sz; is_aligned w sz\<rbrakk> \<Longrightarrow> alignUp (word_of_nat rv) bits >> sz = 0 proof (prove)
goal:
No subgoals! proof (state)
this:
alignUp (w + word_of_nat rv) bits && ~~ mask sz = w

goal (1 subgoal):
 1. \<lbrakk>0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); rv \<le> 2 ^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow> sz < 32