BT00WW · Bertrand theorem

bertrand_hj_base_window_thirty_two_from_total

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

All six roots 32 through 37 satisfy both RFC-v1 H/J base bounds.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ s. ∀ e. ∀ h. ∀ u. ∀ j. ∀ g. (∀ x. ∀ y. ∃ z. Pow(x,y,z)) → Lt(31,s) → Le(s,37) → CeilDivSix(s · s,e) → Pow(s + 1,2 · s + 2,h) → Pow(4,e,u) → Pow(s + 7,12,j) → Pow(4,s + 5,g) → Le(h,u) ∧ Le(j,g)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0020 Pow PD0052 CeilDivSix

10 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0020 Pow PD0052 CeilDivSix

29 occurrences

Exact expanded native-PA statement
forall s e h u j g. (forall bpt_a_hj32_base bpt_e_hj32_base. exists bpt_x_hj32_base. (exists ff_b_bpt_value_hj32_base ff_c_bpt_value_hj32_base. ((forall ff_i_bpt_value_hj32_base_repeat. (exists ff_lt_bpt_value_hj32_base_repeat_bound. ff_lt_bpt_value_hj32_base_repeat_bound + S ff_i_bpt_value_hj32_base_repeat = bpt_e_hj32_base) -> (((exists ff_h_bpt_value_hj32_base_repeat_decoded. ff_h_bpt_value_hj32_base_repeat_decoded + S (bpt_a_hj32_base) = S ((S (ff_i_bpt_value_hj32_base_repeat)) * ff_c_bpt_value_hj32_base)) /\ exists ff_q_bpt_value_hj32_base_repeat_decoded. ff_b_bpt_value_hj32_base = ff_q_bpt_value_hj32_base_repeat_decoded * S ((S (ff_i_bpt_value_hj32_base_repeat)) * ff_c_bpt_value_hj32_base) + (bpt_a_hj32_base)))) /\ (exists ff_u_bpt_value_hj32_base_product ff_v_bpt_value_hj32_base_product. ((((exists ff_h_bpt_value_hj32_base_product_start. ff_h_bpt_value_hj32_base_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_start. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_start * S ((S (0)) * ff_v_bpt_value_hj32_base_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_base_product_terminal. ff_h_bpt_value_hj32_base_product_terminal + S (bpt_x_hj32_base) = S ((S (bpt_e_hj32_base)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_terminal. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_terminal * S ((S (bpt_e_hj32_base)) * ff_v_bpt_value_hj32_base_product) + (bpt_x_hj32_base))) /\ forall ff_i_bpt_value_hj32_base_product. (exists ff_lt_bpt_value_hj32_base_product_bound. ff_lt_bpt_value_hj32_base_product_bound + S ff_i_bpt_value_hj32_base_product = bpt_e_hj32_base) -> exists ff_p_bpt_value_hj32_base_product ff_r_bpt_value_hj32_base_product ff_s_bpt_value_hj32_base_product. ((((exists ff_h_bpt_value_hj32_base_product_factor. ff_h_bpt_value_hj32_base_product_factor + S (ff_p_bpt_value_hj32_base_product) = S ((S (ff_i_bpt_value_hj32_base_product)) * ff_c_bpt_value_hj32_base)) /\ exists ff_q_bpt_value_hj32_base_product_factor. ff_b_bpt_value_hj32_base = ff_q_bpt_value_hj32_base_product_factor * S ((S (ff_i_bpt_value_hj32_base_product)) * ff_c_bpt_value_hj32_base) + (ff_p_bpt_value_hj32_base_product))) /\ ((((exists ff_h_bpt_value_hj32_base_product_partial. ff_h_bpt_value_hj32_base_product_partial + S (ff_r_bpt_value_hj32_base_product) = S ((S (ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_partial. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_partial * S ((S (ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product) + (ff_r_bpt_value_hj32_base_product))) /\ ((((exists ff_h_bpt_value_hj32_base_product_successor. ff_h_bpt_value_hj32_base_product_successor + S (ff_s_bpt_value_hj32_base_product) = S ((S (S ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_successor. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_successor * S ((S (S ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product) + (ff_s_bpt_value_hj32_base_product))) /\ ff_s_bpt_value_hj32_base_product = ff_r_bpt_value_hj32_base_product * ff_p_bpt_value_hj32_base_product))))))))) -> (exists bqb_le_gap_hj32_base_lower. bqb_le_gap_hj32_base_lower + (32) = (s)) -> (exists bqb_le_gap_hj32_base_upper. bqb_le_gap_hj32_base_upper + (s) = (37)) -> (((exists bcs_lower_gap_hj32_base_ceiling. bcs_lower_gap_hj32_base_ceiling + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_hj32_base_ceiling. bcs_upper_gap_hj32_base_ceiling + S (6 * (e)) = (s * s) + 6)) -> (exists pa_b_hj32_base_h pa_c_hj32_base_h. ((forall pa_i_hj32_base_h_repeat. (exists pa_lt_hj32_base_h_repeat_bound. pa_lt_hj32_base_h_repeat_bound + S pa_i_hj32_base_h_repeat = 2 * s + 2) -> (((exists pa_h_hj32_base_h_repeat_decoded. pa_h_hj32_base_h_repeat_decoded + S (s + 1) = S ((S (pa_i_hj32_base_h_repeat)) * pa_c_hj32_base_h)) /\ exists pa_q_hj32_base_h_repeat_decoded. pa_b_hj32_base_h = pa_q_hj32_base_h_repeat_decoded * S ((S (pa_i_hj32_base_h_repeat)) * pa_c_hj32_base_h) + (s + 1)))) /\ (exists pa_u_hj32_base_h_product pa_v_hj32_base_h_product. ((((exists pa_h_hj32_base_h_product_start. pa_h_hj32_base_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_h_product)) /\ exists pa_q_hj32_base_h_product_start. pa_u_hj32_base_h_product = pa_q_hj32_base_h_product_start * S ((S (0)) * pa_v_hj32_base_h_product) + (1))) /\ ((((exists pa_h_hj32_base_h_product_terminal. pa_h_hj32_base_h_product_terminal + S (h) = S ((S (2 * s + 2)) * pa_v_hj32_base_h_product)) /\ exists pa_q_hj32_base_h_product_terminal. pa_u_hj32_base_h_product = pa_q_hj32_base_h_product_terminal * S ((S (2 * s + 2)) * pa_v_hj32_base_h_product) + (h))) /\ forall pa_i_hj32_base_h_product. (exists pa_lt_hj32_base_h_product_bound. pa_lt_hj32_base_h_product_bound + S pa_i_hj32_base_h_product = 2 * s + 2) -> exists pa_p_hj32_base_h_product pa_r_hj32_base_h_product pa_s_hj32_base_h_product. ((((exists pa_h_hj32_base_h_product_factor. pa_h_hj32_base_h_product_factor + S (pa_p_hj32_base_h_product) = S ((S (pa_i_hj32_base_h_product)) * pa_c_hj32_base_h)) /\ exists pa_q_hj32_base_h_product_factor. pa_b_hj32_base_h = pa_q_hj32_base_h_product_factor * S ((S (pa_i_hj32_base_h_product)) * pa_c_hj32_base_h) + (pa_p_hj32_base_h_product))) /\ ((((exists pa_h_hj32_base_h_product_partial. pa_h_hj32_base_h_product_partial + S (pa_r_hj32_base_h_product) = S ((S (pa_i_hj32_base_h_product)) * pa_v_hj32_base_h_product)) /\ exists pa_q_hj32_base_h_product_partial. pa_u_hj32_base_h_product = pa_q_hj32_base_h_product_partial * S ((S (pa_i_hj32_base_h_product)) * pa_v_hj32_base_h_product) + (pa_r_hj32_base_h_product))) /\ ((((exists pa_h_hj32_base_h_product_successor. pa_h_hj32_base_h_product_successor + S (pa_s_hj32_base_h_product) = S ((S (S pa_i_hj32_base_h_product)) * pa_v_hj32_base_h_product)) /\ exists pa_q_hj32_base_h_product_successor. pa_u_hj32_base_h_product = pa_q_hj32_base_h_product_successor * S ((S (S pa_i_hj32_base_h_product)) * pa_v_hj32_base_h_product) + (pa_s_hj32_base_h_product))) /\ pa_s_hj32_base_h_product = pa_r_hj32_base_h_product * pa_p_hj32_base_h_product)))))))) -> (exists pa_b_hj32_base_h_bound pa_c_hj32_base_h_bound. ((forall pa_i_hj32_base_h_bound_repeat. (exists pa_lt_hj32_base_h_bound_repeat_bound. pa_lt_hj32_base_h_bound_repeat_bound + S pa_i_hj32_base_h_bound_repeat = e) -> (((exists pa_h_hj32_base_h_bound_repeat_decoded. pa_h_hj32_base_h_bound_repeat_decoded + S (4) = S ((S (pa_i_hj32_base_h_bound_repeat)) * pa_c_hj32_base_h_bound)) /\ exists pa_q_hj32_base_h_bound_repeat_decoded. pa_b_hj32_base_h_bound = pa_q_hj32_base_h_bound_repeat_decoded * S ((S (pa_i_hj32_base_h_bound_repeat)) * pa_c_hj32_base_h_bound) + (4)))) /\ (exists pa_u_hj32_base_h_bound_product pa_v_hj32_base_h_bound_product. ((((exists pa_h_hj32_base_h_bound_product_start. pa_h_hj32_base_h_bound_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_h_bound_product)) /\ exists pa_q_hj32_base_h_bound_product_start. pa_u_hj32_base_h_bound_product = pa_q_hj32_base_h_bound_product_start * S ((S (0)) * pa_v_hj32_base_h_bound_product) + (1))) /\ ((((exists pa_h_hj32_base_h_bound_product_terminal. pa_h_hj32_base_h_bound_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_base_h_bound_product)) /\ exists pa_q_hj32_base_h_bound_product_terminal. pa_u_hj32_base_h_bound_product = pa_q_hj32_base_h_bound_product_terminal * S ((S (e)) * pa_v_hj32_base_h_bound_product) + (u))) /\ forall pa_i_hj32_base_h_bound_product. (exists pa_lt_hj32_base_h_bound_product_bound. pa_lt_hj32_base_h_bound_product_bound + S pa_i_hj32_base_h_bound_product = e) -> exists pa_p_hj32_base_h_bound_product pa_r_hj32_base_h_bound_product pa_s_hj32_base_h_bound_product. ((((exists pa_h_hj32_base_h_bound_product_factor. pa_h_hj32_base_h_bound_product_factor + S (pa_p_hj32_base_h_bound_product) = S ((S (pa_i_hj32_base_h_bound_product)) * pa_c_hj32_base_h_bound)) /\ exists pa_q_hj32_base_h_bound_product_factor. pa_b_hj32_base_h_bound = pa_q_hj32_base_h_bound_product_factor * S ((S (pa_i_hj32_base_h_bound_product)) * pa_c_hj32_base_h_bound) + (pa_p_hj32_base_h_bound_product))) /\ ((((exists pa_h_hj32_base_h_bound_product_partial. pa_h_hj32_base_h_bound_product_partial + S (pa_r_hj32_base_h_bound_product) = S ((S (pa_i_hj32_base_h_bound_product)) * pa_v_hj32_base_h_bound_product)) /\ exists pa_q_hj32_base_h_bound_product_partial. pa_u_hj32_base_h_bound_product = pa_q_hj32_base_h_bound_product_partial * S ((S (pa_i_hj32_base_h_bound_product)) * pa_v_hj32_base_h_bound_product) + (pa_r_hj32_base_h_bound_product))) /\ ((((exists pa_h_hj32_base_h_bound_product_successor. pa_h_hj32_base_h_bound_product_successor + S (pa_s_hj32_base_h_bound_product) = S ((S (S pa_i_hj32_base_h_bound_product)) * pa_v_hj32_base_h_bound_product)) /\ exists pa_q_hj32_base_h_bound_product_successor. pa_u_hj32_base_h_bound_product = pa_q_hj32_base_h_bound_product_successor * S ((S (S pa_i_hj32_base_h_bound_product)) * pa_v_hj32_base_h_bound_product) + (pa_s_hj32_base_h_bound_product))) /\ pa_s_hj32_base_h_bound_product = pa_r_hj32_base_h_bound_product * pa_p_hj32_base_h_bound_product)))))))) -> (exists pa_b_hj32_base_j pa_c_hj32_base_j. ((forall pa_i_hj32_base_j_repeat. (exists pa_lt_hj32_base_j_repeat_bound. pa_lt_hj32_base_j_repeat_bound + S pa_i_hj32_base_j_repeat = 12) -> (((exists pa_h_hj32_base_j_repeat_decoded. pa_h_hj32_base_j_repeat_decoded + S (s + 7) = S ((S (pa_i_hj32_base_j_repeat)) * pa_c_hj32_base_j)) /\ exists pa_q_hj32_base_j_repeat_decoded. pa_b_hj32_base_j = pa_q_hj32_base_j_repeat_decoded * S ((S (pa_i_hj32_base_j_repeat)) * pa_c_hj32_base_j) + (s + 7)))) /\ (exists pa_u_hj32_base_j_product pa_v_hj32_base_j_product. ((((exists pa_h_hj32_base_j_product_start. pa_h_hj32_base_j_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_start. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_start * S ((S (0)) * pa_v_hj32_base_j_product) + (1))) /\ ((((exists pa_h_hj32_base_j_product_terminal. pa_h_hj32_base_j_product_terminal + S (j) = S ((S (12)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_terminal. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_terminal * S ((S (12)) * pa_v_hj32_base_j_product) + (j))) /\ forall pa_i_hj32_base_j_product. (exists pa_lt_hj32_base_j_product_bound. pa_lt_hj32_base_j_product_bound + S pa_i_hj32_base_j_product = 12) -> exists pa_p_hj32_base_j_product pa_r_hj32_base_j_product pa_s_hj32_base_j_product. ((((exists pa_h_hj32_base_j_product_factor. pa_h_hj32_base_j_product_factor + S (pa_p_hj32_base_j_product) = S ((S (pa_i_hj32_base_j_product)) * pa_c_hj32_base_j)) /\ exists pa_q_hj32_base_j_product_factor. pa_b_hj32_base_j = pa_q_hj32_base_j_product_factor * S ((S (pa_i_hj32_base_j_product)) * pa_c_hj32_base_j) + (pa_p_hj32_base_j_product))) /\ ((((exists pa_h_hj32_base_j_product_partial. pa_h_hj32_base_j_product_partial + S (pa_r_hj32_base_j_product) = S ((S (pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_partial. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_partial * S ((S (pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product) + (pa_r_hj32_base_j_product))) /\ ((((exists pa_h_hj32_base_j_product_successor. pa_h_hj32_base_j_product_successor + S (pa_s_hj32_base_j_product) = S ((S (S pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_successor. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_successor * S ((S (S pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product) + (pa_s_hj32_base_j_product))) /\ pa_s_hj32_base_j_product = pa_r_hj32_base_j_product * pa_p_hj32_base_j_product)))))))) -> (exists pa_b_hj32_base_j_bound pa_c_hj32_base_j_bound. ((forall pa_i_hj32_base_j_bound_repeat. (exists pa_lt_hj32_base_j_bound_repeat_bound. pa_lt_hj32_base_j_bound_repeat_bound + S pa_i_hj32_base_j_bound_repeat = s + 5) -> (((exists pa_h_hj32_base_j_bound_repeat_decoded. pa_h_hj32_base_j_bound_repeat_decoded + S (4) = S ((S (pa_i_hj32_base_j_bound_repeat)) * pa_c_hj32_base_j_bound)) /\ exists pa_q_hj32_base_j_bound_repeat_decoded. pa_b_hj32_base_j_bound = pa_q_hj32_base_j_bound_repeat_decoded * S ((S (pa_i_hj32_base_j_bound_repeat)) * pa_c_hj32_base_j_bound) + (4)))) /\ (exists pa_u_hj32_base_j_bound_product pa_v_hj32_base_j_bound_product. ((((exists pa_h_hj32_base_j_bound_product_start. pa_h_hj32_base_j_bound_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_start. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_start * S ((S (0)) * pa_v_hj32_base_j_bound_product) + (1))) /\ ((((exists pa_h_hj32_base_j_bound_product_terminal. pa_h_hj32_base_j_bound_product_terminal + S (g) = S ((S (s + 5)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_terminal. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_terminal * S ((S (s + 5)) * pa_v_hj32_base_j_bound_product) + (g))) /\ forall pa_i_hj32_base_j_bound_product. (exists pa_lt_hj32_base_j_bound_product_bound. pa_lt_hj32_base_j_bound_product_bound + S pa_i_hj32_base_j_bound_product = s + 5) -> exists pa_p_hj32_base_j_bound_product pa_r_hj32_base_j_bound_product pa_s_hj32_base_j_bound_product. ((((exists pa_h_hj32_base_j_bound_product_factor. pa_h_hj32_base_j_bound_product_factor + S (pa_p_hj32_base_j_bound_product) = S ((S (pa_i_hj32_base_j_bound_product)) * pa_c_hj32_base_j_bound)) /\ exists pa_q_hj32_base_j_bound_product_factor. pa_b_hj32_base_j_bound = pa_q_hj32_base_j_bound_product_factor * S ((S (pa_i_hj32_base_j_bound_product)) * pa_c_hj32_base_j_bound) + (pa_p_hj32_base_j_bound_product))) /\ ((((exists pa_h_hj32_base_j_bound_product_partial. pa_h_hj32_base_j_bound_product_partial + S (pa_r_hj32_base_j_bound_product) = S ((S (pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_partial. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_partial * S ((S (pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product) + (pa_r_hj32_base_j_bound_product))) /\ ((((exists pa_h_hj32_base_j_bound_product_successor. pa_h_hj32_base_j_bound_product_successor + S (pa_s_hj32_base_j_bound_product) = S ((S (S pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_successor. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_successor * S ((S (S pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product) + (pa_s_hj32_base_j_bound_product))) /\ pa_s_hj32_base_j_bound_product = pa_r_hj32_base_j_bound_product * pa_p_hj32_base_j_bound_product)))))))) -> ((exists bqb_le_gap_hj32_base_h_result. bqb_le_gap_hj32_base_h_result + (h) = (u)) /\ (exists bqb_le_gap_hj32_base_j_result. bqb_le_gap_hj32_base_j_result + (j) = (g)))

Proof neighborhood

Direct theorem prerequisites

BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT000J le_antisymm BT00WP bertrand_h_root_32_from_total BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total

Direct theorem dependents

BT00X2 bertrand_hj_six_block_iterate_from_total

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

241 script commands · 49 reading checkpoints · 30 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (10)
le eq or ltle of succ le succle antisymmbertrand h root 32 from totalbertrand h root 33 from totalbertrand h root 34 from totalbertrand h root 35 from totalbertrand h root 36 from totalbertrand h root 37 from totalbertrand j base thirty two window from total
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro s
  2. L2
    intro e
  3. L3
    intro h
  4. L4
    intro u
  5. L5
    intro j
  6. L6
    intro g
  7. L7
    intro htotal
  8. L8
    intro hlower
  9. L9
    intro hupper
  10. L10
    intro hceiling
02Fix variables and assumptionsL11–14

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hh
  2. L12
    intro hu
  3. L13
    intro hj
  4. L14
    intro hg
03Establish hjresultL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand j base thirty two window from total.

  1. L15
    have hjresult : Le(j,g)Definitions: Le(j,g)Original native command in the exact edition
  2. L16
    specialize bertrand_j_base_thirty_two_window_from_total s
  3. L17
    specialize bertrand_j_base_thirty_two_window_from_total j
  4. L18
    specialize bertrand_j_base_thirty_two_window_from_total g
  5. L19
    apply bertrand_j_base_thirty_two_window_from_total
  6. L20
    exact htotal
  7. L21
    exact hlower
  8. L22
    exact hupper
  9. L23
    exact hj
  10. L24
    exact hg
04Establish hcap_cases_37L25–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L25
    have hcap_cases_37 : s = 37 ∨ Lt(s,37)Definitions: Lt(s,37)Original native command in the exact edition
  2. L26
    specialize le_eq_or_lt s
  3. L27
    specialize le_eq_or_lt 37
  4. L28
    apply le_eq_or_lt
  5. L29
    exact hupper
05Separate the logical casesL30–30

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L30
    cases hcap_cases_37
06Establish hcap_37_ceilingL31–36

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hcap_37_ceiling : CeilDivSix(37 · 37,e)Definitions: CeilDivSix(37 · 37,e)Original native command in the exact edition
  2. L32
    rewrite <- hcap_cases_37_left
  3. L33
    rewrite <- hcap_cases_37_left
  4. L34
    rewrite <- hcap_cases_37_left
  5. L35
    rewrite <- hcap_cases_37_left
  6. L36
    exact hceiling
07Establish hcap_37_powerL37–44

Establish this local claim before using it. It is not an additional assumption.

  1. L37
    have hcap_37_power : Pow(37 + 1,2 · 37 + 2,h)Definitions: Pow(37 + 1,2 · 37 + 2,h)Original native command in the exact edition
  2. L38
    rewrite <- hcap_cases_37_left
  3. L39
    rewrite <- hcap_cases_37_left
  4. L40
    rewrite <- hcap_cases_37_left
  5. L41
    rewrite <- hcap_cases_37_left
  6. L42
    rewrite <- hcap_cases_37_left
  7. L43
    rewrite <- hcap_cases_37_left
  8. L44
    exact hh
08Establish hcap_37_resultL45–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand h root 37 from total.

  1. L45
    have hcap_37_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L46
    specialize bertrand_h_root_37_from_total e
  3. L47
    specialize bertrand_h_root_37_from_total h
  4. L48
    specialize bertrand_h_root_37_from_total u
  5. L49
    apply bertrand_h_root_37_from_total
  6. L50
    exact htotal
  7. L51
    exact hcap_37_ceiling
  8. L52
    exact hcap_37_power
  9. L53
    exact hu
09Separate the logical casesL54–54

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    split
10Use earlier factsL55–56

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L55
    exact hcap_37_result
  2. L56
    exact hjresult
11Establish hcap_le_36L57–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L57
    have hcap_le_36 : Le(s,36)Definitions: Le(s,36)Original native command in the exact edition
  2. L58
    specialize le_of_succ_le_succ s
  3. L59
    specialize le_of_succ_le_succ 36
  4. L60
    apply le_of_succ_le_succ
  5. L61
    exact hcap_cases_37_right
12Establish hcap_cases_36L62–66

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L62
    have hcap_cases_36 : s = 36 ∨ Lt(s,36)Definitions: Lt(s,36)Original native command in the exact edition
  2. L63
    specialize le_eq_or_lt s
  3. L64
    specialize le_eq_or_lt 36
  4. L65
    apply le_eq_or_lt
  5. L66
    exact hcap_le_36
13Separate the logical casesL67–67

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L67
    cases hcap_cases_36
14Establish hcap_36_ceilingL68–73

Establish this local claim before using it. It is not an additional assumption.

  1. L68
    have hcap_36_ceiling : CeilDivSix(36 · 36,e)Definitions: CeilDivSix(36 · 36,e)Original native command in the exact edition
  2. L69
    rewrite <- hcap_cases_36_left
  3. L70
    rewrite <- hcap_cases_36_left
  4. L71
    rewrite <- hcap_cases_36_left
  5. L72
    rewrite <- hcap_cases_36_left
  6. L73
    exact hceiling
15Establish hcap_36_powerL74–81

Establish this local claim before using it. It is not an additional assumption.

  1. L74
    have hcap_36_power : Pow(36 + 1,2 · 36 + 2,h)Definitions: Pow(36 + 1,2 · 36 + 2,h)Original native command in the exact edition
  2. L75
    rewrite <- hcap_cases_36_left
  3. L76
    rewrite <- hcap_cases_36_left
  4. L77
    rewrite <- hcap_cases_36_left
  5. L78
    rewrite <- hcap_cases_36_left
  6. L79
    rewrite <- hcap_cases_36_left
  7. L80
    rewrite <- hcap_cases_36_left
  8. L81
    exact hh
16Establish hcap_36_resultL82–90

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand h root 36 from total.

  1. L82
    have hcap_36_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L83
    specialize bertrand_h_root_36_from_total e
  3. L84
    specialize bertrand_h_root_36_from_total h
  4. L85
    specialize bertrand_h_root_36_from_total u
  5. L86
    apply bertrand_h_root_36_from_total
  6. L87
    exact htotal
  7. L88
    exact hcap_36_ceiling
  8. L89
    exact hcap_36_power
  9. L90
    exact hu
17Separate the logical casesL91–91

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L91
    split
18Use earlier factsL92–93

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L92
    exact hcap_36_result
  2. L93
    exact hjresult
19Establish hcap_le_35L94–98

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L94
    have hcap_le_35 : Le(s,35)Definitions: Le(s,35)Original native command in the exact edition
  2. L95
    specialize le_of_succ_le_succ s
  3. L96
    specialize le_of_succ_le_succ 35
  4. L97
    apply le_of_succ_le_succ
  5. L98
    exact hcap_cases_36_right
20Establish hcap_cases_35L99–103

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L99
    have hcap_cases_35 : s = 35 ∨ Lt(s,35)Definitions: Lt(s,35)Original native command in the exact edition
  2. L100
    specialize le_eq_or_lt s
  3. L101
    specialize le_eq_or_lt 35
  4. L102
    apply le_eq_or_lt
  5. L103
    exact hcap_le_35
21Separate the logical casesL104–104

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L104
    cases hcap_cases_35
22Establish hcap_35_ceilingL105–110

Establish this local claim before using it. It is not an additional assumption.

  1. L105
    have hcap_35_ceiling : CeilDivSix(35 · 35,e)Definitions: CeilDivSix(35 · 35,e)Original native command in the exact edition
  2. L106
    rewrite <- hcap_cases_35_left
  3. L107
    rewrite <- hcap_cases_35_left
  4. L108
    rewrite <- hcap_cases_35_left
  5. L109
    rewrite <- hcap_cases_35_left
  6. L110
    exact hceiling
23Establish hcap_35_powerL111–118

Establish this local claim before using it. It is not an additional assumption.

  1. L111
    have hcap_35_power : Pow(35 + 1,2 · 35 + 2,h)Definitions: Pow(35 + 1,2 · 35 + 2,h)Original native command in the exact edition
  2. L112
    rewrite <- hcap_cases_35_left
  3. L113
    rewrite <- hcap_cases_35_left
  4. L114
    rewrite <- hcap_cases_35_left
  5. L115
    rewrite <- hcap_cases_35_left
  6. L116
    rewrite <- hcap_cases_35_left
  7. L117
    rewrite <- hcap_cases_35_left
  8. L118
    exact hh
24Establish hcap_35_resultL119–127

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand h root 35 from total.

  1. L119
    have hcap_35_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L120
    specialize bertrand_h_root_35_from_total e
  3. L121
    specialize bertrand_h_root_35_from_total h
  4. L122
    specialize bertrand_h_root_35_from_total u
  5. L123
    apply bertrand_h_root_35_from_total
  6. L124
    exact htotal
  7. L125
    exact hcap_35_ceiling
  8. L126
    exact hcap_35_power
  9. L127
    exact hu
25Separate the logical casesL128–128

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L128
    split
26Use earlier factsL129–130

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L129
    exact hcap_35_result
  2. L130
    exact hjresult
27Establish hcap_le_34L131–135

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L131
    have hcap_le_34 : Le(s,34)Definitions: Le(s,34)Original native command in the exact edition
  2. L132
    specialize le_of_succ_le_succ s
  3. L133
    specialize le_of_succ_le_succ 34
  4. L134
    apply le_of_succ_le_succ
  5. L135
    exact hcap_cases_35_right
28Establish hcap_cases_34L136–140

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L136
    have hcap_cases_34 : s = 34 ∨ Lt(s,34)Definitions: Lt(s,34)Original native command in the exact edition
  2. L137
    specialize le_eq_or_lt s
  3. L138
    specialize le_eq_or_lt 34
  4. L139
    apply le_eq_or_lt
  5. L140
    exact hcap_le_34
29Separate the logical casesL141–141

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L141
    cases hcap_cases_34
30Establish hcap_34_ceilingL142–147

Establish this local claim before using it. It is not an additional assumption.

  1. L142
    have hcap_34_ceiling : CeilDivSix(34 · 34,e)Definitions: CeilDivSix(34 · 34,e)Original native command in the exact edition
  2. L143
    rewrite <- hcap_cases_34_left
  3. L144
    rewrite <- hcap_cases_34_left
  4. L145
    rewrite <- hcap_cases_34_left
  5. L146
    rewrite <- hcap_cases_34_left
  6. L147
    exact hceiling
31Establish hcap_34_powerL148–155

Establish this local claim before using it. It is not an additional assumption.

  1. L148
    have hcap_34_power : Pow(34 + 1,2 · 34 + 2,h)Definitions: Pow(34 + 1,2 · 34 + 2,h)Original native command in the exact edition
  2. L149
    rewrite <- hcap_cases_34_left
  3. L150
    rewrite <- hcap_cases_34_left
  4. L151
    rewrite <- hcap_cases_34_left
  5. L152
    rewrite <- hcap_cases_34_left
  6. L153
    rewrite <- hcap_cases_34_left
  7. L154
    rewrite <- hcap_cases_34_left
  8. L155
    exact hh
32Establish hcap_34_resultL156–164

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand h root 34 from total.

  1. L156
    have hcap_34_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L157
    specialize bertrand_h_root_34_from_total e
  3. L158
    specialize bertrand_h_root_34_from_total h
  4. L159
    specialize bertrand_h_root_34_from_total u
  5. L160
    apply bertrand_h_root_34_from_total
  6. L161
    exact htotal
  7. L162
    exact hcap_34_ceiling
  8. L163
    exact hcap_34_power
  9. L164
    exact hu
33Separate the logical casesL165–165

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L165
    split
34Use earlier factsL166–167

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L166
    exact hcap_34_result
  2. L167
    exact hjresult
35Establish hcap_le_33L168–172

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L168
    have hcap_le_33 : Le(s,33)Definitions: Le(s,33)Original native command in the exact edition
  2. L169
    specialize le_of_succ_le_succ s
  3. L170
    specialize le_of_succ_le_succ 33
  4. L171
    apply le_of_succ_le_succ
  5. L172
    exact hcap_cases_34_right
36Establish hcap_cases_33L173–177

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L173
    have hcap_cases_33 : s = 33 ∨ Lt(s,33)Definitions: Lt(s,33)Original native command in the exact edition
  2. L174
    specialize le_eq_or_lt s
  3. L175
    specialize le_eq_or_lt 33
  4. L176
    apply le_eq_or_lt
  5. L177
    exact hcap_le_33
37Separate the logical casesL178–178

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L178
    cases hcap_cases_33
38Establish hcap_33_ceilingL179–184

Establish this local claim before using it. It is not an additional assumption.

  1. L179
    have hcap_33_ceiling : CeilDivSix(33 · 33,e)Definitions: CeilDivSix(33 · 33,e)Original native command in the exact edition
  2. L180
    rewrite <- hcap_cases_33_left
  3. L181
    rewrite <- hcap_cases_33_left
  4. L182
    rewrite <- hcap_cases_33_left
  5. L183
    rewrite <- hcap_cases_33_left
  6. L184
    exact hceiling
39Establish hcap_33_powerL185–192

Establish this local claim before using it. It is not an additional assumption.

  1. L185
    have hcap_33_power : Pow(33 + 1,2 · 33 + 2,h)Definitions: Pow(33 + 1,2 · 33 + 2,h)Original native command in the exact edition
  2. L186
    rewrite <- hcap_cases_33_left
  3. L187
    rewrite <- hcap_cases_33_left
  4. L188
    rewrite <- hcap_cases_33_left
  5. L189
    rewrite <- hcap_cases_33_left
  6. L190
    rewrite <- hcap_cases_33_left
  7. L191
    rewrite <- hcap_cases_33_left
  8. L192
    exact hh
40Establish hcap_33_resultL193–201

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand h root 33 from total.

  1. L193
    have hcap_33_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L194
    specialize bertrand_h_root_33_from_total e
  3. L195
    specialize bertrand_h_root_33_from_total h
  4. L196
    specialize bertrand_h_root_33_from_total u
  5. L197
    apply bertrand_h_root_33_from_total
  6. L198
    exact htotal
  7. L199
    exact hcap_33_ceiling
  8. L200
    exact hcap_33_power
  9. L201
    exact hu
41Separate the logical casesL202–202

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L202
    split
42Use earlier factsL203–204

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L203
    exact hcap_33_result
  2. L204
    exact hjresult
43Establish hcap_le_32L205–209

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L205
    have hcap_le_32 : Le(s,32)Definitions: Le(s,32)Original native command in the exact edition
  2. L206
    specialize le_of_succ_le_succ s
  3. L207
    specialize le_of_succ_le_succ 32
  4. L208
    apply le_of_succ_le_succ
  5. L209
    exact hcap_cases_33_right
44Establish hcap_eq_32L210–215

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le antisymm.

  1. L210
    have hcap_eq_32 : s = 32
  2. L211
    specialize le_antisymm s
  3. L212
    specialize le_antisymm 32
  4. L213
    apply le_antisymm
  5. L214
    exact hcap_le_32
  6. L215
    exact hlower
45Establish hcap_32_ceilingL216–221

Establish this local claim before using it. It is not an additional assumption.

  1. L216
    have hcap_32_ceiling : CeilDivSix(32 · 32,e)Definitions: CeilDivSix(32 · 32,e)Original native command in the exact edition
  2. L217
    rewrite <- hcap_eq_32
  3. L218
    rewrite <- hcap_eq_32
  4. L219
    rewrite <- hcap_eq_32
  5. L220
    rewrite <- hcap_eq_32
  6. L221
    exact hceiling
46Establish hcap_32_powerL222–229

Establish this local claim before using it. It is not an additional assumption.

  1. L222
    have hcap_32_power : Pow(32 + 1,2 · 32 + 2,h)Definitions: Pow(32 + 1,2 · 32 + 2,h)Original native command in the exact edition
  2. L223
    rewrite <- hcap_eq_32
  3. L224
    rewrite <- hcap_eq_32
  4. L225
    rewrite <- hcap_eq_32
  5. L226
    rewrite <- hcap_eq_32
  6. L227
    rewrite <- hcap_eq_32
  7. L228
    rewrite <- hcap_eq_32
  8. L229
    exact hh
47Establish hcap_32_resultL230–238

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand h root 32 from total.

  1. L230
    have hcap_32_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L231
    specialize bertrand_h_root_32_from_total e
  3. L232
    specialize bertrand_h_root_32_from_total h
  4. L233
    specialize bertrand_h_root_32_from_total u
  5. L234
    apply bertrand_h_root_32_from_total
  6. L235
    exact htotal
  7. L236
    exact hcap_32_ceiling
  8. L237
    exact hcap_32_power
  9. L238
    exact hu
48Separate the logical casesL239–239

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L239
    split
49Use earlier factsL240–241

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L240
    exact hcap_32_result
  2. L241
    exact hjresult

Library-wide reading audit

Original defined command ledger · 241 lines
  1. 0001intro s
  2. 0002intro e
  3. 0003intro h
  4. 0004intro u
  5. 0005intro j
  6. 0006intro g
  7. 0007intro htotal
  8. 0008intro hlower
  9. 0009intro hupper
  10. 0010intro hceiling
  11. 0011intro hh
  12. 0012intro hu
  13. 0013intro hj
  14. 0014intro hg
  15. 0015have hjresult : Le(j,g)
    Exact native replay linehave hjresult : exists bqb_le_gap_hj32_capstone_j_result. bqb_le_gap_hj32_capstone_j_result + (j) = (g)
  16. 0016specialize bertrand_j_base_thirty_two_window_from_total s
  17. 0017specialize bertrand_j_base_thirty_two_window_from_total j
  18. 0018specialize bertrand_j_base_thirty_two_window_from_total g
  19. 0019apply bertrand_j_base_thirty_two_window_from_total
  20. 0020exact htotal
  21. 0021exact hlower
  22. 0022exact hupper
  23. 0023exact hj
  24. 0024exact hg
  25. 0025have hcap_cases_37 : s = 37 ∨ Lt(s,37)
    Exact native replay linehave hcap_cases_37 : s = 37 \/ exists bqb_le_gap_hj32_capstone_lt_37. bqb_le_gap_hj32_capstone_lt_37 + (S s) = (37)
  26. 0026specialize le_eq_or_lt s
  27. 0027specialize le_eq_or_lt 37
  28. 0028apply le_eq_or_lt
  29. 0029exact hupper
  30. 0030cases hcap_cases_37
  31. 0031have hcap_37_ceiling : CeilDivSix(37 · 37,e)
    Exact native replay linehave hcap_37_ceiling : ((exists bcs_lower_gap_hj32_capstone_37_ceiling. bcs_lower_gap_hj32_capstone_37_ceiling + (37 * 37) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_37_ceiling. bcs_upper_gap_hj32_capstone_37_ceiling + S (6 * (e)) = (37 * 37) + 6)
  32. 0032rewrite <- hcap_cases_37_left
  33. 0033rewrite <- hcap_cases_37_left
  34. 0034rewrite <- hcap_cases_37_left
  35. 0035rewrite <- hcap_cases_37_left
  36. 0036exact hceiling
  37. 0037have hcap_37_power : Pow(37 + 1,2 · 37 + 2,h)
    Exact native replay linehave hcap_37_power : exists pa_b_hj32_capstone_37_h pa_c_hj32_capstone_37_h. ((forall pa_i_hj32_capstone_37_h_repeat. (exists pa_lt_hj32_capstone_37_h_repeat_bound. pa_lt_hj32_capstone_37_h_repeat_bound + S pa_i_hj32_capstone_37_h_repeat = 2 * 37 + 2) -> (((exists pa_h_hj32_capstone_37_h_repeat_decoded. pa_h_hj32_capstone_37_h_repeat_decoded + S (37 + 1) = S ((S (pa_i_hj32_capstone_37_h_repeat)) * pa_c_hj32_capstone_37_h)) /\ exists pa_q_hj32_capstone_37_h_repeat_decoded. pa_b_hj32_capstone_37_h = pa_q_hj32_capstone_37_h_repeat_decoded * S ((S (pa_i_hj32_capstone_37_h_repeat)) * pa_c_hj32_capstone_37_h) + (37 + 1)))) /\ (exists pa_u_hj32_capstone_37_h_product pa_v_hj32_capstone_37_h_product. ((((exists pa_h_hj32_capstone_37_h_product_start. pa_h_hj32_capstone_37_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_37_h_product)) /\ exists pa_q_hj32_capstone_37_h_product_start. pa_u_hj32_capstone_37_h_product = pa_q_hj32_capstone_37_h_product_start * S ((S (0)) * pa_v_hj32_capstone_37_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_37_h_product_terminal. pa_h_hj32_capstone_37_h_product_terminal + S (h) = S ((S (2 * 37 + 2)) * pa_v_hj32_capstone_37_h_product)) /\ exists pa_q_hj32_capstone_37_h_product_terminal. pa_u_hj32_capstone_37_h_product = pa_q_hj32_capstone_37_h_product_terminal * S ((S (2 * 37 + 2)) * pa_v_hj32_capstone_37_h_product) + (h))) /\ forall pa_i_hj32_capstone_37_h_product. (exists pa_lt_hj32_capstone_37_h_product_bound. pa_lt_hj32_capstone_37_h_product_bound + S pa_i_hj32_capstone_37_h_product = 2 * 37 + 2) -> exists pa_p_hj32_capstone_37_h_product pa_r_hj32_capstone_37_h_product pa_s_hj32_capstone_37_h_product. ((((exists pa_h_hj32_capstone_37_h_product_factor. pa_h_hj32_capstone_37_h_product_factor + S (pa_p_hj32_capstone_37_h_product) = S ((S (pa_i_hj32_capstone_37_h_product)) * pa_c_hj32_capstone_37_h)) /\ exists pa_q_hj32_capstone_37_h_product_factor. pa_b_hj32_capstone_37_h = pa_q_hj32_capstone_37_h_product_factor * S ((S (pa_i_hj32_capstone_37_h_product)) * pa_c_hj32_capstone_37_h) + (pa_p_hj32_capstone_37_h_product))) /\ ((((exists pa_h_hj32_capstone_37_h_product_partial. pa_h_hj32_capstone_37_h_product_partial + S (pa_r_hj32_capstone_37_h_product) = S ((S (pa_i_hj32_capstone_37_h_product)) * pa_v_hj32_capstone_37_h_product)) /\ exists pa_q_hj32_capstone_37_h_product_partial. pa_u_hj32_capstone_37_h_product = pa_q_hj32_capstone_37_h_product_partial * S ((S (pa_i_hj32_capstone_37_h_product)) * pa_v_hj32_capstone_37_h_product) + (pa_r_hj32_capstone_37_h_product))) /\ ((((exists pa_h_hj32_capstone_37_h_product_successor. pa_h_hj32_capstone_37_h_product_successor + S (pa_s_hj32_capstone_37_h_product) = S ((S (S pa_i_hj32_capstone_37_h_product)) * pa_v_hj32_capstone_37_h_product)) /\ exists pa_q_hj32_capstone_37_h_product_successor. pa_u_hj32_capstone_37_h_product = pa_q_hj32_capstone_37_h_product_successor * S ((S (S pa_i_hj32_capstone_37_h_product)) * pa_v_hj32_capstone_37_h_product) + (pa_s_hj32_capstone_37_h_product))) /\ pa_s_hj32_capstone_37_h_product = pa_r_hj32_capstone_37_h_product * pa_p_hj32_capstone_37_h_product)))))))
  38. 0038rewrite <- hcap_cases_37_left
  39. 0039rewrite <- hcap_cases_37_left
  40. 0040rewrite <- hcap_cases_37_left
  41. 0041rewrite <- hcap_cases_37_left
  42. 0042rewrite <- hcap_cases_37_left
  43. 0043rewrite <- hcap_cases_37_left
  44. 0044exact hh
  45. 0045have hcap_37_result : Le(h,u)
    Exact native replay linehave hcap_37_result : exists bqb_le_gap_hj32_capstone_37_result. bqb_le_gap_hj32_capstone_37_result + (h) = (u)
  46. 0046specialize bertrand_h_root_37_from_total e
  47. 0047specialize bertrand_h_root_37_from_total h
  48. 0048specialize bertrand_h_root_37_from_total u
  49. 0049apply bertrand_h_root_37_from_total
  50. 0050exact htotal
  51. 0051exact hcap_37_ceiling
  52. 0052exact hcap_37_power
  53. 0053exact hu
  54. 0054split
  55. 0055exact hcap_37_result
  56. 0056exact hjresult
  57. 0057have hcap_le_36 : Le(s,36)
    Exact native replay linehave hcap_le_36 : exists bqb_le_gap_hj32_capstone_le_36. bqb_le_gap_hj32_capstone_le_36 + (s) = (36)
  58. 0058specialize le_of_succ_le_succ s
  59. 0059specialize le_of_succ_le_succ 36
  60. 0060apply le_of_succ_le_succ
  61. 0061exact hcap_cases_37_right
  62. 0062have hcap_cases_36 : s = 36 ∨ Lt(s,36)
    Exact native replay linehave hcap_cases_36 : s = 36 \/ exists bqb_le_gap_hj32_capstone_lt_36. bqb_le_gap_hj32_capstone_lt_36 + (S s) = (36)
  63. 0063specialize le_eq_or_lt s
  64. 0064specialize le_eq_or_lt 36
  65. 0065apply le_eq_or_lt
  66. 0066exact hcap_le_36
  67. 0067cases hcap_cases_36
  68. 0068have hcap_36_ceiling : CeilDivSix(36 · 36,e)
    Exact native replay linehave hcap_36_ceiling : ((exists bcs_lower_gap_hj32_capstone_36_ceiling. bcs_lower_gap_hj32_capstone_36_ceiling + (36 * 36) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_36_ceiling. bcs_upper_gap_hj32_capstone_36_ceiling + S (6 * (e)) = (36 * 36) + 6)
  69. 0069rewrite <- hcap_cases_36_left
  70. 0070rewrite <- hcap_cases_36_left
  71. 0071rewrite <- hcap_cases_36_left
  72. 0072rewrite <- hcap_cases_36_left
  73. 0073exact hceiling
  74. 0074have hcap_36_power : Pow(36 + 1,2 · 36 + 2,h)
    Exact native replay linehave hcap_36_power : exists pa_b_hj32_capstone_36_h pa_c_hj32_capstone_36_h. ((forall pa_i_hj32_capstone_36_h_repeat. (exists pa_lt_hj32_capstone_36_h_repeat_bound. pa_lt_hj32_capstone_36_h_repeat_bound + S pa_i_hj32_capstone_36_h_repeat = 2 * 36 + 2) -> (((exists pa_h_hj32_capstone_36_h_repeat_decoded. pa_h_hj32_capstone_36_h_repeat_decoded + S (36 + 1) = S ((S (pa_i_hj32_capstone_36_h_repeat)) * pa_c_hj32_capstone_36_h)) /\ exists pa_q_hj32_capstone_36_h_repeat_decoded. pa_b_hj32_capstone_36_h = pa_q_hj32_capstone_36_h_repeat_decoded * S ((S (pa_i_hj32_capstone_36_h_repeat)) * pa_c_hj32_capstone_36_h) + (36 + 1)))) /\ (exists pa_u_hj32_capstone_36_h_product pa_v_hj32_capstone_36_h_product. ((((exists pa_h_hj32_capstone_36_h_product_start. pa_h_hj32_capstone_36_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_36_h_product)) /\ exists pa_q_hj32_capstone_36_h_product_start. pa_u_hj32_capstone_36_h_product = pa_q_hj32_capstone_36_h_product_start * S ((S (0)) * pa_v_hj32_capstone_36_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_36_h_product_terminal. pa_h_hj32_capstone_36_h_product_terminal + S (h) = S ((S (2 * 36 + 2)) * pa_v_hj32_capstone_36_h_product)) /\ exists pa_q_hj32_capstone_36_h_product_terminal. pa_u_hj32_capstone_36_h_product = pa_q_hj32_capstone_36_h_product_terminal * S ((S (2 * 36 + 2)) * pa_v_hj32_capstone_36_h_product) + (h))) /\ forall pa_i_hj32_capstone_36_h_product. (exists pa_lt_hj32_capstone_36_h_product_bound. pa_lt_hj32_capstone_36_h_product_bound + S pa_i_hj32_capstone_36_h_product = 2 * 36 + 2) -> exists pa_p_hj32_capstone_36_h_product pa_r_hj32_capstone_36_h_product pa_s_hj32_capstone_36_h_product. ((((exists pa_h_hj32_capstone_36_h_product_factor. pa_h_hj32_capstone_36_h_product_factor + S (pa_p_hj32_capstone_36_h_product) = S ((S (pa_i_hj32_capstone_36_h_product)) * pa_c_hj32_capstone_36_h)) /\ exists pa_q_hj32_capstone_36_h_product_factor. pa_b_hj32_capstone_36_h = pa_q_hj32_capstone_36_h_product_factor * S ((S (pa_i_hj32_capstone_36_h_product)) * pa_c_hj32_capstone_36_h) + (pa_p_hj32_capstone_36_h_product))) /\ ((((exists pa_h_hj32_capstone_36_h_product_partial. pa_h_hj32_capstone_36_h_product_partial + S (pa_r_hj32_capstone_36_h_product) = S ((S (pa_i_hj32_capstone_36_h_product)) * pa_v_hj32_capstone_36_h_product)) /\ exists pa_q_hj32_capstone_36_h_product_partial. pa_u_hj32_capstone_36_h_product = pa_q_hj32_capstone_36_h_product_partial * S ((S (pa_i_hj32_capstone_36_h_product)) * pa_v_hj32_capstone_36_h_product) + (pa_r_hj32_capstone_36_h_product))) /\ ((((exists pa_h_hj32_capstone_36_h_product_successor. pa_h_hj32_capstone_36_h_product_successor + S (pa_s_hj32_capstone_36_h_product) = S ((S (S pa_i_hj32_capstone_36_h_product)) * pa_v_hj32_capstone_36_h_product)) /\ exists pa_q_hj32_capstone_36_h_product_successor. pa_u_hj32_capstone_36_h_product = pa_q_hj32_capstone_36_h_product_successor * S ((S (S pa_i_hj32_capstone_36_h_product)) * pa_v_hj32_capstone_36_h_product) + (pa_s_hj32_capstone_36_h_product))) /\ pa_s_hj32_capstone_36_h_product = pa_r_hj32_capstone_36_h_product * pa_p_hj32_capstone_36_h_product)))))))
  75. 0075rewrite <- hcap_cases_36_left
  76. 0076rewrite <- hcap_cases_36_left
  77. 0077rewrite <- hcap_cases_36_left
  78. 0078rewrite <- hcap_cases_36_left
  79. 0079rewrite <- hcap_cases_36_left
  80. 0080rewrite <- hcap_cases_36_left
  81. 0081exact hh
  82. 0082have hcap_36_result : Le(h,u)
    Exact native replay linehave hcap_36_result : exists bqb_le_gap_hj32_capstone_36_result. bqb_le_gap_hj32_capstone_36_result + (h) = (u)
  83. 0083specialize bertrand_h_root_36_from_total e
  84. 0084specialize bertrand_h_root_36_from_total h
  85. 0085specialize bertrand_h_root_36_from_total u
  86. 0086apply bertrand_h_root_36_from_total
  87. 0087exact htotal
  88. 0088exact hcap_36_ceiling
  89. 0089exact hcap_36_power
  90. 0090exact hu
  91. 0091split
  92. 0092exact hcap_36_result
  93. 0093exact hjresult
  94. 0094have hcap_le_35 : Le(s,35)
    Exact native replay linehave hcap_le_35 : exists bqb_le_gap_hj32_capstone_le_35. bqb_le_gap_hj32_capstone_le_35 + (s) = (35)
  95. 0095specialize le_of_succ_le_succ s
  96. 0096specialize le_of_succ_le_succ 35
  97. 0097apply le_of_succ_le_succ
  98. 0098exact hcap_cases_36_right
  99. 0099have hcap_cases_35 : s = 35 ∨ Lt(s,35)
    Exact native replay linehave hcap_cases_35 : s = 35 \/ exists bqb_le_gap_hj32_capstone_lt_35. bqb_le_gap_hj32_capstone_lt_35 + (S s) = (35)
  100. 0100specialize le_eq_or_lt s
  101. 0101specialize le_eq_or_lt 35
  102. 0102apply le_eq_or_lt
  103. 0103exact hcap_le_35
  104. 0104cases hcap_cases_35
  105. 0105have hcap_35_ceiling : CeilDivSix(35 · 35,e)
    Exact native replay linehave hcap_35_ceiling : ((exists bcs_lower_gap_hj32_capstone_35_ceiling. bcs_lower_gap_hj32_capstone_35_ceiling + (35 * 35) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_35_ceiling. bcs_upper_gap_hj32_capstone_35_ceiling + S (6 * (e)) = (35 * 35) + 6)
  106. 0106rewrite <- hcap_cases_35_left
  107. 0107rewrite <- hcap_cases_35_left
  108. 0108rewrite <- hcap_cases_35_left
  109. 0109rewrite <- hcap_cases_35_left
  110. 0110exact hceiling
  111. 0111have hcap_35_power : Pow(35 + 1,2 · 35 + 2,h)
    Exact native replay linehave hcap_35_power : exists pa_b_hj32_capstone_35_h pa_c_hj32_capstone_35_h. ((forall pa_i_hj32_capstone_35_h_repeat. (exists pa_lt_hj32_capstone_35_h_repeat_bound. pa_lt_hj32_capstone_35_h_repeat_bound + S pa_i_hj32_capstone_35_h_repeat = 2 * 35 + 2) -> (((exists pa_h_hj32_capstone_35_h_repeat_decoded. pa_h_hj32_capstone_35_h_repeat_decoded + S (35 + 1) = S ((S (pa_i_hj32_capstone_35_h_repeat)) * pa_c_hj32_capstone_35_h)) /\ exists pa_q_hj32_capstone_35_h_repeat_decoded. pa_b_hj32_capstone_35_h = pa_q_hj32_capstone_35_h_repeat_decoded * S ((S (pa_i_hj32_capstone_35_h_repeat)) * pa_c_hj32_capstone_35_h) + (35 + 1)))) /\ (exists pa_u_hj32_capstone_35_h_product pa_v_hj32_capstone_35_h_product. ((((exists pa_h_hj32_capstone_35_h_product_start. pa_h_hj32_capstone_35_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_35_h_product)) /\ exists pa_q_hj32_capstone_35_h_product_start. pa_u_hj32_capstone_35_h_product = pa_q_hj32_capstone_35_h_product_start * S ((S (0)) * pa_v_hj32_capstone_35_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_35_h_product_terminal. pa_h_hj32_capstone_35_h_product_terminal + S (h) = S ((S (2 * 35 + 2)) * pa_v_hj32_capstone_35_h_product)) /\ exists pa_q_hj32_capstone_35_h_product_terminal. pa_u_hj32_capstone_35_h_product = pa_q_hj32_capstone_35_h_product_terminal * S ((S (2 * 35 + 2)) * pa_v_hj32_capstone_35_h_product) + (h))) /\ forall pa_i_hj32_capstone_35_h_product. (exists pa_lt_hj32_capstone_35_h_product_bound. pa_lt_hj32_capstone_35_h_product_bound + S pa_i_hj32_capstone_35_h_product = 2 * 35 + 2) -> exists pa_p_hj32_capstone_35_h_product pa_r_hj32_capstone_35_h_product pa_s_hj32_capstone_35_h_product. ((((exists pa_h_hj32_capstone_35_h_product_factor. pa_h_hj32_capstone_35_h_product_factor + S (pa_p_hj32_capstone_35_h_product) = S ((S (pa_i_hj32_capstone_35_h_product)) * pa_c_hj32_capstone_35_h)) /\ exists pa_q_hj32_capstone_35_h_product_factor. pa_b_hj32_capstone_35_h = pa_q_hj32_capstone_35_h_product_factor * S ((S (pa_i_hj32_capstone_35_h_product)) * pa_c_hj32_capstone_35_h) + (pa_p_hj32_capstone_35_h_product))) /\ ((((exists pa_h_hj32_capstone_35_h_product_partial. pa_h_hj32_capstone_35_h_product_partial + S (pa_r_hj32_capstone_35_h_product) = S ((S (pa_i_hj32_capstone_35_h_product)) * pa_v_hj32_capstone_35_h_product)) /\ exists pa_q_hj32_capstone_35_h_product_partial. pa_u_hj32_capstone_35_h_product = pa_q_hj32_capstone_35_h_product_partial * S ((S (pa_i_hj32_capstone_35_h_product)) * pa_v_hj32_capstone_35_h_product) + (pa_r_hj32_capstone_35_h_product))) /\ ((((exists pa_h_hj32_capstone_35_h_product_successor. pa_h_hj32_capstone_35_h_product_successor + S (pa_s_hj32_capstone_35_h_product) = S ((S (S pa_i_hj32_capstone_35_h_product)) * pa_v_hj32_capstone_35_h_product)) /\ exists pa_q_hj32_capstone_35_h_product_successor. pa_u_hj32_capstone_35_h_product = pa_q_hj32_capstone_35_h_product_successor * S ((S (S pa_i_hj32_capstone_35_h_product)) * pa_v_hj32_capstone_35_h_product) + (pa_s_hj32_capstone_35_h_product))) /\ pa_s_hj32_capstone_35_h_product = pa_r_hj32_capstone_35_h_product * pa_p_hj32_capstone_35_h_product)))))))
  112. 0112rewrite <- hcap_cases_35_left
  113. 0113rewrite <- hcap_cases_35_left
  114. 0114rewrite <- hcap_cases_35_left
  115. 0115rewrite <- hcap_cases_35_left
  116. 0116rewrite <- hcap_cases_35_left
  117. 0117rewrite <- hcap_cases_35_left
  118. 0118exact hh
  119. 0119have hcap_35_result : Le(h,u)
    Exact native replay linehave hcap_35_result : exists bqb_le_gap_hj32_capstone_35_result. bqb_le_gap_hj32_capstone_35_result + (h) = (u)
  120. 0120specialize bertrand_h_root_35_from_total e
  121. 0121specialize bertrand_h_root_35_from_total h
  122. 0122specialize bertrand_h_root_35_from_total u
  123. 0123apply bertrand_h_root_35_from_total
  124. 0124exact htotal
  125. 0125exact hcap_35_ceiling
  126. 0126exact hcap_35_power
  127. 0127exact hu
  128. 0128split
  129. 0129exact hcap_35_result
  130. 0130exact hjresult
  131. 0131have hcap_le_34 : Le(s,34)
    Exact native replay linehave hcap_le_34 : exists bqb_le_gap_hj32_capstone_le_34. bqb_le_gap_hj32_capstone_le_34 + (s) = (34)
  132. 0132specialize le_of_succ_le_succ s
  133. 0133specialize le_of_succ_le_succ 34
  134. 0134apply le_of_succ_le_succ
  135. 0135exact hcap_cases_35_right
  136. 0136have hcap_cases_34 : s = 34 ∨ Lt(s,34)
    Exact native replay linehave hcap_cases_34 : s = 34 \/ exists bqb_le_gap_hj32_capstone_lt_34. bqb_le_gap_hj32_capstone_lt_34 + (S s) = (34)
  137. 0137specialize le_eq_or_lt s
  138. 0138specialize le_eq_or_lt 34
  139. 0139apply le_eq_or_lt
  140. 0140exact hcap_le_34
  141. 0141cases hcap_cases_34
  142. 0142have hcap_34_ceiling : CeilDivSix(34 · 34,e)
    Exact native replay linehave hcap_34_ceiling : ((exists bcs_lower_gap_hj32_capstone_34_ceiling. bcs_lower_gap_hj32_capstone_34_ceiling + (34 * 34) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_34_ceiling. bcs_upper_gap_hj32_capstone_34_ceiling + S (6 * (e)) = (34 * 34) + 6)
  143. 0143rewrite <- hcap_cases_34_left
  144. 0144rewrite <- hcap_cases_34_left
  145. 0145rewrite <- hcap_cases_34_left
  146. 0146rewrite <- hcap_cases_34_left
  147. 0147exact hceiling
  148. 0148have hcap_34_power : Pow(34 + 1,2 · 34 + 2,h)
    Exact native replay linehave hcap_34_power : exists pa_b_hj32_capstone_34_h pa_c_hj32_capstone_34_h. ((forall pa_i_hj32_capstone_34_h_repeat. (exists pa_lt_hj32_capstone_34_h_repeat_bound. pa_lt_hj32_capstone_34_h_repeat_bound + S pa_i_hj32_capstone_34_h_repeat = 2 * 34 + 2) -> (((exists pa_h_hj32_capstone_34_h_repeat_decoded. pa_h_hj32_capstone_34_h_repeat_decoded + S (34 + 1) = S ((S (pa_i_hj32_capstone_34_h_repeat)) * pa_c_hj32_capstone_34_h)) /\ exists pa_q_hj32_capstone_34_h_repeat_decoded. pa_b_hj32_capstone_34_h = pa_q_hj32_capstone_34_h_repeat_decoded * S ((S (pa_i_hj32_capstone_34_h_repeat)) * pa_c_hj32_capstone_34_h) + (34 + 1)))) /\ (exists pa_u_hj32_capstone_34_h_product pa_v_hj32_capstone_34_h_product. ((((exists pa_h_hj32_capstone_34_h_product_start. pa_h_hj32_capstone_34_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_34_h_product)) /\ exists pa_q_hj32_capstone_34_h_product_start. pa_u_hj32_capstone_34_h_product = pa_q_hj32_capstone_34_h_product_start * S ((S (0)) * pa_v_hj32_capstone_34_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_34_h_product_terminal. pa_h_hj32_capstone_34_h_product_terminal + S (h) = S ((S (2 * 34 + 2)) * pa_v_hj32_capstone_34_h_product)) /\ exists pa_q_hj32_capstone_34_h_product_terminal. pa_u_hj32_capstone_34_h_product = pa_q_hj32_capstone_34_h_product_terminal * S ((S (2 * 34 + 2)) * pa_v_hj32_capstone_34_h_product) + (h))) /\ forall pa_i_hj32_capstone_34_h_product. (exists pa_lt_hj32_capstone_34_h_product_bound. pa_lt_hj32_capstone_34_h_product_bound + S pa_i_hj32_capstone_34_h_product = 2 * 34 + 2) -> exists pa_p_hj32_capstone_34_h_product pa_r_hj32_capstone_34_h_product pa_s_hj32_capstone_34_h_product. ((((exists pa_h_hj32_capstone_34_h_product_factor. pa_h_hj32_capstone_34_h_product_factor + S (pa_p_hj32_capstone_34_h_product) = S ((S (pa_i_hj32_capstone_34_h_product)) * pa_c_hj32_capstone_34_h)) /\ exists pa_q_hj32_capstone_34_h_product_factor. pa_b_hj32_capstone_34_h = pa_q_hj32_capstone_34_h_product_factor * S ((S (pa_i_hj32_capstone_34_h_product)) * pa_c_hj32_capstone_34_h) + (pa_p_hj32_capstone_34_h_product))) /\ ((((exists pa_h_hj32_capstone_34_h_product_partial. pa_h_hj32_capstone_34_h_product_partial + S (pa_r_hj32_capstone_34_h_product) = S ((S (pa_i_hj32_capstone_34_h_product)) * pa_v_hj32_capstone_34_h_product)) /\ exists pa_q_hj32_capstone_34_h_product_partial. pa_u_hj32_capstone_34_h_product = pa_q_hj32_capstone_34_h_product_partial * S ((S (pa_i_hj32_capstone_34_h_product)) * pa_v_hj32_capstone_34_h_product) + (pa_r_hj32_capstone_34_h_product))) /\ ((((exists pa_h_hj32_capstone_34_h_product_successor. pa_h_hj32_capstone_34_h_product_successor + S (pa_s_hj32_capstone_34_h_product) = S ((S (S pa_i_hj32_capstone_34_h_product)) * pa_v_hj32_capstone_34_h_product)) /\ exists pa_q_hj32_capstone_34_h_product_successor. pa_u_hj32_capstone_34_h_product = pa_q_hj32_capstone_34_h_product_successor * S ((S (S pa_i_hj32_capstone_34_h_product)) * pa_v_hj32_capstone_34_h_product) + (pa_s_hj32_capstone_34_h_product))) /\ pa_s_hj32_capstone_34_h_product = pa_r_hj32_capstone_34_h_product * pa_p_hj32_capstone_34_h_product)))))))
  149. 0149rewrite <- hcap_cases_34_left
  150. 0150rewrite <- hcap_cases_34_left
  151. 0151rewrite <- hcap_cases_34_left
  152. 0152rewrite <- hcap_cases_34_left
  153. 0153rewrite <- hcap_cases_34_left
  154. 0154rewrite <- hcap_cases_34_left
  155. 0155exact hh
  156. 0156have hcap_34_result : Le(h,u)
    Exact native replay linehave hcap_34_result : exists bqb_le_gap_hj32_capstone_34_result. bqb_le_gap_hj32_capstone_34_result + (h) = (u)
  157. 0157specialize bertrand_h_root_34_from_total e
  158. 0158specialize bertrand_h_root_34_from_total h
  159. 0159specialize bertrand_h_root_34_from_total u
  160. 0160apply bertrand_h_root_34_from_total
  161. 0161exact htotal
  162. 0162exact hcap_34_ceiling
  163. 0163exact hcap_34_power
  164. 0164exact hu
  165. 0165split
  166. 0166exact hcap_34_result
  167. 0167exact hjresult
  168. 0168have hcap_le_33 : Le(s,33)
    Exact native replay linehave hcap_le_33 : exists bqb_le_gap_hj32_capstone_le_33. bqb_le_gap_hj32_capstone_le_33 + (s) = (33)
  169. 0169specialize le_of_succ_le_succ s
  170. 0170specialize le_of_succ_le_succ 33
  171. 0171apply le_of_succ_le_succ
  172. 0172exact hcap_cases_34_right
  173. 0173have hcap_cases_33 : s = 33 ∨ Lt(s,33)
    Exact native replay linehave hcap_cases_33 : s = 33 \/ exists bqb_le_gap_hj32_capstone_lt_33. bqb_le_gap_hj32_capstone_lt_33 + (S s) = (33)
  174. 0174specialize le_eq_or_lt s
  175. 0175specialize le_eq_or_lt 33
  176. 0176apply le_eq_or_lt
  177. 0177exact hcap_le_33
  178. 0178cases hcap_cases_33
  179. 0179have hcap_33_ceiling : CeilDivSix(33 · 33,e)
    Exact native replay linehave hcap_33_ceiling : ((exists bcs_lower_gap_hj32_capstone_33_ceiling. bcs_lower_gap_hj32_capstone_33_ceiling + (33 * 33) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_33_ceiling. bcs_upper_gap_hj32_capstone_33_ceiling + S (6 * (e)) = (33 * 33) + 6)
  180. 0180rewrite <- hcap_cases_33_left
  181. 0181rewrite <- hcap_cases_33_left
  182. 0182rewrite <- hcap_cases_33_left
  183. 0183rewrite <- hcap_cases_33_left
  184. 0184exact hceiling
  185. 0185have hcap_33_power : Pow(33 + 1,2 · 33 + 2,h)
    Exact native replay linehave hcap_33_power : exists pa_b_hj32_capstone_33_h pa_c_hj32_capstone_33_h. ((forall pa_i_hj32_capstone_33_h_repeat. (exists pa_lt_hj32_capstone_33_h_repeat_bound. pa_lt_hj32_capstone_33_h_repeat_bound + S pa_i_hj32_capstone_33_h_repeat = 2 * 33 + 2) -> (((exists pa_h_hj32_capstone_33_h_repeat_decoded. pa_h_hj32_capstone_33_h_repeat_decoded + S (33 + 1) = S ((S (pa_i_hj32_capstone_33_h_repeat)) * pa_c_hj32_capstone_33_h)) /\ exists pa_q_hj32_capstone_33_h_repeat_decoded. pa_b_hj32_capstone_33_h = pa_q_hj32_capstone_33_h_repeat_decoded * S ((S (pa_i_hj32_capstone_33_h_repeat)) * pa_c_hj32_capstone_33_h) + (33 + 1)))) /\ (exists pa_u_hj32_capstone_33_h_product pa_v_hj32_capstone_33_h_product. ((((exists pa_h_hj32_capstone_33_h_product_start. pa_h_hj32_capstone_33_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_33_h_product)) /\ exists pa_q_hj32_capstone_33_h_product_start. pa_u_hj32_capstone_33_h_product = pa_q_hj32_capstone_33_h_product_start * S ((S (0)) * pa_v_hj32_capstone_33_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_33_h_product_terminal. pa_h_hj32_capstone_33_h_product_terminal + S (h) = S ((S (2 * 33 + 2)) * pa_v_hj32_capstone_33_h_product)) /\ exists pa_q_hj32_capstone_33_h_product_terminal. pa_u_hj32_capstone_33_h_product = pa_q_hj32_capstone_33_h_product_terminal * S ((S (2 * 33 + 2)) * pa_v_hj32_capstone_33_h_product) + (h))) /\ forall pa_i_hj32_capstone_33_h_product. (exists pa_lt_hj32_capstone_33_h_product_bound. pa_lt_hj32_capstone_33_h_product_bound + S pa_i_hj32_capstone_33_h_product = 2 * 33 + 2) -> exists pa_p_hj32_capstone_33_h_product pa_r_hj32_capstone_33_h_product pa_s_hj32_capstone_33_h_product. ((((exists pa_h_hj32_capstone_33_h_product_factor. pa_h_hj32_capstone_33_h_product_factor + S (pa_p_hj32_capstone_33_h_product) = S ((S (pa_i_hj32_capstone_33_h_product)) * pa_c_hj32_capstone_33_h)) /\ exists pa_q_hj32_capstone_33_h_product_factor. pa_b_hj32_capstone_33_h = pa_q_hj32_capstone_33_h_product_factor * S ((S (pa_i_hj32_capstone_33_h_product)) * pa_c_hj32_capstone_33_h) + (pa_p_hj32_capstone_33_h_product))) /\ ((((exists pa_h_hj32_capstone_33_h_product_partial. pa_h_hj32_capstone_33_h_product_partial + S (pa_r_hj32_capstone_33_h_product) = S ((S (pa_i_hj32_capstone_33_h_product)) * pa_v_hj32_capstone_33_h_product)) /\ exists pa_q_hj32_capstone_33_h_product_partial. pa_u_hj32_capstone_33_h_product = pa_q_hj32_capstone_33_h_product_partial * S ((S (pa_i_hj32_capstone_33_h_product)) * pa_v_hj32_capstone_33_h_product) + (pa_r_hj32_capstone_33_h_product))) /\ ((((exists pa_h_hj32_capstone_33_h_product_successor. pa_h_hj32_capstone_33_h_product_successor + S (pa_s_hj32_capstone_33_h_product) = S ((S (S pa_i_hj32_capstone_33_h_product)) * pa_v_hj32_capstone_33_h_product)) /\ exists pa_q_hj32_capstone_33_h_product_successor. pa_u_hj32_capstone_33_h_product = pa_q_hj32_capstone_33_h_product_successor * S ((S (S pa_i_hj32_capstone_33_h_product)) * pa_v_hj32_capstone_33_h_product) + (pa_s_hj32_capstone_33_h_product))) /\ pa_s_hj32_capstone_33_h_product = pa_r_hj32_capstone_33_h_product * pa_p_hj32_capstone_33_h_product)))))))
  186. 0186rewrite <- hcap_cases_33_left
  187. 0187rewrite <- hcap_cases_33_left
  188. 0188rewrite <- hcap_cases_33_left
  189. 0189rewrite <- hcap_cases_33_left
  190. 0190rewrite <- hcap_cases_33_left
  191. 0191rewrite <- hcap_cases_33_left
  192. 0192exact hh
  193. 0193have hcap_33_result : Le(h,u)
    Exact native replay linehave hcap_33_result : exists bqb_le_gap_hj32_capstone_33_result. bqb_le_gap_hj32_capstone_33_result + (h) = (u)
  194. 0194specialize bertrand_h_root_33_from_total e
  195. 0195specialize bertrand_h_root_33_from_total h
  196. 0196specialize bertrand_h_root_33_from_total u
  197. 0197apply bertrand_h_root_33_from_total
  198. 0198exact htotal
  199. 0199exact hcap_33_ceiling
  200. 0200exact hcap_33_power
  201. 0201exact hu
  202. 0202split
  203. 0203exact hcap_33_result
  204. 0204exact hjresult
  205. 0205have hcap_le_32 : Le(s,32)
    Exact native replay linehave hcap_le_32 : exists bqb_le_gap_hj32_capstone_le_32. bqb_le_gap_hj32_capstone_le_32 + (s) = (32)
  206. 0206specialize le_of_succ_le_succ s
  207. 0207specialize le_of_succ_le_succ 32
  208. 0208apply le_of_succ_le_succ
  209. 0209exact hcap_cases_33_right
  210. 0210have hcap_eq_32 : s = 32
  211. 0211specialize le_antisymm s
  212. 0212specialize le_antisymm 32
  213. 0213apply le_antisymm
  214. 0214exact hcap_le_32
  215. 0215exact hlower
  216. 0216have hcap_32_ceiling : CeilDivSix(32 · 32,e)
    Exact native replay linehave hcap_32_ceiling : ((exists bcs_lower_gap_hj32_capstone_32_ceiling. bcs_lower_gap_hj32_capstone_32_ceiling + (32 * 32) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_32_ceiling. bcs_upper_gap_hj32_capstone_32_ceiling + S (6 * (e)) = (32 * 32) + 6)
  217. 0217rewrite <- hcap_eq_32
  218. 0218rewrite <- hcap_eq_32
  219. 0219rewrite <- hcap_eq_32
  220. 0220rewrite <- hcap_eq_32
  221. 0221exact hceiling
  222. 0222have hcap_32_power : Pow(32 + 1,2 · 32 + 2,h)
    Exact native replay linehave hcap_32_power : exists pa_b_hj32_capstone_32_h pa_c_hj32_capstone_32_h. ((forall pa_i_hj32_capstone_32_h_repeat. (exists pa_lt_hj32_capstone_32_h_repeat_bound. pa_lt_hj32_capstone_32_h_repeat_bound + S pa_i_hj32_capstone_32_h_repeat = 2 * 32 + 2) -> (((exists pa_h_hj32_capstone_32_h_repeat_decoded. pa_h_hj32_capstone_32_h_repeat_decoded + S (32 + 1) = S ((S (pa_i_hj32_capstone_32_h_repeat)) * pa_c_hj32_capstone_32_h)) /\ exists pa_q_hj32_capstone_32_h_repeat_decoded. pa_b_hj32_capstone_32_h = pa_q_hj32_capstone_32_h_repeat_decoded * S ((S (pa_i_hj32_capstone_32_h_repeat)) * pa_c_hj32_capstone_32_h) + (32 + 1)))) /\ (exists pa_u_hj32_capstone_32_h_product pa_v_hj32_capstone_32_h_product. ((((exists pa_h_hj32_capstone_32_h_product_start. pa_h_hj32_capstone_32_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_32_h_product)) /\ exists pa_q_hj32_capstone_32_h_product_start. pa_u_hj32_capstone_32_h_product = pa_q_hj32_capstone_32_h_product_start * S ((S (0)) * pa_v_hj32_capstone_32_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_32_h_product_terminal. pa_h_hj32_capstone_32_h_product_terminal + S (h) = S ((S (2 * 32 + 2)) * pa_v_hj32_capstone_32_h_product)) /\ exists pa_q_hj32_capstone_32_h_product_terminal. pa_u_hj32_capstone_32_h_product = pa_q_hj32_capstone_32_h_product_terminal * S ((S (2 * 32 + 2)) * pa_v_hj32_capstone_32_h_product) + (h))) /\ forall pa_i_hj32_capstone_32_h_product. (exists pa_lt_hj32_capstone_32_h_product_bound. pa_lt_hj32_capstone_32_h_product_bound + S pa_i_hj32_capstone_32_h_product = 2 * 32 + 2) -> exists pa_p_hj32_capstone_32_h_product pa_r_hj32_capstone_32_h_product pa_s_hj32_capstone_32_h_product. ((((exists pa_h_hj32_capstone_32_h_product_factor. pa_h_hj32_capstone_32_h_product_factor + S (pa_p_hj32_capstone_32_h_product) = S ((S (pa_i_hj32_capstone_32_h_product)) * pa_c_hj32_capstone_32_h)) /\ exists pa_q_hj32_capstone_32_h_product_factor. pa_b_hj32_capstone_32_h = pa_q_hj32_capstone_32_h_product_factor * S ((S (pa_i_hj32_capstone_32_h_product)) * pa_c_hj32_capstone_32_h) + (pa_p_hj32_capstone_32_h_product))) /\ ((((exists pa_h_hj32_capstone_32_h_product_partial. pa_h_hj32_capstone_32_h_product_partial + S (pa_r_hj32_capstone_32_h_product) = S ((S (pa_i_hj32_capstone_32_h_product)) * pa_v_hj32_capstone_32_h_product)) /\ exists pa_q_hj32_capstone_32_h_product_partial. pa_u_hj32_capstone_32_h_product = pa_q_hj32_capstone_32_h_product_partial * S ((S (pa_i_hj32_capstone_32_h_product)) * pa_v_hj32_capstone_32_h_product) + (pa_r_hj32_capstone_32_h_product))) /\ ((((exists pa_h_hj32_capstone_32_h_product_successor. pa_h_hj32_capstone_32_h_product_successor + S (pa_s_hj32_capstone_32_h_product) = S ((S (S pa_i_hj32_capstone_32_h_product)) * pa_v_hj32_capstone_32_h_product)) /\ exists pa_q_hj32_capstone_32_h_product_successor. pa_u_hj32_capstone_32_h_product = pa_q_hj32_capstone_32_h_product_successor * S ((S (S pa_i_hj32_capstone_32_h_product)) * pa_v_hj32_capstone_32_h_product) + (pa_s_hj32_capstone_32_h_product))) /\ pa_s_hj32_capstone_32_h_product = pa_r_hj32_capstone_32_h_product * pa_p_hj32_capstone_32_h_product)))))))
  223. 0223rewrite <- hcap_eq_32
  224. 0224rewrite <- hcap_eq_32
  225. 0225rewrite <- hcap_eq_32
  226. 0226rewrite <- hcap_eq_32
  227. 0227rewrite <- hcap_eq_32
  228. 0228rewrite <- hcap_eq_32
  229. 0229exact hh
  230. 0230have hcap_32_result : Le(h,u)
    Exact native replay linehave hcap_32_result : exists bqb_le_gap_hj32_capstone_32_result. bqb_le_gap_hj32_capstone_32_result + (h) = (u)
  231. 0231specialize bertrand_h_root_32_from_total e
  232. 0232specialize bertrand_h_root_32_from_total h
  233. 0233specialize bertrand_h_root_32_from_total u
  234. 0234apply bertrand_h_root_32_from_total
  235. 0235exact htotal
  236. 0236exact hcap_32_ceiling
  237. 0237exact hcap_32_power
  238. 0238exact hu
  239. 0239split
  240. 0240exact hcap_32_result
  241. 0241exact hjresult