BT00X2 · Bertrand theorem

bertrand_hj_six_block_iterate_from_total

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

The common H/J invariant iterates constructively over every six-step block.

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

∀ b. (∀ x. ∀ y. ∃ z. Pow(x,y,z)) → Lt(31,b) → Le(b,37) → ∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. CeilDivSix((b + 6 · x) · (b + 6 · x),y) → Pow(b + 6 · x + 1,2 · (b + 6 · x) + 2,z) → Pow(4,y,n) → Pow(b + 6 · x + 7,12,m) → Pow(4,b + 6 · x + 5,k) → Le(z,n) ∧ Le(m,k)

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

17 occurrences

Exact expanded native-PA statement
forall b. (forall bpt_a_hjas_iterator bpt_e_hjas_iterator. exists bpt_x_hjas_iterator. (exists ff_b_bpt_value_hjas_iterator ff_c_bpt_value_hjas_iterator. ((forall ff_i_bpt_value_hjas_iterator_repeat. (exists ff_lt_bpt_value_hjas_iterator_repeat_bound. ff_lt_bpt_value_hjas_iterator_repeat_bound + S ff_i_bpt_value_hjas_iterator_repeat = bpt_e_hjas_iterator) -> (((exists ff_h_bpt_value_hjas_iterator_repeat_decoded. ff_h_bpt_value_hjas_iterator_repeat_decoded + S (bpt_a_hjas_iterator) = S ((S (ff_i_bpt_value_hjas_iterator_repeat)) * ff_c_bpt_value_hjas_iterator)) /\ exists ff_q_bpt_value_hjas_iterator_repeat_decoded. ff_b_bpt_value_hjas_iterator = ff_q_bpt_value_hjas_iterator_repeat_decoded * S ((S (ff_i_bpt_value_hjas_iterator_repeat)) * ff_c_bpt_value_hjas_iterator) + (bpt_a_hjas_iterator)))) /\ (exists ff_u_bpt_value_hjas_iterator_product ff_v_bpt_value_hjas_iterator_product. ((((exists ff_h_bpt_value_hjas_iterator_product_start. ff_h_bpt_value_hjas_iterator_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hjas_iterator_product)) /\ exists ff_q_bpt_value_hjas_iterator_product_start. ff_u_bpt_value_hjas_iterator_product = ff_q_bpt_value_hjas_iterator_product_start * S ((S (0)) * ff_v_bpt_value_hjas_iterator_product) + (1))) /\ ((((exists ff_h_bpt_value_hjas_iterator_product_terminal. ff_h_bpt_value_hjas_iterator_product_terminal + S (bpt_x_hjas_iterator) = S ((S (bpt_e_hjas_iterator)) * ff_v_bpt_value_hjas_iterator_product)) /\ exists ff_q_bpt_value_hjas_iterator_product_terminal. ff_u_bpt_value_hjas_iterator_product = ff_q_bpt_value_hjas_iterator_product_terminal * S ((S (bpt_e_hjas_iterator)) * ff_v_bpt_value_hjas_iterator_product) + (bpt_x_hjas_iterator))) /\ forall ff_i_bpt_value_hjas_iterator_product. (exists ff_lt_bpt_value_hjas_iterator_product_bound. ff_lt_bpt_value_hjas_iterator_product_bound + S ff_i_bpt_value_hjas_iterator_product = bpt_e_hjas_iterator) -> exists ff_p_bpt_value_hjas_iterator_product ff_r_bpt_value_hjas_iterator_product ff_s_bpt_value_hjas_iterator_product. ((((exists ff_h_bpt_value_hjas_iterator_product_factor. ff_h_bpt_value_hjas_iterator_product_factor + S (ff_p_bpt_value_hjas_iterator_product) = S ((S (ff_i_bpt_value_hjas_iterator_product)) * ff_c_bpt_value_hjas_iterator)) /\ exists ff_q_bpt_value_hjas_iterator_product_factor. ff_b_bpt_value_hjas_iterator = ff_q_bpt_value_hjas_iterator_product_factor * S ((S (ff_i_bpt_value_hjas_iterator_product)) * ff_c_bpt_value_hjas_iterator) + (ff_p_bpt_value_hjas_iterator_product))) /\ ((((exists ff_h_bpt_value_hjas_iterator_product_partial. ff_h_bpt_value_hjas_iterator_product_partial + S (ff_r_bpt_value_hjas_iterator_product) = S ((S (ff_i_bpt_value_hjas_iterator_product)) * ff_v_bpt_value_hjas_iterator_product)) /\ exists ff_q_bpt_value_hjas_iterator_product_partial. ff_u_bpt_value_hjas_iterator_product = ff_q_bpt_value_hjas_iterator_product_partial * S ((S (ff_i_bpt_value_hjas_iterator_product)) * ff_v_bpt_value_hjas_iterator_product) + (ff_r_bpt_value_hjas_iterator_product))) /\ ((((exists ff_h_bpt_value_hjas_iterator_product_successor. ff_h_bpt_value_hjas_iterator_product_successor + S (ff_s_bpt_value_hjas_iterator_product) = S ((S (S ff_i_bpt_value_hjas_iterator_product)) * ff_v_bpt_value_hjas_iterator_product)) /\ exists ff_q_bpt_value_hjas_iterator_product_successor. ff_u_bpt_value_hjas_iterator_product = ff_q_bpt_value_hjas_iterator_product_successor * S ((S (S ff_i_bpt_value_hjas_iterator_product)) * ff_v_bpt_value_hjas_iterator_product) + (ff_s_bpt_value_hjas_iterator_product))) /\ ff_s_bpt_value_hjas_iterator_product = ff_r_bpt_value_hjas_iterator_product * ff_p_bpt_value_hjas_iterator_product))))))))) -> (exists bqb_le_gap_hjas_iterator_base_lower. bqb_le_gap_hjas_iterator_base_lower + (32) = (b)) -> (exists bqb_le_gap_hjas_iterator_base_upper. bqb_le_gap_hjas_iterator_base_upper + (b) = (37)) -> forall k e h u j g. (((exists bcs_lower_gap_hjas_iterator_ceiling. bcs_lower_gap_hjas_iterator_ceiling + ((b + 6 * k) * (b + 6 * k)) = 6 * (e)) /\ exists bcs_upper_gap_hjas_iterator_ceiling. bcs_upper_gap_hjas_iterator_ceiling + S (6 * (e)) = ((b + 6 * k) * (b + 6 * k)) + 6)) -> (exists pa_b_hjas_iterator_h pa_c_hjas_iterator_h. ((forall pa_i_hjas_iterator_h_repeat. (exists pa_lt_hjas_iterator_h_repeat_bound. pa_lt_hjas_iterator_h_repeat_bound + S pa_i_hjas_iterator_h_repeat = 2 * (b + 6 * k) + 2) -> (((exists pa_h_hjas_iterator_h_repeat_decoded. pa_h_hjas_iterator_h_repeat_decoded + S ((b + 6 * k) + 1) = S ((S (pa_i_hjas_iterator_h_repeat)) * pa_c_hjas_iterator_h)) /\ exists pa_q_hjas_iterator_h_repeat_decoded. pa_b_hjas_iterator_h = pa_q_hjas_iterator_h_repeat_decoded * S ((S (pa_i_hjas_iterator_h_repeat)) * pa_c_hjas_iterator_h) + ((b + 6 * k) + 1)))) /\ (exists pa_u_hjas_iterator_h_product pa_v_hjas_iterator_h_product. ((((exists pa_h_hjas_iterator_h_product_start. pa_h_hjas_iterator_h_product_start + S (1) = S ((S (0)) * pa_v_hjas_iterator_h_product)) /\ exists pa_q_hjas_iterator_h_product_start. pa_u_hjas_iterator_h_product = pa_q_hjas_iterator_h_product_start * S ((S (0)) * pa_v_hjas_iterator_h_product) + (1))) /\ ((((exists pa_h_hjas_iterator_h_product_terminal. pa_h_hjas_iterator_h_product_terminal + S (h) = S ((S (2 * (b + 6 * k) + 2)) * pa_v_hjas_iterator_h_product)) /\ exists pa_q_hjas_iterator_h_product_terminal. pa_u_hjas_iterator_h_product = pa_q_hjas_iterator_h_product_terminal * S ((S (2 * (b + 6 * k) + 2)) * pa_v_hjas_iterator_h_product) + (h))) /\ forall pa_i_hjas_iterator_h_product. (exists pa_lt_hjas_iterator_h_product_bound. pa_lt_hjas_iterator_h_product_bound + S pa_i_hjas_iterator_h_product = 2 * (b + 6 * k) + 2) -> exists pa_p_hjas_iterator_h_product pa_r_hjas_iterator_h_product pa_s_hjas_iterator_h_product. ((((exists pa_h_hjas_iterator_h_product_factor. pa_h_hjas_iterator_h_product_factor + S (pa_p_hjas_iterator_h_product) = S ((S (pa_i_hjas_iterator_h_product)) * pa_c_hjas_iterator_h)) /\ exists pa_q_hjas_iterator_h_product_factor. pa_b_hjas_iterator_h = pa_q_hjas_iterator_h_product_factor * S ((S (pa_i_hjas_iterator_h_product)) * pa_c_hjas_iterator_h) + (pa_p_hjas_iterator_h_product))) /\ ((((exists pa_h_hjas_iterator_h_product_partial. pa_h_hjas_iterator_h_product_partial + S (pa_r_hjas_iterator_h_product) = S ((S (pa_i_hjas_iterator_h_product)) * pa_v_hjas_iterator_h_product)) /\ exists pa_q_hjas_iterator_h_product_partial. pa_u_hjas_iterator_h_product = pa_q_hjas_iterator_h_product_partial * S ((S (pa_i_hjas_iterator_h_product)) * pa_v_hjas_iterator_h_product) + (pa_r_hjas_iterator_h_product))) /\ ((((exists pa_h_hjas_iterator_h_product_successor. pa_h_hjas_iterator_h_product_successor + S (pa_s_hjas_iterator_h_product) = S ((S (S pa_i_hjas_iterator_h_product)) * pa_v_hjas_iterator_h_product)) /\ exists pa_q_hjas_iterator_h_product_successor. pa_u_hjas_iterator_h_product = pa_q_hjas_iterator_h_product_successor * S ((S (S pa_i_hjas_iterator_h_product)) * pa_v_hjas_iterator_h_product) + (pa_s_hjas_iterator_h_product))) /\ pa_s_hjas_iterator_h_product = pa_r_hjas_iterator_h_product * pa_p_hjas_iterator_h_product)))))))) -> (exists pa_b_hjas_iterator_h_bound pa_c_hjas_iterator_h_bound. ((forall pa_i_hjas_iterator_h_bound_repeat. (exists pa_lt_hjas_iterator_h_bound_repeat_bound. pa_lt_hjas_iterator_h_bound_repeat_bound + S pa_i_hjas_iterator_h_bound_repeat = e) -> (((exists pa_h_hjas_iterator_h_bound_repeat_decoded. pa_h_hjas_iterator_h_bound_repeat_decoded + S (4) = S ((S (pa_i_hjas_iterator_h_bound_repeat)) * pa_c_hjas_iterator_h_bound)) /\ exists pa_q_hjas_iterator_h_bound_repeat_decoded. pa_b_hjas_iterator_h_bound = pa_q_hjas_iterator_h_bound_repeat_decoded * S ((S (pa_i_hjas_iterator_h_bound_repeat)) * pa_c_hjas_iterator_h_bound) + (4)))) /\ (exists pa_u_hjas_iterator_h_bound_product pa_v_hjas_iterator_h_bound_product. ((((exists pa_h_hjas_iterator_h_bound_product_start. pa_h_hjas_iterator_h_bound_product_start + S (1) = S ((S (0)) * pa_v_hjas_iterator_h_bound_product)) /\ exists pa_q_hjas_iterator_h_bound_product_start. pa_u_hjas_iterator_h_bound_product = pa_q_hjas_iterator_h_bound_product_start * S ((S (0)) * pa_v_hjas_iterator_h_bound_product) + (1))) /\ ((((exists pa_h_hjas_iterator_h_bound_product_terminal. pa_h_hjas_iterator_h_bound_product_terminal + S (u) = S ((S (e)) * pa_v_hjas_iterator_h_bound_product)) /\ exists pa_q_hjas_iterator_h_bound_product_terminal. pa_u_hjas_iterator_h_bound_product = pa_q_hjas_iterator_h_bound_product_terminal * S ((S (e)) * pa_v_hjas_iterator_h_bound_product) + (u))) /\ forall pa_i_hjas_iterator_h_bound_product. (exists pa_lt_hjas_iterator_h_bound_product_bound. pa_lt_hjas_iterator_h_bound_product_bound + S pa_i_hjas_iterator_h_bound_product = e) -> exists pa_p_hjas_iterator_h_bound_product pa_r_hjas_iterator_h_bound_product pa_s_hjas_iterator_h_bound_product. ((((exists pa_h_hjas_iterator_h_bound_product_factor. pa_h_hjas_iterator_h_bound_product_factor + S (pa_p_hjas_iterator_h_bound_product) = S ((S (pa_i_hjas_iterator_h_bound_product)) * pa_c_hjas_iterator_h_bound)) /\ exists pa_q_hjas_iterator_h_bound_product_factor. pa_b_hjas_iterator_h_bound = pa_q_hjas_iterator_h_bound_product_factor * S ((S (pa_i_hjas_iterator_h_bound_product)) * pa_c_hjas_iterator_h_bound) + (pa_p_hjas_iterator_h_bound_product))) /\ ((((exists pa_h_hjas_iterator_h_bound_product_partial. pa_h_hjas_iterator_h_bound_product_partial + S (pa_r_hjas_iterator_h_bound_product) = S ((S (pa_i_hjas_iterator_h_bound_product)) * pa_v_hjas_iterator_h_bound_product)) /\ exists pa_q_hjas_iterator_h_bound_product_partial. pa_u_hjas_iterator_h_bound_product = pa_q_hjas_iterator_h_bound_product_partial * S ((S (pa_i_hjas_iterator_h_bound_product)) * pa_v_hjas_iterator_h_bound_product) + (pa_r_hjas_iterator_h_bound_product))) /\ ((((exists pa_h_hjas_iterator_h_bound_product_successor. pa_h_hjas_iterator_h_bound_product_successor + S (pa_s_hjas_iterator_h_bound_product) = S ((S (S pa_i_hjas_iterator_h_bound_product)) * pa_v_hjas_iterator_h_bound_product)) /\ exists pa_q_hjas_iterator_h_bound_product_successor. pa_u_hjas_iterator_h_bound_product = pa_q_hjas_iterator_h_bound_product_successor * S ((S (S pa_i_hjas_iterator_h_bound_product)) * pa_v_hjas_iterator_h_bound_product) + (pa_s_hjas_iterator_h_bound_product))) /\ pa_s_hjas_iterator_h_bound_product = pa_r_hjas_iterator_h_bound_product * pa_p_hjas_iterator_h_bound_product)))))))) -> (exists pa_b_hjas_iterator_j pa_c_hjas_iterator_j. ((forall pa_i_hjas_iterator_j_repeat. (exists pa_lt_hjas_iterator_j_repeat_bound. pa_lt_hjas_iterator_j_repeat_bound + S pa_i_hjas_iterator_j_repeat = 12) -> (((exists pa_h_hjas_iterator_j_repeat_decoded. pa_h_hjas_iterator_j_repeat_decoded + S ((b + 6 * k) + 7) = S ((S (pa_i_hjas_iterator_j_repeat)) * pa_c_hjas_iterator_j)) /\ exists pa_q_hjas_iterator_j_repeat_decoded. pa_b_hjas_iterator_j = pa_q_hjas_iterator_j_repeat_decoded * S ((S (pa_i_hjas_iterator_j_repeat)) * pa_c_hjas_iterator_j) + ((b + 6 * k) + 7)))) /\ (exists pa_u_hjas_iterator_j_product pa_v_hjas_iterator_j_product. ((((exists pa_h_hjas_iterator_j_product_start. pa_h_hjas_iterator_j_product_start + S (1) = S ((S (0)) * pa_v_hjas_iterator_j_product)) /\ exists pa_q_hjas_iterator_j_product_start. pa_u_hjas_iterator_j_product = pa_q_hjas_iterator_j_product_start * S ((S (0)) * pa_v_hjas_iterator_j_product) + (1))) /\ ((((exists pa_h_hjas_iterator_j_product_terminal. pa_h_hjas_iterator_j_product_terminal + S (j) = S ((S (12)) * pa_v_hjas_iterator_j_product)) /\ exists pa_q_hjas_iterator_j_product_terminal. pa_u_hjas_iterator_j_product = pa_q_hjas_iterator_j_product_terminal * S ((S (12)) * pa_v_hjas_iterator_j_product) + (j))) /\ forall pa_i_hjas_iterator_j_product. (exists pa_lt_hjas_iterator_j_product_bound. pa_lt_hjas_iterator_j_product_bound + S pa_i_hjas_iterator_j_product = 12) -> exists pa_p_hjas_iterator_j_product pa_r_hjas_iterator_j_product pa_s_hjas_iterator_j_product. ((((exists pa_h_hjas_iterator_j_product_factor. pa_h_hjas_iterator_j_product_factor + S (pa_p_hjas_iterator_j_product) = S ((S (pa_i_hjas_iterator_j_product)) * pa_c_hjas_iterator_j)) /\ exists pa_q_hjas_iterator_j_product_factor. pa_b_hjas_iterator_j = pa_q_hjas_iterator_j_product_factor * S ((S (pa_i_hjas_iterator_j_product)) * pa_c_hjas_iterator_j) + (pa_p_hjas_iterator_j_product))) /\ ((((exists pa_h_hjas_iterator_j_product_partial. pa_h_hjas_iterator_j_product_partial + S (pa_r_hjas_iterator_j_product) = S ((S (pa_i_hjas_iterator_j_product)) * pa_v_hjas_iterator_j_product)) /\ exists pa_q_hjas_iterator_j_product_partial. pa_u_hjas_iterator_j_product = pa_q_hjas_iterator_j_product_partial * S ((S (pa_i_hjas_iterator_j_product)) * pa_v_hjas_iterator_j_product) + (pa_r_hjas_iterator_j_product))) /\ ((((exists pa_h_hjas_iterator_j_product_successor. pa_h_hjas_iterator_j_product_successor + S (pa_s_hjas_iterator_j_product) = S ((S (S pa_i_hjas_iterator_j_product)) * pa_v_hjas_iterator_j_product)) /\ exists pa_q_hjas_iterator_j_product_successor. pa_u_hjas_iterator_j_product = pa_q_hjas_iterator_j_product_successor * S ((S (S pa_i_hjas_iterator_j_product)) * pa_v_hjas_iterator_j_product) + (pa_s_hjas_iterator_j_product))) /\ pa_s_hjas_iterator_j_product = pa_r_hjas_iterator_j_product * pa_p_hjas_iterator_j_product)))))))) -> (exists pa_b_hjas_iterator_j_bound pa_c_hjas_iterator_j_bound. ((forall pa_i_hjas_iterator_j_bound_repeat. (exists pa_lt_hjas_iterator_j_bound_repeat_bound. pa_lt_hjas_iterator_j_bound_repeat_bound + S pa_i_hjas_iterator_j_bound_repeat = (b + 6 * k) + 5) -> (((exists pa_h_hjas_iterator_j_bound_repeat_decoded. pa_h_hjas_iterator_j_bound_repeat_decoded + S (4) = S ((S (pa_i_hjas_iterator_j_bound_repeat)) * pa_c_hjas_iterator_j_bound)) /\ exists pa_q_hjas_iterator_j_bound_repeat_decoded. pa_b_hjas_iterator_j_bound = pa_q_hjas_iterator_j_bound_repeat_decoded * S ((S (pa_i_hjas_iterator_j_bound_repeat)) * pa_c_hjas_iterator_j_bound) + (4)))) /\ (exists pa_u_hjas_iterator_j_bound_product pa_v_hjas_iterator_j_bound_product. ((((exists pa_h_hjas_iterator_j_bound_product_start. pa_h_hjas_iterator_j_bound_product_start + S (1) = S ((S (0)) * pa_v_hjas_iterator_j_bound_product)) /\ exists pa_q_hjas_iterator_j_bound_product_start. pa_u_hjas_iterator_j_bound_product = pa_q_hjas_iterator_j_bound_product_start * S ((S (0)) * pa_v_hjas_iterator_j_bound_product) + (1))) /\ ((((exists pa_h_hjas_iterator_j_bound_product_terminal. pa_h_hjas_iterator_j_bound_product_terminal + S (g) = S ((S ((b + 6 * k) + 5)) * pa_v_hjas_iterator_j_bound_product)) /\ exists pa_q_hjas_iterator_j_bound_product_terminal. pa_u_hjas_iterator_j_bound_product = pa_q_hjas_iterator_j_bound_product_terminal * S ((S ((b + 6 * k) + 5)) * pa_v_hjas_iterator_j_bound_product) + (g))) /\ forall pa_i_hjas_iterator_j_bound_product. (exists pa_lt_hjas_iterator_j_bound_product_bound. pa_lt_hjas_iterator_j_bound_product_bound + S pa_i_hjas_iterator_j_bound_product = (b + 6 * k) + 5) -> exists pa_p_hjas_iterator_j_bound_product pa_r_hjas_iterator_j_bound_product pa_s_hjas_iterator_j_bound_product. ((((exists pa_h_hjas_iterator_j_bound_product_factor. pa_h_hjas_iterator_j_bound_product_factor + S (pa_p_hjas_iterator_j_bound_product) = S ((S (pa_i_hjas_iterator_j_bound_product)) * pa_c_hjas_iterator_j_bound)) /\ exists pa_q_hjas_iterator_j_bound_product_factor. pa_b_hjas_iterator_j_bound = pa_q_hjas_iterator_j_bound_product_factor * S ((S (pa_i_hjas_iterator_j_bound_product)) * pa_c_hjas_iterator_j_bound) + (pa_p_hjas_iterator_j_bound_product))) /\ ((((exists pa_h_hjas_iterator_j_bound_product_partial. pa_h_hjas_iterator_j_bound_product_partial + S (pa_r_hjas_iterator_j_bound_product) = S ((S (pa_i_hjas_iterator_j_bound_product)) * pa_v_hjas_iterator_j_bound_product)) /\ exists pa_q_hjas_iterator_j_bound_product_partial. pa_u_hjas_iterator_j_bound_product = pa_q_hjas_iterator_j_bound_product_partial * S ((S (pa_i_hjas_iterator_j_bound_product)) * pa_v_hjas_iterator_j_bound_product) + (pa_r_hjas_iterator_j_bound_product))) /\ ((((exists pa_h_hjas_iterator_j_bound_product_successor. pa_h_hjas_iterator_j_bound_product_successor + S (pa_s_hjas_iterator_j_bound_product) = S ((S (S pa_i_hjas_iterator_j_bound_product)) * pa_v_hjas_iterator_j_bound_product)) /\ exists pa_q_hjas_iterator_j_bound_product_successor. pa_u_hjas_iterator_j_bound_product = pa_q_hjas_iterator_j_bound_product_successor * S ((S (S pa_i_hjas_iterator_j_bound_product)) * pa_v_hjas_iterator_j_bound_product) + (pa_s_hjas_iterator_j_bound_product))) /\ pa_s_hjas_iterator_j_bound_product = pa_r_hjas_iterator_j_bound_product * pa_p_hjas_iterator_j_bound_product)))))))) -> (((exists bqb_le_gap_hjas_iterator_h_result. bqb_le_gap_hjas_iterator_h_result + (h) = (u)) /\ (exists bqb_le_gap_hjas_iterator_j_result. bqb_le_gap_hjas_iterator_j_result + (j) = (g))))

