BT00WO · Bertrand theorem

pow_thirty_six_double_block_eq_pow_six_four_block_from_total

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

A double block of base thirty six is a fourfold block of base six.

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

∀ m. ∀ x. ∀ y. (∀ z. ∀ n. ∃ k. Pow(z,n,k)) → Pow(36,2 · m,x) → Pow(6,4 · m,y) → x = y

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

PD0020 Pow

3 occurrences

In local proof propositions

PD0020 Pow

2 occurrences

Exact expanded native-PA statement
forall m x y. (forall bpt_a_hj32_thirty_six_block bpt_e_hj32_thirty_six_block. exists bpt_x_hj32_thirty_six_block. (exists ff_b_bpt_value_hj32_thirty_six_block ff_c_bpt_value_hj32_thirty_six_block. ((forall ff_i_bpt_value_hj32_thirty_six_block_repeat. (exists ff_lt_bpt_value_hj32_thirty_six_block_repeat_bound. ff_lt_bpt_value_hj32_thirty_six_block_repeat_bound + S ff_i_bpt_value_hj32_thirty_six_block_repeat = bpt_e_hj32_thirty_six_block) -> (((exists ff_h_bpt_value_hj32_thirty_six_block_repeat_decoded. ff_h_bpt_value_hj32_thirty_six_block_repeat_decoded + S (bpt_a_hj32_thirty_six_block) = S ((S (ff_i_bpt_value_hj32_thirty_six_block_repeat)) * ff_c_bpt_value_hj32_thirty_six_block)) /\ exists ff_q_bpt_value_hj32_thirty_six_block_repeat_decoded. ff_b_bpt_value_hj32_thirty_six_block = ff_q_bpt_value_hj32_thirty_six_block_repeat_decoded * S ((S (ff_i_bpt_value_hj32_thirty_six_block_repeat)) * ff_c_bpt_value_hj32_thirty_six_block) + (bpt_a_hj32_thirty_six_block)))) /\ (exists ff_u_bpt_value_hj32_thirty_six_block_product ff_v_bpt_value_hj32_thirty_six_block_product. ((((exists ff_h_bpt_value_hj32_thirty_six_block_product_start. ff_h_bpt_value_hj32_thirty_six_block_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_thirty_six_block_product)) /\ exists ff_q_bpt_value_hj32_thirty_six_block_product_start. ff_u_bpt_value_hj32_thirty_six_block_product = ff_q_bpt_value_hj32_thirty_six_block_product_start * S ((S (0)) * ff_v_bpt_value_hj32_thirty_six_block_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_thirty_six_block_product_terminal. ff_h_bpt_value_hj32_thirty_six_block_product_terminal + S (bpt_x_hj32_thirty_six_block) = S ((S (bpt_e_hj32_thirty_six_block)) * ff_v_bpt_value_hj32_thirty_six_block_product)) /\ exists ff_q_bpt_value_hj32_thirty_six_block_product_terminal. ff_u_bpt_value_hj32_thirty_six_block_product = ff_q_bpt_value_hj32_thirty_six_block_product_terminal * S ((S (bpt_e_hj32_thirty_six_block)) * ff_v_bpt_value_hj32_thirty_six_block_product) + (bpt_x_hj32_thirty_six_block))) /\ forall ff_i_bpt_value_hj32_thirty_six_block_product. (exists ff_lt_bpt_value_hj32_thirty_six_block_product_bound. ff_lt_bpt_value_hj32_thirty_six_block_product_bound + S ff_i_bpt_value_hj32_thirty_six_block_product = bpt_e_hj32_thirty_six_block) -> exists ff_p_bpt_value_hj32_thirty_six_block_product ff_r_bpt_value_hj32_thirty_six_block_product ff_s_bpt_value_hj32_thirty_six_block_product. ((((exists ff_h_bpt_value_hj32_thirty_six_block_product_factor. ff_h_bpt_value_hj32_thirty_six_block_product_factor + S (ff_p_bpt_value_hj32_thirty_six_block_product) = S ((S (ff_i_bpt_value_hj32_thirty_six_block_product)) * ff_c_bpt_value_hj32_thirty_six_block)) /\ exists ff_q_bpt_value_hj32_thirty_six_block_product_factor. ff_b_bpt_value_hj32_thirty_six_block = ff_q_bpt_value_hj32_thirty_six_block_product_factor * S ((S (ff_i_bpt_value_hj32_thirty_six_block_product)) * ff_c_bpt_value_hj32_thirty_six_block) + (ff_p_bpt_value_hj32_thirty_six_block_product))) /\ ((((exists ff_h_bpt_value_hj32_thirty_six_block_product_partial. ff_h_bpt_value_hj32_thirty_six_block_product_partial + S (ff_r_bpt_value_hj32_thirty_six_block_product) = S ((S (ff_i_bpt_value_hj32_thirty_six_block_product)) * ff_v_bpt_value_hj32_thirty_six_block_product)) /\ exists ff_q_bpt_value_hj32_thirty_six_block_product_partial. ff_u_bpt_value_hj32_thirty_six_block_product = ff_q_bpt_value_hj32_thirty_six_block_product_partial * S ((S (ff_i_bpt_value_hj32_thirty_six_block_product)) * ff_v_bpt_value_hj32_thirty_six_block_product) + (ff_r_bpt_value_hj32_thirty_six_block_product))) /\ ((((exists ff_h_bpt_value_hj32_thirty_six_block_product_successor. ff_h_bpt_value_hj32_thirty_six_block_product_successor + S (ff_s_bpt_value_hj32_thirty_six_block_product) = S ((S (S ff_i_bpt_value_hj32_thirty_six_block_product)) * ff_v_bpt_value_hj32_thirty_six_block_product)) /\ exists ff_q_bpt_value_hj32_thirty_six_block_product_successor. ff_u_bpt_value_hj32_thirty_six_block_product = ff_q_bpt_value_hj32_thirty_six_block_product_successor * S ((S (S ff_i_bpt_value_hj32_thirty_six_block_product)) * ff_v_bpt_value_hj32_thirty_six_block_product) + (ff_s_bpt_value_hj32_thirty_six_block_product))) /\ ff_s_bpt_value_hj32_thirty_six_block_product = ff_r_bpt_value_hj32_thirty_six_block_product * ff_p_bpt_value_hj32_thirty_six_block_product))))))))) -> (exists pa_b_hj32_thirty_six_left pa_c_hj32_thirty_six_left. ((forall pa_i_hj32_thirty_six_left_repeat. (exists pa_lt_hj32_thirty_six_left_repeat_bound. pa_lt_hj32_thirty_six_left_repeat_bound + S pa_i_hj32_thirty_six_left_repeat = 2 * m) -> (((exists pa_h_hj32_thirty_six_left_repeat_decoded. pa_h_hj32_thirty_six_left_repeat_decoded + S (36) = S ((S (pa_i_hj32_thirty_six_left_repeat)) * pa_c_hj32_thirty_six_left)) /\ exists pa_q_hj32_thirty_six_left_repeat_decoded. pa_b_hj32_thirty_six_left = pa_q_hj32_thirty_six_left_repeat_decoded * S ((S (pa_i_hj32_thirty_six_left_repeat)) * pa_c_hj32_thirty_six_left) + (36)))) /\ (exists pa_u_hj32_thirty_six_left_product pa_v_hj32_thirty_six_left_product. ((((exists pa_h_hj32_thirty_six_left_product_start. pa_h_hj32_thirty_six_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_thirty_six_left_product)) /\ exists pa_q_hj32_thirty_six_left_product_start. pa_u_hj32_thirty_six_left_product = pa_q_hj32_thirty_six_left_product_start * S ((S (0)) * pa_v_hj32_thirty_six_left_product) + (1))) /\ ((((exists pa_h_hj32_thirty_six_left_product_terminal. pa_h_hj32_thirty_six_left_product_terminal + S (x) = S ((S (2 * m)) * pa_v_hj32_thirty_six_left_product)) /\ exists pa_q_hj32_thirty_six_left_product_terminal. pa_u_hj32_thirty_six_left_product = pa_q_hj32_thirty_six_left_product_terminal * S ((S (2 * m)) * pa_v_hj32_thirty_six_left_product) + (x))) /\ forall pa_i_hj32_thirty_six_left_product. (exists pa_lt_hj32_thirty_six_left_product_bound. pa_lt_hj32_thirty_six_left_product_bound + S pa_i_hj32_thirty_six_left_product = 2 * m) -> exists pa_p_hj32_thirty_six_left_product pa_r_hj32_thirty_six_left_product pa_s_hj32_thirty_six_left_product. ((((exists pa_h_hj32_thirty_six_left_product_factor. pa_h_hj32_thirty_six_left_product_factor + S (pa_p_hj32_thirty_six_left_product) = S ((S (pa_i_hj32_thirty_six_left_product)) * pa_c_hj32_thirty_six_left)) /\ exists pa_q_hj32_thirty_six_left_product_factor. pa_b_hj32_thirty_six_left = pa_q_hj32_thirty_six_left_product_factor * S ((S (pa_i_hj32_thirty_six_left_product)) * pa_c_hj32_thirty_six_left) + (pa_p_hj32_thirty_six_left_product))) /\ ((((exists pa_h_hj32_thirty_six_left_product_partial. pa_h_hj32_thirty_six_left_product_partial + S (pa_r_hj32_thirty_six_left_product) = S ((S (pa_i_hj32_thirty_six_left_product)) * pa_v_hj32_thirty_six_left_product)) /\ exists pa_q_hj32_thirty_six_left_product_partial. pa_u_hj32_thirty_six_left_product = pa_q_hj32_thirty_six_left_product_partial * S ((S (pa_i_hj32_thirty_six_left_product)) * pa_v_hj32_thirty_six_left_product) + (pa_r_hj32_thirty_six_left_product))) /\ ((((exists pa_h_hj32_thirty_six_left_product_successor. pa_h_hj32_thirty_six_left_product_successor + S (pa_s_hj32_thirty_six_left_product) = S ((S (S pa_i_hj32_thirty_six_left_product)) * pa_v_hj32_thirty_six_left_product)) /\ exists pa_q_hj32_thirty_six_left_product_successor. pa_u_hj32_thirty_six_left_product = pa_q_hj32_thirty_six_left_product_successor * S ((S (S pa_i_hj32_thirty_six_left_product)) * pa_v_hj32_thirty_six_left_product) + (pa_s_hj32_thirty_six_left_product))) /\ pa_s_hj32_thirty_six_left_product = pa_r_hj32_thirty_six_left_product * pa_p_hj32_thirty_six_left_product)))))))) -> (exists pa_b_hj32_thirty_six_right pa_c_hj32_thirty_six_right. ((forall pa_i_hj32_thirty_six_right_repeat. (exists pa_lt_hj32_thirty_six_right_repeat_bound. pa_lt_hj32_thirty_six_right_repeat_bound + S pa_i_hj32_thirty_six_right_repeat = 4 * m) -> (((exists pa_h_hj32_thirty_six_right_repeat_decoded. pa_h_hj32_thirty_six_right_repeat_decoded + S (6) = S ((S (pa_i_hj32_thirty_six_right_repeat)) * pa_c_hj32_thirty_six_right)) /\ exists pa_q_hj32_thirty_six_right_repeat_decoded. pa_b_hj32_thirty_six_right = pa_q_hj32_thirty_six_right_repeat_decoded * S ((S (pa_i_hj32_thirty_six_right_repeat)) * pa_c_hj32_thirty_six_right) + (6)))) /\ (exists pa_u_hj32_thirty_six_right_product pa_v_hj32_thirty_six_right_product. ((((exists pa_h_hj32_thirty_six_right_product_start. pa_h_hj32_thirty_six_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_thirty_six_right_product)) /\ exists pa_q_hj32_thirty_six_right_product_start. pa_u_hj32_thirty_six_right_product = pa_q_hj32_thirty_six_right_product_start * S ((S (0)) * pa_v_hj32_thirty_six_right_product) + (1))) /\ ((((exists pa_h_hj32_thirty_six_right_product_terminal. pa_h_hj32_thirty_six_right_product_terminal + S (y) = S ((S (4 * m)) * pa_v_hj32_thirty_six_right_product)) /\ exists pa_q_hj32_thirty_six_right_product_terminal. pa_u_hj32_thirty_six_right_product = pa_q_hj32_thirty_six_right_product_terminal * S ((S (4 * m)) * pa_v_hj32_thirty_six_right_product) + (y))) /\ forall pa_i_hj32_thirty_six_right_product. (exists pa_lt_hj32_thirty_six_right_product_bound. pa_lt_hj32_thirty_six_right_product_bound + S pa_i_hj32_thirty_six_right_product = 4 * m) -> exists pa_p_hj32_thirty_six_right_product pa_r_hj32_thirty_six_right_product pa_s_hj32_thirty_six_right_product. ((((exists pa_h_hj32_thirty_six_right_product_factor. pa_h_hj32_thirty_six_right_product_factor + S (pa_p_hj32_thirty_six_right_product) = S ((S (pa_i_hj32_thirty_six_right_product)) * pa_c_hj32_thirty_six_right)) /\ exists pa_q_hj32_thirty_six_right_product_factor. pa_b_hj32_thirty_six_right = pa_q_hj32_thirty_six_right_product_factor * S ((S (pa_i_hj32_thirty_six_right_product)) * pa_c_hj32_thirty_six_right) + (pa_p_hj32_thirty_six_right_product))) /\ ((((exists pa_h_hj32_thirty_six_right_product_partial. pa_h_hj32_thirty_six_right_product_partial + S (pa_r_hj32_thirty_six_right_product) = S ((S (pa_i_hj32_thirty_six_right_product)) * pa_v_hj32_thirty_six_right_product)) /\ exists pa_q_hj32_thirty_six_right_product_partial. pa_u_hj32_thirty_six_right_product = pa_q_hj32_thirty_six_right_product_partial * S ((S (pa_i_hj32_thirty_six_right_product)) * pa_v_hj32_thirty_six_right_product) + (pa_r_hj32_thirty_six_right_product))) /\ ((((exists pa_h_hj32_thirty_six_right_product_successor. pa_h_hj32_thirty_six_right_product_successor + S (pa_s_hj32_thirty_six_right_product) = S ((S (S pa_i_hj32_thirty_six_right_product)) * pa_v_hj32_thirty_six_right_product)) /\ exists pa_q_hj32_thirty_six_right_product_successor. pa_u_hj32_thirty_six_right_product = pa_q_hj32_thirty_six_right_product_successor * S ((S (S pa_i_hj32_thirty_six_right_product)) * pa_v_hj32_thirty_six_right_product) + (pa_s_hj32_thirty_six_right_product))) /\ pa_s_hj32_thirty_six_right_product = pa_r_hj32_thirty_six_right_product * pa_p_hj32_thirty_six_right_product)))))))) -> x = y