Proof neighborhood

Direct theorem prerequisites

BT00WW bertrand_hj_base_window_thirty_two_from_total BT00SY bertrand_hj_six_step_from_total BT00R1 ceil_div_six_total BT0013 le_add_right BT000F le_trans BT0007 mul_add BT0003 add_assoc

Direct theorem dependents

BT00X3 bertrand_hj_envelope_thirty_two

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

177 script commands · 40 reading checkpoints · 22 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 (6)
bertrand hj base window thirty two from totalbertrand hj six step from totalceil div six totalle add rightle transadd assoc
01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro htotal
  3. L3
    intro hlower
  4. L4
    intro hupper
02Induction on kL5–14

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L5
    induction k
  2. L6
    intro e
  3. L7
    intro h
  4. L8
    intro u
  5. L9
    intro j
  6. L10
    intro g
  7. L11
    intro hceiling
  8. L12
    intro hh
  9. L13
    intro hu
  10. L14
    intro hj
03Fix variables and assumptionsL15–15

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

  1. L15
    intro hg
04Establish hroot_zeroL16–18

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

  1. L16
    have hroot_zero : b + 6 * 0 = b
  2. L17
    rewrite PA5
  3. L18
    apply PA3
05Establish hzero_lowerL19–21

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

  1. L19
    have hzero_lower : Lt(31,b + 6 · 0)Definitions: Lt(31,b + 6 · 0)Original native command in the exact edition
  2. L20
    rewrite hroot_zero
  3. L21
    exact hlower
06Establish hzero_upperL22–31

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

  1. L22
    have hzero_upper : Le(b + 6 · 0,37)Definitions: Le(b + 6 · 0,37)Original native command in the exact edition
  2. L23
    rewrite hroot_zero
  3. L24
    exact hupper
  4. L25
    specialize bertrand_hj_base_window_thirty_two_from_total (b + 6 * 0)
  5. L26
    specialize bertrand_hj_base_window_thirty_two_from_total e
  6. L27
    specialize bertrand_hj_base_window_thirty_two_from_total h
  7. L28
    specialize bertrand_hj_base_window_thirty_two_from_total u
  8. L29
    specialize bertrand_hj_base_window_thirty_two_from_total j
  9. L30
    specialize bertrand_hj_base_window_thirty_two_from_total g
  10. L31
    apply bertrand_hj_base_window_thirty_two_from_total
07Use earlier factsL32–39

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

  1. L32
    exact htotal
  2. L33
    exact hzero_lower
  3. L34
    exact hzero_upper
  4. L35
    exact hceiling
  5. L36
    exact hh
  6. L37
    exact hu
  7. L38
    exact hj
  8. L39
    exact hg
08Fix variables and assumptionsL40–49

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

  1. L40
    intro e
  2. L41
    intro h
  3. L42
    intro u
  4. L43
    intro j
  5. L44
    intro g
  6. L45
    intro hceiling
  7. L46
    intro hh
  8. L47
    intro hu
  9. L48
    intro hj
  10. L49
    intro hg
09Establish hcurrent_ceilingL50–52

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

  1. L50
    have hcurrent_ceiling : ∃ ce. CeilDivSix((b + 6 · k) · (b + 6 · k),ce)Definitions: CeilDivSix((b + 6 · k) · (b + 6 · k),ce)Original native command in the exact edition
  2. L51
    specialize ceil_div_six_total ((b + 6 * k) * (b + 6 * k))
  3. L52
    exact ceil_div_six_total
10Separate the logical casesL53–53

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

  1. L53
    cases hcurrent_ceiling
11Establish hcurrent_hL54–57

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

  1. L54
    have hcurrent_h : ∃ hh. Pow(b + 6 · k + 1,2 · (b + 6 · k) + 2,hh)Definitions: Pow(b + 6 · k + 1,2 · (b + 6 · k) + 2,hh)Original native command in the exact edition
  2. L55
    specialize htotal ((b + 6 * k) + 1)
  3. L56
    specialize htotal (2 * (b + 6 * k) + 2)
  4. L57
    exact htotal
12Separate the logical casesL58–58

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

  1. L58
    cases hcurrent_h
13Establish hcurrent_uL59–62

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

  1. L59
    have hcurrent_u : ∃ hu. Pow(4,x,hu)Definitions: Pow(4,x,hu)Original native command in the exact edition
  2. L60
    specialize htotal 4
  3. L61
    specialize htotal x
  4. L62
    exact htotal
14Separate the logical casesL63–63

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

  1. L63
    cases hcurrent_u
15Establish hcurrent_jL64–67

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

  1. L64
    have hcurrent_j : ∃ jj. Pow(b + 6 · k + 7,12,jj)Definitions: Pow(b + 6 · k + 7,12,jj)Original native command in the exact edition
  2. L65
    specialize htotal ((b + 6 * k) + 7)
  3. L66
    specialize htotal 12
  4. L67
    exact htotal
16Separate the logical casesL68–68

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

  1. L68
    cases hcurrent_j
17Establish hcurrent_gL69–72

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

  1. L69
    have hcurrent_g : ∃ gg. Pow(4,b + 6 · k + 5,gg)Definitions: Pow(4,b + 6 · k + 5,gg)Original native command in the exact edition
  2. L70
    specialize htotal 4
  3. L71
    specialize htotal ((b + 6 * k) + 5)
  4. L72
    exact htotal