Proof neighborhood

Direct theorem prerequisites

BT009W pow_two BT00SM pow_mul_exp_from_total BT0008 mul_assoc

Direct theorem dependents

BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_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

47 script commands · 9 reading checkpoints · 6 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 (3)
pow twopow mul exp from totalmul assoc
01Fix variables and assumptionsL1–6

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

  1. L1
    intro m
  2. L2
    intro x
  3. L3
    intro y
  4. L4
    intro htotal
  5. L5
    intro hx
  6. L6
    intro hy
02Establish ts_seed_anyL7–10

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

  1. L7
    have ts_seed_any : ∃ ts_value. Pow(6,2,ts_value)Definitions: Pow(6,2,ts_value)Original native command in the exact edition
  2. L8
    specialize htotal 6
  3. L9
    specialize htotal 2
  4. L10
    exact htotal
03Separate the logical casesL11–11

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

  1. L11
    cases ts_seed_any
04Establish ts_valueL12–12

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

  1. L12
    have ts_value : x1 = 36
05Establish ts_squareL13–22

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

  1. L13
    have ts_square : x1 = 6 * 6
  2. L14
    specialize pow_two 6
  3. L15
    specialize pow_two 2
  4. L16
    specialize pow_two x1
  5. L17
    apply pow_two
  6. L18
    refl
  7. L19
    exact ts_seed_any_witness
  8. L20
    trans 6 * 6
  9. L21
    exact ts_square
  10. L22
    norm_num