18Separate the logical casesL73–73

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

  1. L73
    cases hcurrent_g
19Establish hcurrent_boundsL74–83

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

  1. L74
    have hcurrent_bounds : Le(x1,x2) ∧ Le(x3,x4)Definitions: Le(x1,x2)Le(x3,x4)Original native command in the exact edition
  2. L75
    specialize IH x
  3. L76
    specialize IH x1
  4. L77
    specialize IH x2
  5. L78
    specialize IH x3
  6. L79
    specialize IH x4
  7. L80
    apply IH
  8. L81
    exact hcurrent_ceiling_witness
  9. L82
    exact hcurrent_h_witness
  10. L83
    exact hcurrent_u_witness
20Use earlier factsL84–85

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

  1. L84
    exact hcurrent_j_witness
  2. L85
    exact hcurrent_g_witness
21Separate the logical casesL86–86

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

  1. L86
    cases hcurrent_bounds
22Establish hfive_thirty_twoL87–87

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

  1. L87
    have hfive_thirty_two : Lt(4,32)Definitions: Lt(4,32)Original native command in the exact edition
23Construct an explicit witnessL88–88

Supply the displayed value, then prove that it has the required property.

  1. L88
    exists 27
24Calculate and transport equalitiesL89–89

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L89
    norm_num
25Establish hfive_baseL90–96

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

  1. L90
    have hfive_base : Lt(4,b)Definitions: Lt(4,b)Original native command in the exact edition
  2. L91
    specialize le_trans 5
  3. L92
    specialize le_trans 32
  4. L93
    specialize le_trans b
  5. L94
    apply le_trans
  6. L95
    exact hfive_thirty_two
  7. L96
    exact hlower
26Establish hbase_currentL97–100

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

  1. L97
    have hbase_current : Le(b,b + 6 · k)Definitions: Le(b,b + 6 · k)Original native command in the exact edition
  2. L98
    specialize le_add_right b
  3. L99
    specialize le_add_right (6 * k)
  4. L100
    exact le_add_right
27Establish hfive_currentL101–107

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

  1. L101
    have hfive_current : Lt(4,b + 6 · k)Definitions: Lt(4,b + 6 · k)Original native command in the exact edition
  2. L102
    specialize le_trans 5
  3. L103
    specialize le_trans b
  4. L104
    specialize le_trans (b + 6 * k)
  5. L105
    apply le_trans
  6. L106
    exact hfive_base
  7. L107
    exact hbase_current
28Establish hroot_stepL108–114

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

  1. L108
    have hroot_step : b + 6 * S k = (b + 6 * k) + 6
  2. L109
    rewrite PA6
  3. L110
    symm
  4. L111
    specialize add_assoc b
  5. L112
    specialize add_assoc (6 * k)
  6. L113
    specialize add_assoc 6
  7. L114
    apply add_assoc
29Establish hnext_h_baseL115–117

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

  1. L115
    have hnext_h_base : (b + 6 * S k) + 1 = (b + 6 * k) + 7
  2. L116
    rewrite hroot_step
  3. L117
    simp
30Establish hnext_h_exponentL118–120

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

  1. L118
    have hnext_h_exponent : 2 * (b + 6 * S k) + 2 = 2 * (b + 6 * k) + 14
  2. L119
    rewrite hroot_step
  3. L120
    simp [mul_add, add_assoc]
31Establish hnext_j_baseL121–123

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

  1. L121
    have hnext_j_base : (b + 6 * S k) + 7 = (b + 6 * k) + 13
  2. L122
    rewrite hroot_step
  3. L123
    simp [add_assoc]
32Establish hnext_j_exponentL124–126

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

  1. L124
    have hnext_j_exponent : (b + 6 * S k) + 5 = (b + 6 * k) + 11
  2. L125
    rewrite hroot_step
  3. L126
    simp [add_assoc]
33Establish hnext_ceilingL127–132

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

  1. L127
    have hnext_ceiling : CeilDivSix((b + 6 · k + 6) · (b + 6 · k + 6),e)Definitions: CeilDivSix((b + 6 · k + 6) · (b + 6 · k + 6),e)Original native command in the exact edition
  2. L128
    rewrite <- hroot_step
  3. L129
    rewrite <- hroot_step
  4. L130
    rewrite <- hroot_step
  5. L131
    rewrite <- hroot_step
  6. L132
    exact hceiling
34Establish hnext_hL133–140

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

  1. L133
    have hnext_h : Pow(b + 6 · k + 7,2 · (b + 6 · k) + 14,h)Definitions: Pow(b + 6 · k + 7,2 · (b + 6 · k) + 14,h)Original native command in the exact edition
  2. L134
    rewrite <- hnext_h_base
  3. L135
    rewrite <- hnext_h_base
  4. L136
    rewrite <- hnext_h_exponent
  5. L137
    rewrite <- hnext_h_exponent
  6. L138
    rewrite <- hnext_h_exponent
  7. L139
    rewrite <- hnext_h_exponent
  8. L140
    exact hh
35Establish hnext_jL141–144

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

  1. L141
    have hnext_j : Pow(b + 6 · k + 13,12,j)Definitions: Pow(b + 6 · k + 13,12,j)Original native command in the exact edition
  2. L142
    rewrite <- hnext_j_base
  3. L143
    rewrite <- hnext_j_base
  4. L144
    exact hj
36Establish hnext_gL145–154

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

  1. L145
    have hnext_g : Pow(4,b + 6 · k + 11,g)Definitions: Pow(4,b + 6 · k + 11,g)Original native command in the exact edition
  2. L146
    rewrite <- hnext_j_exponent
  3. L147
    rewrite <- hnext_j_exponent
  4. L148
    rewrite <- hnext_j_exponent
  5. L149
    rewrite <- hnext_j_exponent
  6. L150
    exact hg
  7. L151
    specialize bertrand_hj_six_step_from_total (b + 6 * k)
  8. L152
    specialize bertrand_hj_six_step_from_total x
  9. L153
    specialize bertrand_hj_six_step_from_total e
  10. L154
    specialize bertrand_hj_six_step_from_total x1
37Use earlier factsL155–164

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

  1. L155
    specialize bertrand_hj_six_step_from_total x2
  2. L156
    specialize bertrand_hj_six_step_from_total x3
  3. L157
    specialize bertrand_hj_six_step_from_total x4
  4. L158
    specialize bertrand_hj_six_step_from_total h
  5. L159
    specialize bertrand_hj_six_step_from_total u
  6. L160
    specialize bertrand_hj_six_step_from_total j
  7. L161
    specialize bertrand_hj_six_step_from_total g
  8. L162
    apply bertrand_hj_six_step_from_total
  9. L163
    exact htotal
  10. L164
    exact hfive_current
38Use earlier factsL165–170

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

  1. L165
    exact hcurrent_ceiling_witness
  2. L166
    exact hnext_ceiling
  3. L167
    exact hcurrent_h_witness
  4. L168
    exact hcurrent_u_witness
  5. L169
    exact hcurrent_j_witness
  6. L170
    exact hcurrent_g_witness
39Separate the logical casesL171–171

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

  1. L171
    split
40Use earlier factsL172–177

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

  1. L172
    exact hcurrent_bounds_left
  2. L173
    exact hcurrent_bounds_right
  3. L174
    exact hnext_h
  4. L175
    exact hu
  5. L176
    exact hnext_j
  6. L177
    exact hnext_g

Library-wide reading audit