06Establish ts_seedL23–26

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

  1. L23
    have ts_seed : Pow(6,2,36)Definitions: Pow(6,2,36)Original native command in the exact edition
  2. L24
    rewrite <- ts_value
  3. L25
    rewrite <- ts_value
  4. L26
    exact ts_seed_any_witness
07Establish ts_exponentL27–27

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

  1. L27
    have ts_exponent : 4 * m = 2 * (2 * m)
08Establish ts_fourL28–37

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

  1. L28
    have ts_four : 4 = 2 * 2
  2. L29
    norm_num
  3. L30
    rewrite ts_four
  4. L31
    specialize mul_assoc 2
  5. L32
    specialize mul_assoc 2
  6. L33
    specialize mul_assoc m
  7. L34
    apply mul_assoc
  8. L35
    specialize pow_mul_exp_from_total 6
  9. L36
    specialize pow_mul_exp_from_total 2
  10. L37
    specialize pow_mul_exp_from_total (2 * m)
09Use earlier factsL38–47

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

  1. L38
    specialize pow_mul_exp_from_total (4 * m)
  2. L39
    specialize pow_mul_exp_from_total 36
  3. L40
    specialize pow_mul_exp_from_total x
  4. L41
    specialize pow_mul_exp_from_total y
  5. L42
    apply pow_mul_exp_from_total
  6. L43
    exact htotal
  7. L44
    exact ts_exponent
  8. L45
    exact ts_seed
  9. L46
    exact hx
  10. L47
    exact hy

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro m
  2. 0002intro x
  3. 0003intro y
  4. 0004intro htotal
  5. 0005intro hx
  6. 0006intro hy
  7. 0007have ts_seed_any : ∃ ts_value. Pow(6,2,ts_value)
    Exact native replay linehave ts_seed_any : exists ts_value. (exists pa_b_hj32_ts_seed_any pa_c_hj32_ts_seed_any. ((forall pa_i_hj32_ts_seed_any_repeat. (exists pa_lt_hj32_ts_seed_any_repeat_bound. pa_lt_hj32_ts_seed_any_repeat_bound + S pa_i_hj32_ts_seed_any_repeat = 2) -> (((exists pa_h_hj32_ts_seed_any_repeat_decoded. pa_h_hj32_ts_seed_any_repeat_decoded + S (6) = S ((S (pa_i_hj32_ts_seed_any_repeat)) * pa_c_hj32_ts_seed_any)) /\ exists pa_q_hj32_ts_seed_any_repeat_decoded. pa_b_hj32_ts_seed_any = pa_q_hj32_ts_seed_any_repeat_decoded * S ((S (pa_i_hj32_ts_seed_any_repeat)) * pa_c_hj32_ts_seed_any) + (6)))) /\ (exists pa_u_hj32_ts_seed_any_product pa_v_hj32_ts_seed_any_product. ((((exists pa_h_hj32_ts_seed_any_product_start. pa_h_hj32_ts_seed_any_product_start + S (1) = S ((S (0)) * pa_v_hj32_ts_seed_any_product)) /\ exists pa_q_hj32_ts_seed_any_product_start. pa_u_hj32_ts_seed_any_product = pa_q_hj32_ts_seed_any_product_start * S ((S (0)) * pa_v_hj32_ts_seed_any_product) + (1))) /\ ((((exists pa_h_hj32_ts_seed_any_product_terminal. pa_h_hj32_ts_seed_any_product_terminal + S (ts_value) = S ((S (2)) * pa_v_hj32_ts_seed_any_product)) /\ exists pa_q_hj32_ts_seed_any_product_terminal. pa_u_hj32_ts_seed_any_product = pa_q_hj32_ts_seed_any_product_terminal * S ((S (2)) * pa_v_hj32_ts_seed_any_product) + (ts_value))) /\ forall pa_i_hj32_ts_seed_any_product. (exists pa_lt_hj32_ts_seed_any_product_bound. pa_lt_hj32_ts_seed_any_product_bound + S pa_i_hj32_ts_seed_any_product = 2) -> exists pa_p_hj32_ts_seed_any_product pa_r_hj32_ts_seed_any_product pa_s_hj32_ts_seed_any_product. ((((exists pa_h_hj32_ts_seed_any_product_factor. pa_h_hj32_ts_seed_any_product_factor + S (pa_p_hj32_ts_seed_any_product) = S ((S (pa_i_hj32_ts_seed_any_product)) * pa_c_hj32_ts_seed_any)) /\ exists pa_q_hj32_ts_seed_any_product_factor. pa_b_hj32_ts_seed_any = pa_q_hj32_ts_seed_any_product_factor * S ((S (pa_i_hj32_ts_seed_any_product)) * pa_c_hj32_ts_seed_any) + (pa_p_hj32_ts_seed_any_product))) /\ ((((exists pa_h_hj32_ts_seed_any_product_partial. pa_h_hj32_ts_seed_any_product_partial + S (pa_r_hj32_ts_seed_any_product) = S ((S (pa_i_hj32_ts_seed_any_product)) * pa_v_hj32_ts_seed_any_product)) /\ exists pa_q_hj32_ts_seed_any_product_partial. pa_u_hj32_ts_seed_any_product = pa_q_hj32_ts_seed_any_product_partial * S ((S (pa_i_hj32_ts_seed_any_product)) * pa_v_hj32_ts_seed_any_product) + (pa_r_hj32_ts_seed_any_product))) /\ ((((exists pa_h_hj32_ts_seed_any_product_successor. pa_h_hj32_ts_seed_any_product_successor + S (pa_s_hj32_ts_seed_any_product) = S ((S (S pa_i_hj32_ts_seed_any_product)) * pa_v_hj32_ts_seed_any_product)) /\ exists pa_q_hj32_ts_seed_any_product_successor. pa_u_hj32_ts_seed_any_product = pa_q_hj32_ts_seed_any_product_successor * S ((S (S pa_i_hj32_ts_seed_any_product)) * pa_v_hj32_ts_seed_any_product) + (pa_s_hj32_ts_seed_any_product))) /\ pa_s_hj32_ts_seed_any_product = pa_r_hj32_ts_seed_any_product * pa_p_hj32_ts_seed_any_product))))))))
  8. 0008specialize htotal 6
  9. 0009specialize htotal 2
  10. 0010exact htotal
  11. 0011cases ts_seed_any
  12. 0012have ts_value : x1 = 36
  13. 0013have ts_square : x1 = 6 * 6
  14. 0014specialize pow_two 6
  15. 0015specialize pow_two 2
  16. 0016specialize pow_two x1
  17. 0017apply pow_two
  18. 0018refl
  19. 0019exact ts_seed_any_witness
  20. 0020trans 6 * 6
  21. 0021exact ts_square
  22. 0022norm_num
  23. 0023have ts_seed : Pow(6,2,36)
    Exact native replay linehave ts_seed : exists pa_b_hj32_ts_seed pa_c_hj32_ts_seed. ((forall pa_i_hj32_ts_seed_repeat. (exists pa_lt_hj32_ts_seed_repeat_bound. pa_lt_hj32_ts_seed_repeat_bound + S pa_i_hj32_ts_seed_repeat = 2) -> (((exists pa_h_hj32_ts_seed_repeat_decoded. pa_h_hj32_ts_seed_repeat_decoded + S (6) = S ((S (pa_i_hj32_ts_seed_repeat)) * pa_c_hj32_ts_seed)) /\ exists pa_q_hj32_ts_seed_repeat_decoded. pa_b_hj32_ts_seed = pa_q_hj32_ts_seed_repeat_decoded * S ((S (pa_i_hj32_ts_seed_repeat)) * pa_c_hj32_ts_seed) + (6)))) /\ (exists pa_u_hj32_ts_seed_product pa_v_hj32_ts_seed_product. ((((exists pa_h_hj32_ts_seed_product_start. pa_h_hj32_ts_seed_product_start + S (1) = S ((S (0)) * pa_v_hj32_ts_seed_product)) /\ exists pa_q_hj32_ts_seed_product_start. pa_u_hj32_ts_seed_product = pa_q_hj32_ts_seed_product_start * S ((S (0)) * pa_v_hj32_ts_seed_product) + (1))) /\ ((((exists pa_h_hj32_ts_seed_product_terminal. pa_h_hj32_ts_seed_product_terminal + S (36) = S ((S (2)) * pa_v_hj32_ts_seed_product)) /\ exists pa_q_hj32_ts_seed_product_terminal. pa_u_hj32_ts_seed_product = pa_q_hj32_ts_seed_product_terminal * S ((S (2)) * pa_v_hj32_ts_seed_product) + (36))) /\ forall pa_i_hj32_ts_seed_product. (exists pa_lt_hj32_ts_seed_product_bound. pa_lt_hj32_ts_seed_product_bound + S pa_i_hj32_ts_seed_product = 2) -> exists pa_p_hj32_ts_seed_product pa_r_hj32_ts_seed_product pa_s_hj32_ts_seed_product. ((((exists pa_h_hj32_ts_seed_product_factor. pa_h_hj32_ts_seed_product_factor + S (pa_p_hj32_ts_seed_product) = S ((S (pa_i_hj32_ts_seed_product)) * pa_c_hj32_ts_seed)) /\ exists pa_q_hj32_ts_seed_product_factor. pa_b_hj32_ts_seed = pa_q_hj32_ts_seed_product_factor * S ((S (pa_i_hj32_ts_seed_product)) * pa_c_hj32_ts_seed) + (pa_p_hj32_ts_seed_product))) /\ ((((exists pa_h_hj32_ts_seed_product_partial. pa_h_hj32_ts_seed_product_partial + S (pa_r_hj32_ts_seed_product) = S ((S (pa_i_hj32_ts_seed_product)) * pa_v_hj32_ts_seed_product)) /\ exists pa_q_hj32_ts_seed_product_partial. pa_u_hj32_ts_seed_product = pa_q_hj32_ts_seed_product_partial * S ((S (pa_i_hj32_ts_seed_product)) * pa_v_hj32_ts_seed_product) + (pa_r_hj32_ts_seed_product))) /\ ((((exists pa_h_hj32_ts_seed_product_successor. pa_h_hj32_ts_seed_product_successor + S (pa_s_hj32_ts_seed_product) = S ((S (S pa_i_hj32_ts_seed_product)) * pa_v_hj32_ts_seed_product)) /\ exists pa_q_hj32_ts_seed_product_successor. pa_u_hj32_ts_seed_product = pa_q_hj32_ts_seed_product_successor * S ((S (S pa_i_hj32_ts_seed_product)) * pa_v_hj32_ts_seed_product) + (pa_s_hj32_ts_seed_product))) /\ pa_s_hj32_ts_seed_product = pa_r_hj32_ts_seed_product * pa_p_hj32_ts_seed_product)))))))
  24. 0024rewrite <- ts_value
  25. 0025rewrite <- ts_value
  26. 0026exact ts_seed_any_witness
  27. 0027have ts_exponent : 4 * m = 2 * (2 * m)
  28. 0028have ts_four : 4 = 2 * 2
  29. 0029norm_num
  30. 0030rewrite ts_four
  31. 0031specialize mul_assoc 2
  32. 0032specialize mul_assoc 2
  33. 0033specialize mul_assoc m
  34. 0034apply mul_assoc
  35. 0035specialize pow_mul_exp_from_total 6
  36. 0036specialize pow_mul_exp_from_total 2
  37. 0037specialize pow_mul_exp_from_total (2 * m)
  38. 0038specialize pow_mul_exp_from_total (4 * m)
  39. 0039specialize pow_mul_exp_from_total 36
  40. 0040specialize pow_mul_exp_from_total x
  41. 0041specialize pow_mul_exp_from_total y
  42. 0042apply pow_mul_exp_from_total
  43. 0043exact htotal
  44. 0044exact ts_exponent
  45. 0045exact ts_seed
  46. 0046exact hx
  47. 0047exact hy