Original defined command ledger · 177 lines
  1. 0001intro b
  2. 0002intro htotal
  3. 0003intro hlower
  4. 0004intro hupper
  5. 0005induction k
  6. 0006intro e
  7. 0007intro h
  8. 0008intro u
  9. 0009intro j
  10. 0010intro g
  11. 0011intro hceiling
  12. 0012intro hh
  13. 0013intro hu
  14. 0014intro hj
  15. 0015intro hg
  16. 0016have hroot_zero : b + 6 * 0 = b
  17. 0017rewrite PA5
  18. 0018apply PA3
  19. 0019have hzero_lower : Lt(31,b + 6 · 0)
    Exact native replay linehave hzero_lower : exists bqb_le_gap_hjas_iterator_zero_lower. bqb_le_gap_hjas_iterator_zero_lower + (32) = (b + 6 * 0)
  20. 0020rewrite hroot_zero
  21. 0021exact hlower
  22. 0022have hzero_upper : Le(b + 6 · 0,37)
    Exact native replay linehave hzero_upper : exists bqb_le_gap_hjas_iterator_zero_upper. bqb_le_gap_hjas_iterator_zero_upper + (b + 6 * 0) = (37)
  23. 0023rewrite hroot_zero
  24. 0024exact hupper
  25. 0025specialize bertrand_hj_base_window_thirty_two_from_total (b + 6 * 0)
  26. 0026specialize bertrand_hj_base_window_thirty_two_from_total e
  27. 0027specialize bertrand_hj_base_window_thirty_two_from_total h
  28. 0028specialize bertrand_hj_base_window_thirty_two_from_total u
  29. 0029specialize bertrand_hj_base_window_thirty_two_from_total j
  30. 0030specialize bertrand_hj_base_window_thirty_two_from_total g
  31. 0031apply bertrand_hj_base_window_thirty_two_from_total
  32. 0032exact htotal
  33. 0033exact hzero_lower
  34. 0034exact hzero_upper
  35. 0035exact hceiling
  36. 0036exact hh
  37. 0037exact hu
  38. 0038exact hj
  39. 0039exact hg
  40. 0040intro e
  41. 0041intro h
  42. 0042intro u
  43. 0043intro j
  44. 0044intro g
  45. 0045intro hceiling
  46. 0046intro hh
  47. 0047intro hu
  48. 0048intro hj
  49. 0049intro hg
  50. 0050have hcurrent_ceiling : ∃ ce. CeilDivSix((b + 6 · k) · (b + 6 · k),ce)
    Exact native replay linehave hcurrent_ceiling : exists ce. (((exists bcs_lower_gap_hjas_current_ceiling_exists. bcs_lower_gap_hjas_current_ceiling_exists + ((b + 6 * k) * (b + 6 * k)) = 6 * (ce)) /\ exists bcs_upper_gap_hjas_current_ceiling_exists. bcs_upper_gap_hjas_current_ceiling_exists + S (6 * (ce)) = ((b + 6 * k) * (b + 6 * k)) + 6))
  51. 0051specialize ceil_div_six_total ((b + 6 * k) * (b + 6 * k))
  52. 0052exact ceil_div_six_total
  53. 0053cases hcurrent_ceiling
  54. 0054have hcurrent_h : ∃ hh. Pow(b + 6 · k + 1,2 · (b + 6 · k) + 2,hh)
    Exact native replay linehave hcurrent_h : exists hh. (exists pa_b_hjas_current_h_exists pa_c_hjas_current_h_exists. ((forall pa_i_hjas_current_h_exists_repeat. (exists pa_lt_hjas_current_h_exists_repeat_bound. pa_lt_hjas_current_h_exists_repeat_bound + S pa_i_hjas_current_h_exists_repeat = 2 * (b + 6 * k) + 2) -> (((exists pa_h_hjas_current_h_exists_repeat_decoded. pa_h_hjas_current_h_exists_repeat_decoded + S ((b + 6 * k) + 1) = S ((S (pa_i_hjas_current_h_exists_repeat)) * pa_c_hjas_current_h_exists)) /\ exists pa_q_hjas_current_h_exists_repeat_decoded. pa_b_hjas_current_h_exists = pa_q_hjas_current_h_exists_repeat_decoded * S ((S (pa_i_hjas_current_h_exists_repeat)) * pa_c_hjas_current_h_exists) + ((b + 6 * k) + 1)))) /\ (exists pa_u_hjas_current_h_exists_product pa_v_hjas_current_h_exists_product. ((((exists pa_h_hjas_current_h_exists_product_start. pa_h_hjas_current_h_exists_product_start + S (1) = S ((S (0)) * pa_v_hjas_current_h_exists_product)) /\ exists pa_q_hjas_current_h_exists_product_start. pa_u_hjas_current_h_exists_product = pa_q_hjas_current_h_exists_product_start * S ((S (0)) * pa_v_hjas_current_h_exists_product) + (1))) /\ ((((exists pa_h_hjas_current_h_exists_product_terminal. pa_h_hjas_current_h_exists_product_terminal + S (hh) = S ((S (2 * (b + 6 * k) + 2)) * pa_v_hjas_current_h_exists_product)) /\ exists pa_q_hjas_current_h_exists_product_terminal. pa_u_hjas_current_h_exists_product = pa_q_hjas_current_h_exists_product_terminal * S ((S (2 * (b + 6 * k) + 2)) * pa_v_hjas_current_h_exists_product) + (hh))) /\ forall pa_i_hjas_current_h_exists_product. (exists pa_lt_hjas_current_h_exists_product_bound. pa_lt_hjas_current_h_exists_product_bound + S pa_i_hjas_current_h_exists_product = 2 * (b + 6 * k) + 2) -> exists pa_p_hjas_current_h_exists_product pa_r_hjas_current_h_exists_product pa_s_hjas_current_h_exists_product. ((((exists pa_h_hjas_current_h_exists_product_factor. pa_h_hjas_current_h_exists_product_factor + S (pa_p_hjas_current_h_exists_product) = S ((S (pa_i_hjas_current_h_exists_product)) * pa_c_hjas_current_h_exists)) /\ exists pa_q_hjas_current_h_exists_product_factor. pa_b_hjas_current_h_exists = pa_q_hjas_current_h_exists_product_factor * S ((S (pa_i_hjas_current_h_exists_product)) * pa_c_hjas_current_h_exists) + (pa_p_hjas_current_h_exists_product))) /\ ((((exists pa_h_hjas_current_h_exists_product_partial. pa_h_hjas_current_h_exists_product_partial + S (pa_r_hjas_current_h_exists_product) = S ((S (pa_i_hjas_current_h_exists_product)) * pa_v_hjas_current_h_exists_product)) /\ exists pa_q_hjas_current_h_exists_product_partial. pa_u_hjas_current_h_exists_product = pa_q_hjas_current_h_exists_product_partial * S ((S (pa_i_hjas_current_h_exists_product)) * pa_v_hjas_current_h_exists_product) + (pa_r_hjas_current_h_exists_product))) /\ ((((exists pa_h_hjas_current_h_exists_product_successor. pa_h_hjas_current_h_exists_product_successor + S (pa_s_hjas_current_h_exists_product) = S ((S (S pa_i_hjas_current_h_exists_product)) * pa_v_hjas_current_h_exists_product)) /\ exists pa_q_hjas_current_h_exists_product_successor. pa_u_hjas_current_h_exists_product = pa_q_hjas_current_h_exists_product_successor * S ((S (S pa_i_hjas_current_h_exists_product)) * pa_v_hjas_current_h_exists_product) + (pa_s_hjas_current_h_exists_product))) /\ pa_s_hjas_current_h_exists_product = pa_r_hjas_current_h_exists_product * pa_p_hjas_current_h_exists_product))))))))
  55. 0055specialize htotal ((b + 6 * k) + 1)
  56. 0056specialize htotal (2 * (b + 6 * k) + 2)
  57. 0057exact htotal
  58. 0058cases hcurrent_h
  59. 0059have hcurrent_u : ∃ hu. Pow(4,x,hu)
    Exact native replay linehave hcurrent_u : exists hu. (exists pa_b_hjas_current_u_exists pa_c_hjas_current_u_exists. ((forall pa_i_hjas_current_u_exists_repeat. (exists pa_lt_hjas_current_u_exists_repeat_bound. pa_lt_hjas_current_u_exists_repeat_bound + S pa_i_hjas_current_u_exists_repeat = x) -> (((exists pa_h_hjas_current_u_exists_repeat_decoded. pa_h_hjas_current_u_exists_repeat_decoded + S (4) = S ((S (pa_i_hjas_current_u_exists_repeat)) * pa_c_hjas_current_u_exists)) /\ exists pa_q_hjas_current_u_exists_repeat_decoded. pa_b_hjas_current_u_exists = pa_q_hjas_current_u_exists_repeat_decoded * S ((S (pa_i_hjas_current_u_exists_repeat)) * pa_c_hjas_current_u_exists) + (4)))) /\ (exists pa_u_hjas_current_u_exists_product pa_v_hjas_current_u_exists_product. ((((exists pa_h_hjas_current_u_exists_product_start. pa_h_hjas_current_u_exists_product_start + S (1) = S ((S (0)) * pa_v_hjas_current_u_exists_product)) /\ exists pa_q_hjas_current_u_exists_product_start. pa_u_hjas_current_u_exists_product = pa_q_hjas_current_u_exists_product_start * S ((S (0)) * pa_v_hjas_current_u_exists_product) + (1))) /\ ((((exists pa_h_hjas_current_u_exists_product_terminal. pa_h_hjas_current_u_exists_product_terminal + S (hu) = S ((S (x)) * pa_v_hjas_current_u_exists_product)) /\ exists pa_q_hjas_current_u_exists_product_terminal. pa_u_hjas_current_u_exists_product = pa_q_hjas_current_u_exists_product_terminal * S ((S (x)) * pa_v_hjas_current_u_exists_product) + (hu))) /\ forall pa_i_hjas_current_u_exists_product. (exists pa_lt_hjas_current_u_exists_product_bound. pa_lt_hjas_current_u_exists_product_bound + S pa_i_hjas_current_u_exists_product = x) -> exists pa_p_hjas_current_u_exists_product pa_r_hjas_current_u_exists_product pa_s_hjas_current_u_exists_product. ((((exists pa_h_hjas_current_u_exists_product_factor. pa_h_hjas_current_u_exists_product_factor + S (pa_p_hjas_current_u_exists_product) = S ((S (pa_i_hjas_current_u_exists_product)) * pa_c_hjas_current_u_exists)) /\ exists pa_q_hjas_current_u_exists_product_factor. pa_b_hjas_current_u_exists = pa_q_hjas_current_u_exists_product_factor * S ((S (pa_i_hjas_current_u_exists_product)) * pa_c_hjas_current_u_exists) + (pa_p_hjas_current_u_exists_product))) /\ ((((exists pa_h_hjas_current_u_exists_product_partial. pa_h_hjas_current_u_exists_product_partial + S (pa_r_hjas_current_u_exists_product) = S ((S (pa_i_hjas_current_u_exists_product)) * pa_v_hjas_current_u_exists_product)) /\ exists pa_q_hjas_current_u_exists_product_partial. pa_u_hjas_current_u_exists_product = pa_q_hjas_current_u_exists_product_partial * S ((S (pa_i_hjas_current_u_exists_product)) * pa_v_hjas_current_u_exists_product) + (pa_r_hjas_current_u_exists_product))) /\ ((((exists pa_h_hjas_current_u_exists_product_successor. pa_h_hjas_current_u_exists_product_successor + S (pa_s_hjas_current_u_exists_product) = S ((S (S pa_i_hjas_current_u_exists_product)) * pa_v_hjas_current_u_exists_product)) /\ exists pa_q_hjas_current_u_exists_product_successor. pa_u_hjas_current_u_exists_product = pa_q_hjas_current_u_exists_product_successor * S ((S (S pa_i_hjas_current_u_exists_product)) * pa_v_hjas_current_u_exists_product) + (pa_s_hjas_current_u_exists_product))) /\ pa_s_hjas_current_u_exists_product = pa_r_hjas_current_u_exists_product * pa_p_hjas_current_u_exists_product))))))))
  60. 0060specialize htotal 4
  61. 0061specialize htotal x
  62. 0062exact htotal
  63. 0063cases hcurrent_u
  64. 0064have hcurrent_j : ∃ jj. Pow(b + 6 · k + 7,12,jj)
    Exact native replay linehave hcurrent_j : exists jj. (exists pa_b_hjas_current_j_exists pa_c_hjas_current_j_exists. ((forall pa_i_hjas_current_j_exists_repeat. (exists pa_lt_hjas_current_j_exists_repeat_bound. pa_lt_hjas_current_j_exists_repeat_bound + S pa_i_hjas_current_j_exists_repeat = 12) -> (((exists pa_h_hjas_current_j_exists_repeat_decoded. pa_h_hjas_current_j_exists_repeat_decoded + S ((b + 6 * k) + 7) = S ((S (pa_i_hjas_current_j_exists_repeat)) * pa_c_hjas_current_j_exists)) /\ exists pa_q_hjas_current_j_exists_repeat_decoded. pa_b_hjas_current_j_exists = pa_q_hjas_current_j_exists_repeat_decoded * S ((S (pa_i_hjas_current_j_exists_repeat)) * pa_c_hjas_current_j_exists) + ((b + 6 * k) + 7)))) /\ (exists pa_u_hjas_current_j_exists_product pa_v_hjas_current_j_exists_product. ((((exists pa_h_hjas_current_j_exists_product_start. pa_h_hjas_current_j_exists_product_start + S (1) = S ((S (0)) * pa_v_hjas_current_j_exists_product)) /\ exists pa_q_hjas_current_j_exists_product_start. pa_u_hjas_current_j_exists_product = pa_q_hjas_current_j_exists_product_start * S ((S (0)) * pa_v_hjas_current_j_exists_product) + (1))) /\ ((((exists pa_h_hjas_current_j_exists_product_terminal. pa_h_hjas_current_j_exists_product_terminal + S (jj) = S ((S (12)) * pa_v_hjas_current_j_exists_product)) /\ exists pa_q_hjas_current_j_exists_product_terminal. pa_u_hjas_current_j_exists_product = pa_q_hjas_current_j_exists_product_terminal * S ((S (12)) * pa_v_hjas_current_j_exists_product) + (jj))) /\ forall pa_i_hjas_current_j_exists_product. (exists pa_lt_hjas_current_j_exists_product_bound. pa_lt_hjas_current_j_exists_product_bound + S pa_i_hjas_current_j_exists_product = 12) -> exists pa_p_hjas_current_j_exists_product pa_r_hjas_current_j_exists_product pa_s_hjas_current_j_exists_product. ((((exists pa_h_hjas_current_j_exists_product_factor. pa_h_hjas_current_j_exists_product_factor + S (pa_p_hjas_current_j_exists_product) = S ((S (pa_i_hjas_current_j_exists_product)) * pa_c_hjas_current_j_exists)) /\ exists pa_q_hjas_current_j_exists_product_factor. pa_b_hjas_current_j_exists = pa_q_hjas_current_j_exists_product_factor * S ((S (pa_i_hjas_current_j_exists_product)) * pa_c_hjas_current_j_exists) + (pa_p_hjas_current_j_exists_product))) /\ ((((exists pa_h_hjas_current_j_exists_product_partial. pa_h_hjas_current_j_exists_product_partial + S (pa_r_hjas_current_j_exists_product) = S ((S (pa_i_hjas_current_j_exists_product)) * pa_v_hjas_current_j_exists_product)) /\ exists pa_q_hjas_current_j_exists_product_partial. pa_u_hjas_current_j_exists_product = pa_q_hjas_current_j_exists_product_partial * S ((S (pa_i_hjas_current_j_exists_product)) * pa_v_hjas_current_j_exists_product) + (pa_r_hjas_current_j_exists_product))) /\ ((((exists pa_h_hjas_current_j_exists_product_successor. pa_h_hjas_current_j_exists_product_successor + S (pa_s_hjas_current_j_exists_product) = S ((S (S pa_i_hjas_current_j_exists_product)) * pa_v_hjas_current_j_exists_product)) /\ exists pa_q_hjas_current_j_exists_product_successor. pa_u_hjas_current_j_exists_product = pa_q_hjas_current_j_exists_product_successor * S ((S (S pa_i_hjas_current_j_exists_product)) * pa_v_hjas_current_j_exists_product) + (pa_s_hjas_current_j_exists_product))) /\ pa_s_hjas_current_j_exists_product = pa_r_hjas_current_j_exists_product * pa_p_hjas_current_j_exists_product))))))))
  65. 0065specialize htotal ((b + 6 * k) + 7)
  66. 0066specialize htotal 12
  67. 0067exact htotal
  68. 0068cases hcurrent_j
  69. 0069have hcurrent_g : ∃ gg. Pow(4,b + 6 · k + 5,gg)
    Exact native replay linehave hcurrent_g : exists gg. (exists pa_b_hjas_current_g_exists pa_c_hjas_current_g_exists. ((forall pa_i_hjas_current_g_exists_repeat. (exists pa_lt_hjas_current_g_exists_repeat_bound. pa_lt_hjas_current_g_exists_repeat_bound + S pa_i_hjas_current_g_exists_repeat = (b + 6 * k) + 5) -> (((exists pa_h_hjas_current_g_exists_repeat_decoded. pa_h_hjas_current_g_exists_repeat_decoded + S (4) = S ((S (pa_i_hjas_current_g_exists_repeat)) * pa_c_hjas_current_g_exists)) /\ exists pa_q_hjas_current_g_exists_repeat_decoded. pa_b_hjas_current_g_exists = pa_q_hjas_current_g_exists_repeat_decoded * S ((S (pa_i_hjas_current_g_exists_repeat)) * pa_c_hjas_current_g_exists) + (4)))) /\ (exists pa_u_hjas_current_g_exists_product pa_v_hjas_current_g_exists_product. ((((exists pa_h_hjas_current_g_exists_product_start. pa_h_hjas_current_g_exists_product_start + S (1) = S ((S (0)) * pa_v_hjas_current_g_exists_product)) /\ exists pa_q_hjas_current_g_exists_product_start. pa_u_hjas_current_g_exists_product = pa_q_hjas_current_g_exists_product_start * S ((S (0)) * pa_v_hjas_current_g_exists_product) + (1))) /\ ((((exists pa_h_hjas_current_g_exists_product_terminal. pa_h_hjas_current_g_exists_product_terminal + S (gg) = S ((S ((b + 6 * k) + 5)) * pa_v_hjas_current_g_exists_product)) /\ exists pa_q_hjas_current_g_exists_product_terminal. pa_u_hjas_current_g_exists_product = pa_q_hjas_current_g_exists_product_terminal * S ((S ((b + 6 * k) + 5)) * pa_v_hjas_current_g_exists_product) + (gg))) /\ forall pa_i_hjas_current_g_exists_product. (exists pa_lt_hjas_current_g_exists_product_bound. pa_lt_hjas_current_g_exists_product_bound + S pa_i_hjas_current_g_exists_product = (b + 6 * k) + 5) -> exists pa_p_hjas_current_g_exists_product pa_r_hjas_current_g_exists_product pa_s_hjas_current_g_exists_product. ((((exists pa_h_hjas_current_g_exists_product_factor. pa_h_hjas_current_g_exists_product_factor + S (pa_p_hjas_current_g_exists_product) = S ((S (pa_i_hjas_current_g_exists_product)) * pa_c_hjas_current_g_exists)) /\ exists pa_q_hjas_current_g_exists_product_factor. pa_b_hjas_current_g_exists = pa_q_hjas_current_g_exists_product_factor * S ((S (pa_i_hjas_current_g_exists_product)) * pa_c_hjas_current_g_exists) + (pa_p_hjas_current_g_exists_product))) /\ ((((exists pa_h_hjas_current_g_exists_product_partial. pa_h_hjas_current_g_exists_product_partial + S (pa_r_hjas_current_g_exists_product) = S ((S (pa_i_hjas_current_g_exists_product)) * pa_v_hjas_current_g_exists_product)) /\ exists pa_q_hjas_current_g_exists_product_partial. pa_u_hjas_current_g_exists_product = pa_q_hjas_current_g_exists_product_partial * S ((S (pa_i_hjas_current_g_exists_product)) * pa_v_hjas_current_g_exists_product) + (pa_r_hjas_current_g_exists_product))) /\ ((((exists pa_h_hjas_current_g_exists_product_successor. pa_h_hjas_current_g_exists_product_successor + S (pa_s_hjas_current_g_exists_product) = S ((S (S pa_i_hjas_current_g_exists_product)) * pa_v_hjas_current_g_exists_product)) /\ exists pa_q_hjas_current_g_exists_product_successor. pa_u_hjas_current_g_exists_product = pa_q_hjas_current_g_exists_product_successor * S ((S (S pa_i_hjas_current_g_exists_product)) * pa_v_hjas_current_g_exists_product) + (pa_s_hjas_current_g_exists_product))) /\ pa_s_hjas_current_g_exists_product = pa_r_hjas_current_g_exists_product * pa_p_hjas_current_g_exists_product))))))))
  70. 0070specialize htotal 4
  71. 0071specialize htotal ((b + 6 * k) + 5)
  72. 0072exact htotal
  73. 0073cases hcurrent_g
  74. 0074have hcurrent_bounds : Le(x1,x2) ∧ Le(x3,x4)
    Exact native replay linehave hcurrent_bounds : ((exists bqb_le_gap_hjas_current_h_result. bqb_le_gap_hjas_current_h_result + (x1) = (x2)) /\ (exists bqb_le_gap_hjas_current_j_result. bqb_le_gap_hjas_current_j_result + (x3) = (x4)))
  75. 0075specialize IH x
  76. 0076specialize IH x1
  77. 0077specialize IH x2
  78. 0078specialize IH x3
  79. 0079specialize IH x4
  80. 0080apply IH
  81. 0081exact hcurrent_ceiling_witness
  82. 0082exact hcurrent_h_witness
  83. 0083exact hcurrent_u_witness
  84. 0084exact hcurrent_j_witness
  85. 0085exact hcurrent_g_witness
  86. 0086cases hcurrent_bounds
  87. 0087have hfive_thirty_two : Lt(4,32)
    Exact native replay linehave hfive_thirty_two : exists bqb_le_gap_hjas_five_le_thirty_two. bqb_le_gap_hjas_five_le_thirty_two + (5) = (32)
  88. 0088exists 27
  89. 0089norm_num
  90. 0090have hfive_base : Lt(4,b)
    Exact native replay linehave hfive_base : exists bqb_le_gap_hjas_five_le_base. bqb_le_gap_hjas_five_le_base + (5) = (b)
  91. 0091specialize le_trans 5
  92. 0092specialize le_trans 32
  93. 0093specialize le_trans b
  94. 0094apply le_trans
  95. 0095exact hfive_thirty_two
  96. 0096exact hlower
  97. 0097have hbase_current : Le(b,b + 6 · k)
    Exact native replay linehave hbase_current : exists bqb_le_gap_hjas_base_le_current. bqb_le_gap_hjas_base_le_current + (b) = (b + 6 * k)
  98. 0098specialize le_add_right b
  99. 0099specialize le_add_right (6 * k)
  100. 0100exact le_add_right
  101. 0101have hfive_current : Lt(4,b + 6 · k)
    Exact native replay linehave hfive_current : exists bqb_le_gap_hjas_five_le_current. bqb_le_gap_hjas_five_le_current + (5) = (b + 6 * k)
  102. 0102specialize le_trans 5
  103. 0103specialize le_trans b
  104. 0104specialize le_trans (b + 6 * k)
  105. 0105apply le_trans
  106. 0106exact hfive_base
  107. 0107exact hbase_current
  108. 0108have hroot_step : b + 6 * S k = (b + 6 * k) + 6
  109. 0109rewrite PA6
  110. 0110symm
  111. 0111specialize add_assoc b
  112. 0112specialize add_assoc (6 * k)
  113. 0113specialize add_assoc 6
  114. 0114apply add_assoc
  115. 0115have hnext_h_base : (b + 6 * S k) + 1 = (b + 6 * k) + 7
  116. 0116rewrite hroot_step
  117. 0117simp
  118. 0118have hnext_h_exponent : 2 * (b + 6 * S k) + 2 = 2 * (b + 6 * k) + 14
  119. 0119rewrite hroot_step
  120. 0120simp [mul_add, add_assoc]
  121. 0121have hnext_j_base : (b + 6 * S k) + 7 = (b + 6 * k) + 13
  122. 0122rewrite hroot_step
  123. 0123simp [add_assoc]
  124. 0124have hnext_j_exponent : (b + 6 * S k) + 5 = (b + 6 * k) + 11
  125. 0125rewrite hroot_step
  126. 0126simp [add_assoc]
  127. 0127have hnext_ceiling : CeilDivSix((b + 6 · k + 6) · (b + 6 · k + 6),e)
    Exact native replay linehave hnext_ceiling : ((exists bcs_lower_gap_hjas_transport_next_ceiling. bcs_lower_gap_hjas_transport_next_ceiling + (((b + 6 * k) + 6) * ((b + 6 * k) + 6)) = 6 * (e)) /\ exists bcs_upper_gap_hjas_transport_next_ceiling. bcs_upper_gap_hjas_transport_next_ceiling + S (6 * (e)) = (((b + 6 * k) + 6) * ((b + 6 * k) + 6)) + 6)
  128. 0128rewrite <- hroot_step
  129. 0129rewrite <- hroot_step
  130. 0130rewrite <- hroot_step
  131. 0131rewrite <- hroot_step
  132. 0132exact hceiling
  133. 0133have hnext_h : Pow(b + 6 · k + 7,2 · (b + 6 · k) + 14,h)
    Exact native replay linehave hnext_h : exists pa_b_hjas_transport_next_h pa_c_hjas_transport_next_h. ((forall pa_i_hjas_transport_next_h_repeat. (exists pa_lt_hjas_transport_next_h_repeat_bound. pa_lt_hjas_transport_next_h_repeat_bound + S pa_i_hjas_transport_next_h_repeat = 2 * (b + 6 * k) + 14) -> (((exists pa_h_hjas_transport_next_h_repeat_decoded. pa_h_hjas_transport_next_h_repeat_decoded + S ((b + 6 * k) + 7) = S ((S (pa_i_hjas_transport_next_h_repeat)) * pa_c_hjas_transport_next_h)) /\ exists pa_q_hjas_transport_next_h_repeat_decoded. pa_b_hjas_transport_next_h = pa_q_hjas_transport_next_h_repeat_decoded * S ((S (pa_i_hjas_transport_next_h_repeat)) * pa_c_hjas_transport_next_h) + ((b + 6 * k) + 7)))) /\ (exists pa_u_hjas_transport_next_h_product pa_v_hjas_transport_next_h_product. ((((exists pa_h_hjas_transport_next_h_product_start. pa_h_hjas_transport_next_h_product_start + S (1) = S ((S (0)) * pa_v_hjas_transport_next_h_product)) /\ exists pa_q_hjas_transport_next_h_product_start. pa_u_hjas_transport_next_h_product = pa_q_hjas_transport_next_h_product_start * S ((S (0)) * pa_v_hjas_transport_next_h_product) + (1))) /\ ((((exists pa_h_hjas_transport_next_h_product_terminal. pa_h_hjas_transport_next_h_product_terminal + S (h) = S ((S (2 * (b + 6 * k) + 14)) * pa_v_hjas_transport_next_h_product)) /\ exists pa_q_hjas_transport_next_h_product_terminal. pa_u_hjas_transport_next_h_product = pa_q_hjas_transport_next_h_product_terminal * S ((S (2 * (b + 6 * k) + 14)) * pa_v_hjas_transport_next_h_product) + (h))) /\ forall pa_i_hjas_transport_next_h_product. (exists pa_lt_hjas_transport_next_h_product_bound. pa_lt_hjas_transport_next_h_product_bound + S pa_i_hjas_transport_next_h_product = 2 * (b + 6 * k) + 14) -> exists pa_p_hjas_transport_next_h_product pa_r_hjas_transport_next_h_product pa_s_hjas_transport_next_h_product. ((((exists pa_h_hjas_transport_next_h_product_factor. pa_h_hjas_transport_next_h_product_factor + S (pa_p_hjas_transport_next_h_product) = S ((S (pa_i_hjas_transport_next_h_product)) * pa_c_hjas_transport_next_h)) /\ exists pa_q_hjas_transport_next_h_product_factor. pa_b_hjas_transport_next_h = pa_q_hjas_transport_next_h_product_factor * S ((S (pa_i_hjas_transport_next_h_product)) * pa_c_hjas_transport_next_h) + (pa_p_hjas_transport_next_h_product))) /\ ((((exists pa_h_hjas_transport_next_h_product_partial. pa_h_hjas_transport_next_h_product_partial + S (pa_r_hjas_transport_next_h_product) = S ((S (pa_i_hjas_transport_next_h_product)) * pa_v_hjas_transport_next_h_product)) /\ exists pa_q_hjas_transport_next_h_product_partial. pa_u_hjas_transport_next_h_product = pa_q_hjas_transport_next_h_product_partial * S ((S (pa_i_hjas_transport_next_h_product)) * pa_v_hjas_transport_next_h_product) + (pa_r_hjas_transport_next_h_product))) /\ ((((exists pa_h_hjas_transport_next_h_product_successor. pa_h_hjas_transport_next_h_product_successor + S (pa_s_hjas_transport_next_h_product) = S ((S (S pa_i_hjas_transport_next_h_product)) * pa_v_hjas_transport_next_h_product)) /\ exists pa_q_hjas_transport_next_h_product_successor. pa_u_hjas_transport_next_h_product = pa_q_hjas_transport_next_h_product_successor * S ((S (S pa_i_hjas_transport_next_h_product)) * pa_v_hjas_transport_next_h_product) + (pa_s_hjas_transport_next_h_product))) /\ pa_s_hjas_transport_next_h_product = pa_r_hjas_transport_next_h_product * pa_p_hjas_transport_next_h_product)))))))
  134. 0134rewrite <- hnext_h_base
  135. 0135rewrite <- hnext_h_base
  136. 0136rewrite <- hnext_h_exponent
  137. 0137rewrite <- hnext_h_exponent
  138. 0138rewrite <- hnext_h_exponent
  139. 0139rewrite <- hnext_h_exponent
  140. 0140exact hh
  141. 0141have hnext_j : Pow(b + 6 · k + 13,12,j)
    Exact native replay linehave hnext_j : exists pa_b_hjas_transport_next_j pa_c_hjas_transport_next_j. ((forall pa_i_hjas_transport_next_j_repeat. (exists pa_lt_hjas_transport_next_j_repeat_bound. pa_lt_hjas_transport_next_j_repeat_bound + S pa_i_hjas_transport_next_j_repeat = 12) -> (((exists pa_h_hjas_transport_next_j_repeat_decoded. pa_h_hjas_transport_next_j_repeat_decoded + S ((b + 6 * k) + 13) = S ((S (pa_i_hjas_transport_next_j_repeat)) * pa_c_hjas_transport_next_j)) /\ exists pa_q_hjas_transport_next_j_repeat_decoded. pa_b_hjas_transport_next_j = pa_q_hjas_transport_next_j_repeat_decoded * S ((S (pa_i_hjas_transport_next_j_repeat)) * pa_c_hjas_transport_next_j) + ((b + 6 * k) + 13)))) /\ (exists pa_u_hjas_transport_next_j_product pa_v_hjas_transport_next_j_product. ((((exists pa_h_hjas_transport_next_j_product_start. pa_h_hjas_transport_next_j_product_start + S (1) = S ((S (0)) * pa_v_hjas_transport_next_j_product)) /\ exists pa_q_hjas_transport_next_j_product_start. pa_u_hjas_transport_next_j_product = pa_q_hjas_transport_next_j_product_start * S ((S (0)) * pa_v_hjas_transport_next_j_product) + (1))) /\ ((((exists pa_h_hjas_transport_next_j_product_terminal. pa_h_hjas_transport_next_j_product_terminal + S (j) = S ((S (12)) * pa_v_hjas_transport_next_j_product)) /\ exists pa_q_hjas_transport_next_j_product_terminal. pa_u_hjas_transport_next_j_product = pa_q_hjas_transport_next_j_product_terminal * S ((S (12)) * pa_v_hjas_transport_next_j_product) + (j))) /\ forall pa_i_hjas_transport_next_j_product. (exists pa_lt_hjas_transport_next_j_product_bound. pa_lt_hjas_transport_next_j_product_bound + S pa_i_hjas_transport_next_j_product = 12) -> exists pa_p_hjas_transport_next_j_product pa_r_hjas_transport_next_j_product pa_s_hjas_transport_next_j_product. ((((exists pa_h_hjas_transport_next_j_product_factor. pa_h_hjas_transport_next_j_product_factor + S (pa_p_hjas_transport_next_j_product) = S ((S (pa_i_hjas_transport_next_j_product)) * pa_c_hjas_transport_next_j)) /\ exists pa_q_hjas_transport_next_j_product_factor. pa_b_hjas_transport_next_j = pa_q_hjas_transport_next_j_product_factor * S ((S (pa_i_hjas_transport_next_j_product)) * pa_c_hjas_transport_next_j) + (pa_p_hjas_transport_next_j_product))) /\ ((((exists pa_h_hjas_transport_next_j_product_partial. pa_h_hjas_transport_next_j_product_partial + S (pa_r_hjas_transport_next_j_product) = S ((S (pa_i_hjas_transport_next_j_product)) * pa_v_hjas_transport_next_j_product)) /\ exists pa_q_hjas_transport_next_j_product_partial. pa_u_hjas_transport_next_j_product = pa_q_hjas_transport_next_j_product_partial * S ((S (pa_i_hjas_transport_next_j_product)) * pa_v_hjas_transport_next_j_product) + (pa_r_hjas_transport_next_j_product))) /\ ((((exists pa_h_hjas_transport_next_j_product_successor. pa_h_hjas_transport_next_j_product_successor + S (pa_s_hjas_transport_next_j_product) = S ((S (S pa_i_hjas_transport_next_j_product)) * pa_v_hjas_transport_next_j_product)) /\ exists pa_q_hjas_transport_next_j_product_successor. pa_u_hjas_transport_next_j_product = pa_q_hjas_transport_next_j_product_successor * S ((S (S pa_i_hjas_transport_next_j_product)) * pa_v_hjas_transport_next_j_product) + (pa_s_hjas_transport_next_j_product))) /\ pa_s_hjas_transport_next_j_product = pa_r_hjas_transport_next_j_product * pa_p_hjas_transport_next_j_product)))))))
  142. 0142rewrite <- hnext_j_base
  143. 0143rewrite <- hnext_j_base
  144. 0144exact hj
  145. 0145have hnext_g : Pow(4,b + 6 · k + 11,g)
    Exact native replay linehave hnext_g : exists pa_b_hjas_transport_next_g pa_c_hjas_transport_next_g. ((forall pa_i_hjas_transport_next_g_repeat. (exists pa_lt_hjas_transport_next_g_repeat_bound. pa_lt_hjas_transport_next_g_repeat_bound + S pa_i_hjas_transport_next_g_repeat = (b + 6 * k) + 11) -> (((exists pa_h_hjas_transport_next_g_repeat_decoded. pa_h_hjas_transport_next_g_repeat_decoded + S (4) = S ((S (pa_i_hjas_transport_next_g_repeat)) * pa_c_hjas_transport_next_g)) /\ exists pa_q_hjas_transport_next_g_repeat_decoded. pa_b_hjas_transport_next_g = pa_q_hjas_transport_next_g_repeat_decoded * S ((S (pa_i_hjas_transport_next_g_repeat)) * pa_c_hjas_transport_next_g) + (4)))) /\ (exists pa_u_hjas_transport_next_g_product pa_v_hjas_transport_next_g_product. ((((exists pa_h_hjas_transport_next_g_product_start. pa_h_hjas_transport_next_g_product_start + S (1) = S ((S (0)) * pa_v_hjas_transport_next_g_product)) /\ exists pa_q_hjas_transport_next_g_product_start. pa_u_hjas_transport_next_g_product = pa_q_hjas_transport_next_g_product_start * S ((S (0)) * pa_v_hjas_transport_next_g_product) + (1))) /\ ((((exists pa_h_hjas_transport_next_g_product_terminal. pa_h_hjas_transport_next_g_product_terminal + S (g) = S ((S ((b + 6 * k) + 11)) * pa_v_hjas_transport_next_g_product)) /\ exists pa_q_hjas_transport_next_g_product_terminal. pa_u_hjas_transport_next_g_product = pa_q_hjas_transport_next_g_product_terminal * S ((S ((b + 6 * k) + 11)) * pa_v_hjas_transport_next_g_product) + (g))) /\ forall pa_i_hjas_transport_next_g_product. (exists pa_lt_hjas_transport_next_g_product_bound. pa_lt_hjas_transport_next_g_product_bound + S pa_i_hjas_transport_next_g_product = (b + 6 * k) + 11) -> exists pa_p_hjas_transport_next_g_product pa_r_hjas_transport_next_g_product pa_s_hjas_transport_next_g_product. ((((exists pa_h_hjas_transport_next_g_product_factor. pa_h_hjas_transport_next_g_product_factor + S (pa_p_hjas_transport_next_g_product) = S ((S (pa_i_hjas_transport_next_g_product)) * pa_c_hjas_transport_next_g)) /\ exists pa_q_hjas_transport_next_g_product_factor. pa_b_hjas_transport_next_g = pa_q_hjas_transport_next_g_product_factor * S ((S (pa_i_hjas_transport_next_g_product)) * pa_c_hjas_transport_next_g) + (pa_p_hjas_transport_next_g_product))) /\ ((((exists pa_h_hjas_transport_next_g_product_partial. pa_h_hjas_transport_next_g_product_partial + S (pa_r_hjas_transport_next_g_product) = S ((S (pa_i_hjas_transport_next_g_product)) * pa_v_hjas_transport_next_g_product)) /\ exists pa_q_hjas_transport_next_g_product_partial. pa_u_hjas_transport_next_g_product = pa_q_hjas_transport_next_g_product_partial * S ((S (pa_i_hjas_transport_next_g_product)) * pa_v_hjas_transport_next_g_product) + (pa_r_hjas_transport_next_g_product))) /\ ((((exists pa_h_hjas_transport_next_g_product_successor. pa_h_hjas_transport_next_g_product_successor + S (pa_s_hjas_transport_next_g_product) = S ((S (S pa_i_hjas_transport_next_g_product)) * pa_v_hjas_transport_next_g_product)) /\ exists pa_q_hjas_transport_next_g_product_successor. pa_u_hjas_transport_next_g_product = pa_q_hjas_transport_next_g_product_successor * S ((S (S pa_i_hjas_transport_next_g_product)) * pa_v_hjas_transport_next_g_product) + (pa_s_hjas_transport_next_g_product))) /\ pa_s_hjas_transport_next_g_product = pa_r_hjas_transport_next_g_product * pa_p_hjas_transport_next_g_product)))))))
  146. 0146rewrite <- hnext_j_exponent
  147. 0147rewrite <- hnext_j_exponent
  148. 0148rewrite <- hnext_j_exponent
  149. 0149rewrite <- hnext_j_exponent
  150. 0150exact hg
  151. 0151specialize bertrand_hj_six_step_from_total (b + 6 * k)
  152. 0152specialize bertrand_hj_six_step_from_total x
  153. 0153specialize bertrand_hj_six_step_from_total e
  154. 0154specialize bertrand_hj_six_step_from_total x1
  155. 0155specialize bertrand_hj_six_step_from_total x2
  156. 0156specialize bertrand_hj_six_step_from_total x3
  157. 0157specialize bertrand_hj_six_step_from_total x4
  158. 0158specialize bertrand_hj_six_step_from_total h
  159. 0159specialize bertrand_hj_six_step_from_total u
  160. 0160specialize bertrand_hj_six_step_from_total j
  161. 0161specialize bertrand_hj_six_step_from_total g
  162. 0162apply bertrand_hj_six_step_from_total
  163. 0163exact htotal
  164. 0164exact hfive_current
  165. 0165exact hcurrent_ceiling_witness
  166. 0166exact hnext_ceiling
  167. 0167exact hcurrent_h_witness
  168. 0168exact hcurrent_u_witness
  169. 0169exact hcurrent_j_witness
  170. 0170exact hcurrent_g_witness
  171. 0171split
  172. 0172exact hcurrent_bounds_left
  173. 0173exact hcurrent_bounds_right
  174. 0174exact hnext_h
  175. 0175exact hu
  176. 0176exact hnext_j
  177. 0177exact hnext_g