BT00WT · Bertrand theorem

bertrand_h_root_36_from_total

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

The RFC-v1 H envelope at the fixed root 36.

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

∀ e. ∀ h. ∀ u. (∀ x. ∀ y. ∃ z. Pow(x,y,z)) → CeilDivSix(36 · 36,e) → Pow(36 + 1,2 · 36 + 2,h) → Pow(4,e,u) → Le(h,u)

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 PD0020 Pow PD0052 CeilDivSix

5 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0020 Pow

18 occurrences

Exact expanded native-PA statement
forall e h u. (forall bpt_a_hj32_h_root_36 bpt_e_hj32_h_root_36. exists bpt_x_hj32_h_root_36. (exists ff_b_bpt_value_hj32_h_root_36 ff_c_bpt_value_hj32_h_root_36. ((forall ff_i_bpt_value_hj32_h_root_36_repeat. (exists ff_lt_bpt_value_hj32_h_root_36_repeat_bound. ff_lt_bpt_value_hj32_h_root_36_repeat_bound + S ff_i_bpt_value_hj32_h_root_36_repeat = bpt_e_hj32_h_root_36) -> (((exists ff_h_bpt_value_hj32_h_root_36_repeat_decoded. ff_h_bpt_value_hj32_h_root_36_repeat_decoded + S (bpt_a_hj32_h_root_36) = S ((S (ff_i_bpt_value_hj32_h_root_36_repeat)) * ff_c_bpt_value_hj32_h_root_36)) /\ exists ff_q_bpt_value_hj32_h_root_36_repeat_decoded. ff_b_bpt_value_hj32_h_root_36 = ff_q_bpt_value_hj32_h_root_36_repeat_decoded * S ((S (ff_i_bpt_value_hj32_h_root_36_repeat)) * ff_c_bpt_value_hj32_h_root_36) + (bpt_a_hj32_h_root_36)))) /\ (exists ff_u_bpt_value_hj32_h_root_36_product ff_v_bpt_value_hj32_h_root_36_product. ((((exists ff_h_bpt_value_hj32_h_root_36_product_start. ff_h_bpt_value_hj32_h_root_36_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_h_root_36_product)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_start. ff_u_bpt_value_hj32_h_root_36_product = ff_q_bpt_value_hj32_h_root_36_product_start * S ((S (0)) * ff_v_bpt_value_hj32_h_root_36_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_h_root_36_product_terminal. ff_h_bpt_value_hj32_h_root_36_product_terminal + S (bpt_x_hj32_h_root_36) = S ((S (bpt_e_hj32_h_root_36)) * ff_v_bpt_value_hj32_h_root_36_product)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_terminal. ff_u_bpt_value_hj32_h_root_36_product = ff_q_bpt_value_hj32_h_root_36_product_terminal * S ((S (bpt_e_hj32_h_root_36)) * ff_v_bpt_value_hj32_h_root_36_product) + (bpt_x_hj32_h_root_36))) /\ forall ff_i_bpt_value_hj32_h_root_36_product. (exists ff_lt_bpt_value_hj32_h_root_36_product_bound. ff_lt_bpt_value_hj32_h_root_36_product_bound + S ff_i_bpt_value_hj32_h_root_36_product = bpt_e_hj32_h_root_36) -> exists ff_p_bpt_value_hj32_h_root_36_product ff_r_bpt_value_hj32_h_root_36_product ff_s_bpt_value_hj32_h_root_36_product. ((((exists ff_h_bpt_value_hj32_h_root_36_product_factor. ff_h_bpt_value_hj32_h_root_36_product_factor + S (ff_p_bpt_value_hj32_h_root_36_product) = S ((S (ff_i_bpt_value_hj32_h_root_36_product)) * ff_c_bpt_value_hj32_h_root_36)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_factor. ff_b_bpt_value_hj32_h_root_36 = ff_q_bpt_value_hj32_h_root_36_product_factor * S ((S (ff_i_bpt_value_hj32_h_root_36_product)) * ff_c_bpt_value_hj32_h_root_36) + (ff_p_bpt_value_hj32_h_root_36_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_36_product_partial. ff_h_bpt_value_hj32_h_root_36_product_partial + S (ff_r_bpt_value_hj32_h_root_36_product) = S ((S (ff_i_bpt_value_hj32_h_root_36_product)) * ff_v_bpt_value_hj32_h_root_36_product)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_partial. ff_u_bpt_value_hj32_h_root_36_product = ff_q_bpt_value_hj32_h_root_36_product_partial * S ((S (ff_i_bpt_value_hj32_h_root_36_product)) * ff_v_bpt_value_hj32_h_root_36_product) + (ff_r_bpt_value_hj32_h_root_36_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_36_product_successor. ff_h_bpt_value_hj32_h_root_36_product_successor + S (ff_s_bpt_value_hj32_h_root_36_product) = S ((S (S ff_i_bpt_value_hj32_h_root_36_product)) * ff_v_bpt_value_hj32_h_root_36_product)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_successor. ff_u_bpt_value_hj32_h_root_36_product = ff_q_bpt_value_hj32_h_root_36_product_successor * S ((S (S ff_i_bpt_value_hj32_h_root_36_product)) * ff_v_bpt_value_hj32_h_root_36_product) + (ff_s_bpt_value_hj32_h_root_36_product))) /\ ff_s_bpt_value_hj32_h_root_36_product = ff_r_bpt_value_hj32_h_root_36_product * ff_p_bpt_value_hj32_h_root_36_product))))))))) -> (((exists bcs_lower_gap_hj32_h_root_36_ceiling. bcs_lower_gap_hj32_h_root_36_ceiling + (36 * 36) = 6 * (e)) /\ exists bcs_upper_gap_hj32_h_root_36_ceiling. bcs_upper_gap_hj32_h_root_36_ceiling + S (6 * (e)) = (36 * 36) + 6)) -> (exists pa_b_hj32_h_root_36_h pa_c_hj32_h_root_36_h. ((forall pa_i_hj32_h_root_36_h_repeat. (exists pa_lt_hj32_h_root_36_h_repeat_bound. pa_lt_hj32_h_root_36_h_repeat_bound + S pa_i_hj32_h_root_36_h_repeat = 2 * 36 + 2) -> (((exists pa_h_hj32_h_root_36_h_repeat_decoded. pa_h_hj32_h_root_36_h_repeat_decoded + S (36 + 1) = S ((S (pa_i_hj32_h_root_36_h_repeat)) * pa_c_hj32_h_root_36_h)) /\ exists pa_q_hj32_h_root_36_h_repeat_decoded. pa_b_hj32_h_root_36_h = pa_q_hj32_h_root_36_h_repeat_decoded * S ((S (pa_i_hj32_h_root_36_h_repeat)) * pa_c_hj32_h_root_36_h) + (36 + 1)))) /\ (exists pa_u_hj32_h_root_36_h_product pa_v_hj32_h_root_36_h_product. ((((exists pa_h_hj32_h_root_36_h_product_start. pa_h_hj32_h_root_36_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_36_h_product)) /\ exists pa_q_hj32_h_root_36_h_product_start. pa_u_hj32_h_root_36_h_product = pa_q_hj32_h_root_36_h_product_start * S ((S (0)) * pa_v_hj32_h_root_36_h_product) + (1))) /\ ((((exists pa_h_hj32_h_root_36_h_product_terminal. pa_h_hj32_h_root_36_h_product_terminal + S (h) = S ((S (2 * 36 + 2)) * pa_v_hj32_h_root_36_h_product)) /\ exists pa_q_hj32_h_root_36_h_product_terminal. pa_u_hj32_h_root_36_h_product = pa_q_hj32_h_root_36_h_product_terminal * S ((S (2 * 36 + 2)) * pa_v_hj32_h_root_36_h_product) + (h))) /\ forall pa_i_hj32_h_root_36_h_product. (exists pa_lt_hj32_h_root_36_h_product_bound. pa_lt_hj32_h_root_36_h_product_bound + S pa_i_hj32_h_root_36_h_product = 2 * 36 + 2) -> exists pa_p_hj32_h_root_36_h_product pa_r_hj32_h_root_36_h_product pa_s_hj32_h_root_36_h_product. ((((exists pa_h_hj32_h_root_36_h_product_factor. pa_h_hj32_h_root_36_h_product_factor + S (pa_p_hj32_h_root_36_h_product) = S ((S (pa_i_hj32_h_root_36_h_product)) * pa_c_hj32_h_root_36_h)) /\ exists pa_q_hj32_h_root_36_h_product_factor. pa_b_hj32_h_root_36_h = pa_q_hj32_h_root_36_h_product_factor * S ((S (pa_i_hj32_h_root_36_h_product)) * pa_c_hj32_h_root_36_h) + (pa_p_hj32_h_root_36_h_product))) /\ ((((exists pa_h_hj32_h_root_36_h_product_partial. pa_h_hj32_h_root_36_h_product_partial + S (pa_r_hj32_h_root_36_h_product) = S ((S (pa_i_hj32_h_root_36_h_product)) * pa_v_hj32_h_root_36_h_product)) /\ exists pa_q_hj32_h_root_36_h_product_partial. pa_u_hj32_h_root_36_h_product = pa_q_hj32_h_root_36_h_product_partial * S ((S (pa_i_hj32_h_root_36_h_product)) * pa_v_hj32_h_root_36_h_product) + (pa_r_hj32_h_root_36_h_product))) /\ ((((exists pa_h_hj32_h_root_36_h_product_successor. pa_h_hj32_h_root_36_h_product_successor + S (pa_s_hj32_h_root_36_h_product) = S ((S (S pa_i_hj32_h_root_36_h_product)) * pa_v_hj32_h_root_36_h_product)) /\ exists pa_q_hj32_h_root_36_h_product_successor. pa_u_hj32_h_root_36_h_product = pa_q_hj32_h_root_36_h_product_successor * S ((S (S pa_i_hj32_h_root_36_h_product)) * pa_v_hj32_h_root_36_h_product) + (pa_s_hj32_h_root_36_h_product))) /\ pa_s_hj32_h_root_36_h_product = pa_r_hj32_h_root_36_h_product * pa_p_hj32_h_root_36_h_product)))))))) -> (exists pa_b_hj32_h_root_36_u pa_c_hj32_h_root_36_u. ((forall pa_i_hj32_h_root_36_u_repeat. (exists pa_lt_hj32_h_root_36_u_repeat_bound. pa_lt_hj32_h_root_36_u_repeat_bound + S pa_i_hj32_h_root_36_u_repeat = e) -> (((exists pa_h_hj32_h_root_36_u_repeat_decoded. pa_h_hj32_h_root_36_u_repeat_decoded + S (4) = S ((S (pa_i_hj32_h_root_36_u_repeat)) * pa_c_hj32_h_root_36_u)) /\ exists pa_q_hj32_h_root_36_u_repeat_decoded. pa_b_hj32_h_root_36_u = pa_q_hj32_h_root_36_u_repeat_decoded * S ((S (pa_i_hj32_h_root_36_u_repeat)) * pa_c_hj32_h_root_36_u) + (4)))) /\ (exists pa_u_hj32_h_root_36_u_product pa_v_hj32_h_root_36_u_product. ((((exists pa_h_hj32_h_root_36_u_product_start. pa_h_hj32_h_root_36_u_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_36_u_product)) /\ exists pa_q_hj32_h_root_36_u_product_start. pa_u_hj32_h_root_36_u_product = pa_q_hj32_h_root_36_u_product_start * S ((S (0)) * pa_v_hj32_h_root_36_u_product) + (1))) /\ ((((exists pa_h_hj32_h_root_36_u_product_terminal. pa_h_hj32_h_root_36_u_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_h_root_36_u_product)) /\ exists pa_q_hj32_h_root_36_u_product_terminal. pa_u_hj32_h_root_36_u_product = pa_q_hj32_h_root_36_u_product_terminal * S ((S (e)) * pa_v_hj32_h_root_36_u_product) + (u))) /\ forall pa_i_hj32_h_root_36_u_product. (exists pa_lt_hj32_h_root_36_u_product_bound. pa_lt_hj32_h_root_36_u_product_bound + S pa_i_hj32_h_root_36_u_product = e) -> exists pa_p_hj32_h_root_36_u_product pa_r_hj32_h_root_36_u_product pa_s_hj32_h_root_36_u_product. ((((exists pa_h_hj32_h_root_36_u_product_factor. pa_h_hj32_h_root_36_u_product_factor + S (pa_p_hj32_h_root_36_u_product) = S ((S (pa_i_hj32_h_root_36_u_product)) * pa_c_hj32_h_root_36_u)) /\ exists pa_q_hj32_h_root_36_u_product_factor. pa_b_hj32_h_root_36_u = pa_q_hj32_h_root_36_u_product_factor * S ((S (pa_i_hj32_h_root_36_u_product)) * pa_c_hj32_h_root_36_u) + (pa_p_hj32_h_root_36_u_product))) /\ ((((exists pa_h_hj32_h_root_36_u_product_partial. pa_h_hj32_h_root_36_u_product_partial + S (pa_r_hj32_h_root_36_u_product) = S ((S (pa_i_hj32_h_root_36_u_product)) * pa_v_hj32_h_root_36_u_product)) /\ exists pa_q_hj32_h_root_36_u_product_partial. pa_u_hj32_h_root_36_u_product = pa_q_hj32_h_root_36_u_product_partial * S ((S (pa_i_hj32_h_root_36_u_product)) * pa_v_hj32_h_root_36_u_product) + (pa_r_hj32_h_root_36_u_product))) /\ ((((exists pa_h_hj32_h_root_36_u_product_successor. pa_h_hj32_h_root_36_u_product_successor + S (pa_s_hj32_h_root_36_u_product) = S ((S (S pa_i_hj32_h_root_36_u_product)) * pa_v_hj32_h_root_36_u_product)) /\ exists pa_q_hj32_h_root_36_u_product_successor. pa_u_hj32_h_root_36_u_product = pa_q_hj32_h_root_36_u_product_successor * S ((S (S pa_i_hj32_h_root_36_u_product)) * pa_v_hj32_h_root_36_u_product) + (pa_s_hj32_h_root_36_u_product))) /\ pa_s_hj32_h_root_36_u_product = pa_r_hj32_h_root_36_u_product * pa_p_hj32_h_root_36_u_product)))))))) -> (exists bqb_le_gap_hj32_h_root_36_result. bqb_le_gap_hj32_h_root_36_result + (h) = (u))

Proof neighborhood

Direct theorem prerequisites

BT00WC bertrand_scaled_budget_root_36 BT00WE ceil_div_six_budget_of_scaled_le BT00WM pow_eleven_double_block_le_pow_four_odd_from_total BT00QV pow_mul_base BT009X pow_add BT00PY pow_base_monotone BT00SN pow_exponent_monotone_from_total BT00PV mul_le_mul BT000E le_refl BT000F le_trans BT0007 mul_add BT0008 mul_assoc BT0003 add_assoc

Direct theorem dependents

BT00WW bertrand_hj_base_window_thirty_two_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

244 script commands · 61 reading checkpoints · 45 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 (13)
bertrand scaled budget root 36ceil div six budget of scaled lepow eleven double block le pow four odd from totalpow mul basepow addpow base monotonepow exponent monotone from totalmul le mulle reflle transmul addmul assocadd assoc
01Fix variables and assumptionsL1–7

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

  1. L1
    intro e
  2. L2
    intro h
  3. L3
    intro u
  4. L4
    intro htotal
  5. L5
    intro hceiling
  6. L6
    intro hh
  7. L7
    intro hu
02Establish hh_routeL8–8

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

  1. L8
    have hh_route : Pow(37,2 · 37,h)Definitions: Pow(37,2 · 37,h)Original native command in the exact edition
03Establish hh_baseL9–10

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

  1. L9
    have hh_base : 36 + 1 = 37
  2. L10
    norm_num
04Establish hh_exponentL11–19

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

  1. L11
    have hh_exponent : 2 * 36 + 2 = 2 * 37
  2. L12
    norm_num
  3. L13
    rewrite <- hh_exponent
  4. L14
    rewrite <- hh_exponent
  5. L15
    rewrite <- hh_exponent
  6. L16
    rewrite <- hh_exponent
  7. L17
    rewrite <- hh_base
  8. L18
    rewrite <- hh_base
  9. L19
    exact hh
05Establish h36t_p44L20–23

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

  1. L20
    have h36t_p44 : ∃ hj32_local_value_h36t_p44. Pow(44,2 · 37,hj32_local_value_h36t_p44)Definitions: Pow(44,2 · 37,hj32_local_value_h36t_p44)Original native command in the exact edition
  2. L21
    specialize htotal 44
  3. L22
    specialize htotal 2 * 37
  4. L23
    exact htotal
06Separate the logical casesL24–24

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

  1. L24
    cases h36t_p44
07Establish h36t_baseL25–25

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

  1. L25
    have h36t_base : Lt(36,44)Definitions: Lt(36,44)Original native command in the exact edition
08Construct an explicit witnessL26–26

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

  1. L26
    exists 7
09Calculate and transport equalitiesL27–27

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

  1. L27
    norm_num
10Establish h36t_to_44L28–37

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

  1. L28
    have h36t_to_44 : Le(h,x)Definitions: Le(h,x)Original native command in the exact edition
  2. L29
    specialize pow_base_monotone 37
  3. L30
    specialize pow_base_monotone 44
  4. L31
    specialize pow_base_monotone 2 * 37
  5. L32
    specialize pow_base_monotone h
  6. L33
    specialize pow_base_monotone x
  7. L34
    apply pow_base_monotone
  8. L35
    exact h36t_base
  9. L36
    exact hh_route
  10. L37
    exact h36t_p44_witness
11Establish h36t_p4_expL38–41

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

  1. L38
    have h36t_p4_exp : ∃ hj32_local_value_h36t_p4_exp. Pow(4,2 · 37,hj32_local_value_h36t_p4_exp)Definitions: Pow(4,2 · 37,hj32_local_value_h36t_p4_exp)Original native command in the exact edition
  2. L39
    specialize htotal 4
  3. L40
    specialize htotal 2 * 37
  4. L41
    exact htotal
12Separate the logical casesL42–42

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

  1. L42
    cases h36t_p4_exp
13Establish h36t_p11_expL43–46

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

  1. L43
    have h36t_p11_exp : ∃ hj32_local_value_h36t_p11_exp. Pow(11,2 · 37,hj32_local_value_h36t_p11_exp)Definitions: Pow(11,2 · 37,hj32_local_value_h36t_p11_exp)Original native command in the exact edition
  2. L44
    specialize htotal 11
  3. L45
    specialize htotal 2 * 37
  4. L46
    exact htotal
14Separate the logical casesL47–47

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

  1. L47
    cases h36t_p11_exp
15Establish h36t_p44_product_graphL48–48

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

  1. L48
    have h36t_p44_product_graph : Pow(4 · 11,2 · 37,x)Definitions: Pow(4 · 11,2 · 37,x)Original native command in the exact edition
16Establish h36t_p44_product_baseL49–53

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

  1. L49
    have h36t_p44_product_base : 4 * 11 = 44
  2. L50
    norm_num
  3. L51
    rewrite h36t_p44_product_base
  4. L52
    rewrite h36t_p44_product_base
  5. L53
    exact h36t_p44_witness
17Establish h36t_p44_productL54–63

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

  1. L54
    have h36t_p44_product : x = x1 * x2
  2. L55
    specialize pow_mul_base 4
  3. L56
    specialize pow_mul_base 11
  4. L57
    specialize pow_mul_base 2 * 37
  5. L58
    specialize pow_mul_base x1
  6. L59
    specialize pow_mul_base x2
  7. L60
    specialize pow_mul_base x
  8. L61
    apply pow_mul_base
  9. L62
    exact h36t_p4_exp_witness
  10. L63
    exact h36t_p11_exp_witness
18Use earlier factsL64–64

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

  1. L64
    exact h36t_p44_product_graph
19Establish h36t_p4_tailL65–68

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

  1. L65
    have h36t_p4_tail : ∃ hj32_local_value_h36t_p4_tail. Pow(4,2 · (5 · 13),hj32_local_value_h36t_p4_tail)Definitions: Pow(4,2 · (5 · 13),hj32_local_value_h36t_p4_tail)Original native command in the exact edition
  2. L66
    specialize htotal 4
  3. L67
    specialize htotal 2 * (5 * 13)
  4. L68
    exact htotal
20Separate the logical casesL69–69

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

  1. L69
    cases h36t_p4_tail
21Establish h36t_tail_powerL70–70

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

  1. L70
    have h36t_tail_power : Pow(4,14 · 9 + 3 + 1,x3)Definitions: Pow(4,14 · 9 + 3 + 1,x3)Original native command in the exact edition
22Establish h36t_tail_exponentL71–71

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

  1. L71
    have h36t_tail_exponent : (14 * 9 + 3) + 1 = 2 * (5 * 13)
23Establish h36t_tail_leftL72–72

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

  1. L72
    have h36t_tail_left : (14 * 9 + 3) + 1 = 2 * (7 * 9 + 2)
24Establish h36t_tail_assocL73–78

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

  1. L73
    have h36t_tail_assoc : (14 * 9 + 3) + 1 = 14 * 9 + (3 + 1)
  2. L74
    specialize add_assoc (14 * 9)
  3. L75
    specialize add_assoc 3
  4. L76
    specialize add_assoc 1
  5. L77
    apply add_assoc
  6. L78
    rewrite h36t_tail_assoc
25Establish h36t_fourL79–81

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

  1. L79
    have h36t_four : 3 + 1 = 2 * 2
  2. L80
    norm_num
  3. L81
    rewrite h36t_four
26Establish h36t_fourteenL82–84

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

  1. L82
    have h36t_fourteen : 14 = 2 * 7
  2. L83
    norm_num
  3. L84
    rewrite h36t_fourteen
27Establish h36t_assoc_mulL85–90

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

  1. L85
    have h36t_assoc_mul : (2 * 7) * 9 = 2 * (7 * 9)
  2. L86
    specialize mul_assoc 2
  3. L87
    specialize mul_assoc 7
  4. L88
    specialize mul_assoc 9
  5. L89
    apply mul_assoc
  6. L90
    rewrite h36t_assoc_mul
28Establish h36t_factorL91–97

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

  1. L91
    have h36t_factor : 2 * (7 * 9 + 2) = 2 * (7 * 9) + 2 * 2
  2. L92
    specialize mul_add 2
  3. L93
    specialize mul_add (7 * 9)
  4. L94
    specialize mul_add 2
  5. L95
    apply mul_add
  6. L96
    rewrite <- h36t_factor
  7. L97
    refl
29Establish h36t_tail_rightL98–98

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

  1. L98
    have h36t_tail_right : 2 * (7 * 9 + 2) = 2 * (5 * 13)
30Establish h36t_insideL99–108

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

  1. L99
    have h36t_inside : 7 * 9 + 2 = 5 * 13
  2. L100
    norm_num
  3. L101
    rewrite h36t_inside
  4. L102
    refl
  5. L103
    trans 2 * (7 * 9 + 2)
  6. L104
    exact h36t_tail_left
  7. L105
    exact h36t_tail_right
  8. L106
    rewrite h36t_tail_exponent
  9. L107
    rewrite h36t_tail_exponent
  10. L108
    rewrite h36t_tail_exponent
31Calculate and transport equalitiesL109–109

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

  1. L109
    rewrite h36t_tail_exponent
32Use earlier factsL110–110

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

  1. L110
    exact h36t_p4_tail_witness
33Establish h36t_parityL111–111

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

  1. L111
    have h36t_parity : 7 * 37 = 2 * (14 * 9 + 3) + 1
34Establish h36t_leftL112–112

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

  1. L112
    have h36t_left : 7 * 37 = 28 * 9 + 7
35Establish h36t_rootL113–115

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

  1. L113
    have h36t_root : 37 = 4 * 9 + 1
  2. L114
    norm_num
  3. L115
    rewrite h36t_root
36Establish h36t_left_distribL116–121

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

  1. L116
    have h36t_left_distrib : 7 * (4 * 9 + 1) = 7 * (4 * 9) + 7 * 1
  2. L117
    specialize mul_add 7
  3. L118
    specialize mul_add (4 * 9)
  4. L119
    specialize mul_add 1
  5. L120
    apply mul_add
  6. L121
    rewrite h36t_left_distrib
37Establish h36t_left_assocL122–128

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

  1. L122
    have h36t_left_assoc : 7 * (4 * 9) = (7 * 4) * 9
  2. L123
    symm
  3. L124
    specialize mul_assoc 7
  4. L125
    specialize mul_assoc 4
  5. L126
    specialize mul_assoc 9
  6. L127
    apply mul_assoc
  7. L128
    rewrite h36t_left_assoc
38Establish h36t_twenty_eightL129–131

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

  1. L129
    have h36t_twenty_eight : 7 * 4 = 28
  2. L130
    norm_num
  3. L131
    rewrite h36t_twenty_eight
39Establish h36t_sevenL132–135

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

  1. L132
    have h36t_seven : 7 * 1 = 7
  2. L133
    norm_num
  3. L134
    rewrite h36t_seven
  4. L135
    refl
40Establish h36t_rightL136–136

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

  1. L136
    have h36t_right : 2 * (14 * 9 + 3) + 1 = 28 * 9 + 7
41Establish h36t_right_distribL137–142

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

  1. L137
    have h36t_right_distrib : 2 * (14 * 9 + 3) = 2 * (14 * 9) + 2 * 3
  2. L138
    specialize mul_add 2
  3. L139
    specialize mul_add (14 * 9)
  4. L140
    specialize mul_add 3
  5. L141
    apply mul_add
  6. L142
    rewrite h36t_right_distrib
42Establish h36t_right_assocL143–149

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

  1. L143
    have h36t_right_assoc : 2 * (14 * 9) = (2 * 14) * 9
  2. L144
    symm
  3. L145
    specialize mul_assoc 2
  4. L146
    specialize mul_assoc 14
  5. L147
    specialize mul_assoc 9
  6. L148
    apply mul_assoc
  7. L149
    rewrite h36t_right_assoc
43Establish h36t_right_twenty_eightL150–152

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

  1. L150
    have h36t_right_twenty_eight : 2 * 14 = 28
  2. L151
    norm_num
  3. L152
    rewrite h36t_right_twenty_eight
44Establish h36t_right_addL153–158

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

  1. L153
    have h36t_right_add : (28 * 9 + 2 * 3) + 1 = 28 * 9 + (2 * 3 + 1)
  2. L154
    specialize add_assoc (28 * 9)
  3. L155
    specialize add_assoc (2 * 3)
  4. L156
    specialize add_assoc 1
  5. L157
    apply add_assoc
  6. L158
    rewrite h36t_right_add
45Establish h36t_right_sevenL159–166

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

  1. L159
    have h36t_right_seven : 2 * 3 + 1 = 7
  2. L160
    norm_num
  3. L161
    rewrite h36t_right_seven
  4. L162
    refl
  5. L163
    trans 28 * 9 + 7
  6. L164
    exact h36t_left
  7. L165
    symm
  8. L166
    exact h36t_right
46Establish h36t_eleven_boundL167–176

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow eleven double block le pow four odd from total.

  1. L167
    have h36t_eleven_bound : Le(x2,x3)Definitions: Le(x2,x3)Original native command in the exact edition
  2. L168
    specialize pow_eleven_double_block_le_pow_four_odd_from_total 37
  3. L169
    specialize pow_eleven_double_block_le_pow_four_odd_from_total (14 * 9 + 3)
  4. L170
    specialize pow_eleven_double_block_le_pow_four_odd_from_total x2
  5. L171
    specialize pow_eleven_double_block_le_pow_four_odd_from_total x3
  6. L172
    apply pow_eleven_double_block_le_pow_four_odd_from_total
  7. L173
    exact htotal
  8. L174
    exact h36t_parity
  9. L175
    exact h36t_p11_exp_witness
  10. L176
    exact h36t_tail_power
47Establish h36t_four_reflL177–179

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

  1. L177
    have h36t_four_refl : Le(x1,x1)Definitions: Le(x1,x1)Original native command in the exact edition
  2. L178
    specialize le_refl x1
  3. L179
    exact le_refl
48Establish h36t_product_boundL180–187

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

  1. L180
    have h36t_product_bound : Le(x1 · x2,x1 · x3)Definitions: Le(x1 · x2,x1 · x3)Original native command in the exact edition
  2. L181
    specialize mul_le_mul x1
  3. L182
    specialize mul_le_mul x1
  4. L183
    specialize mul_le_mul x2
  5. L184
    specialize mul_le_mul x3
  6. L185
    apply mul_le_mul
  7. L186
    exact h36t_four_refl
  8. L187
    exact h36t_eleven_bound
49Establish h36t_p4_budgetL188–191

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

  1. L188
    have h36t_p4_budget : ∃ hj32_local_value_h36t_p4_budget. Pow(4,2 · 37 + 2 · (5 · 13),hj32_local_value_h36t_p4_budget)Definitions: Pow(4,2 · 37 + 2 · (5 · 13),hj32_local_value_h36t_p4_budget)Original native command in the exact edition
  2. L189
    specialize htotal 4
  3. L190
    specialize htotal 2 * 37 + 2 * (5 * 13)
  4. L191
    exact htotal
50Separate the logical casesL192–192

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

  1. L192
    cases h36t_p4_budget
51Establish h36t_budget_productL193–202

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

  1. L193
    have h36t_budget_product : x4 = x1 * x3
  2. L194
    specialize pow_add 4
  3. L195
    specialize pow_add 2 * 37
  4. L196
    specialize pow_add 2 * (5 * 13)
  5. L197
    specialize pow_add 2 * 37 + 2 * (5 * 13)
  6. L198
    specialize pow_add x1
  7. L199
    specialize pow_add x3
  8. L200
    specialize pow_add x4
  9. L201
    apply pow_add
  10. L202
    refl
52Use earlier factsL203–205

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

  1. L203
    exact h36t_p4_exp_witness
  2. L204
    exact h36t_p4_tail_witness
  3. L205
    exact h36t_p4_budget_witness
53Calculate and transport equalitiesL206–207

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

  1. L206
    rewrite <- h36t_p44_product at h36t_product_bound
  2. L207
    rewrite <- h36t_budget_product at h36t_product_bound
54Establish h36t_to_budgetL208–214

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

  1. L208
    have h36t_to_budget : Le(h,x4)Definitions: Le(h,x4)Original native command in the exact edition
  2. L209
    specialize le_trans h
  3. L210
    specialize le_trans x
  4. L211
    specialize le_trans x4
  5. L212
    apply le_trans
  6. L213
    exact h36t_to_44
  7. L214
    exact h36t_product_bound
55Establish hscaledL215–216

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

  1. L215
    have hscaled : Le(6 · (2 · 37 + 2 · (5 · 13)),36 · 36)Definitions: Le(6 · (2 · 37 + 2 · (5 · 13)),36 · 36)Original native command in the exact edition
  2. L216
    apply bertrand_scaled_budget_root_36
56Establish hbudget_exponentL217–223

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply ceil div six budget of scaled le.

  1. L217
    have hbudget_exponent : Le(2 · 37 + 2 · (5 · 13),e)Definitions: Le(2 · 37 + 2 · (5 · 13),e)Original native command in the exact edition
  2. L218
    specialize ceil_div_six_budget_of_scaled_le (36 * 36)
  3. L219
    specialize ceil_div_six_budget_of_scaled_le (2 * 37 + 2 * (5 * 13))
  4. L220
    specialize ceil_div_six_budget_of_scaled_le e
  5. L221
    apply ceil_div_six_budget_of_scaled_le
  6. L222
    exact hceiling
  7. L223
    exact hscaled
57Establish h36_budget_growthL224–231

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

  1. L224
    have h36_budget_growth : Le(x4,u)Definitions: Le(x4,u)Original native command in the exact edition
  2. L225
    specialize pow_exponent_monotone_from_total 4
  3. L226
    specialize pow_exponent_monotone_from_total 2 * 37 + 2 * (5 * 13)
  4. L227
    specialize pow_exponent_monotone_from_total e
  5. L228
    specialize pow_exponent_monotone_from_total x4
  6. L229
    specialize pow_exponent_monotone_from_total u
  7. L230
    apply pow_exponent_monotone_from_total
  8. L231
    exact htotal
58Construct an explicit witnessL232–232

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

  1. L232
    exists 3
59Calculate and transport equalitiesL233–233

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

  1. L233
    norm_num
60Use earlier factsL234–236

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

  1. L234
    exact hbudget_exponent
  2. L235
    exact h36t_p4_budget_witness
  3. L236
    exact hu
61Establish h36_resultL237–244

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

  1. L237
    have h36_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L238
    specialize le_trans h
  3. L239
    specialize le_trans x4
  4. L240
    specialize le_trans u
  5. L241
    apply le_trans
  6. L242
    exact h36t_to_budget
  7. L243
    exact h36_budget_growth
  8. L244
    exact h36_result

Library-wide reading audit

Original defined command ledger · 244 lines
  1. 0001intro e
  2. 0002intro h
  3. 0003intro u
  4. 0004intro htotal
  5. 0005intro hceiling
  6. 0006intro hh
  7. 0007intro hu
  8. 0008have hh_route : Pow(37,2 · 37,h)
    Exact native replay linehave hh_route : exists pa_b_hj32_h_36_route pa_c_hj32_h_36_route. ((forall pa_i_hj32_h_36_route_repeat. (exists pa_lt_hj32_h_36_route_repeat_bound. pa_lt_hj32_h_36_route_repeat_bound + S pa_i_hj32_h_36_route_repeat = 2 * 37) -> (((exists pa_h_hj32_h_36_route_repeat_decoded. pa_h_hj32_h_36_route_repeat_decoded + S (37) = S ((S (pa_i_hj32_h_36_route_repeat)) * pa_c_hj32_h_36_route)) /\ exists pa_q_hj32_h_36_route_repeat_decoded. pa_b_hj32_h_36_route = pa_q_hj32_h_36_route_repeat_decoded * S ((S (pa_i_hj32_h_36_route_repeat)) * pa_c_hj32_h_36_route) + (37)))) /\ (exists pa_u_hj32_h_36_route_product pa_v_hj32_h_36_route_product. ((((exists pa_h_hj32_h_36_route_product_start. pa_h_hj32_h_36_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_36_route_product)) /\ exists pa_q_hj32_h_36_route_product_start. pa_u_hj32_h_36_route_product = pa_q_hj32_h_36_route_product_start * S ((S (0)) * pa_v_hj32_h_36_route_product) + (1))) /\ ((((exists pa_h_hj32_h_36_route_product_terminal. pa_h_hj32_h_36_route_product_terminal + S (h) = S ((S (2 * 37)) * pa_v_hj32_h_36_route_product)) /\ exists pa_q_hj32_h_36_route_product_terminal. pa_u_hj32_h_36_route_product = pa_q_hj32_h_36_route_product_terminal * S ((S (2 * 37)) * pa_v_hj32_h_36_route_product) + (h))) /\ forall pa_i_hj32_h_36_route_product. (exists pa_lt_hj32_h_36_route_product_bound. pa_lt_hj32_h_36_route_product_bound + S pa_i_hj32_h_36_route_product = 2 * 37) -> exists pa_p_hj32_h_36_route_product pa_r_hj32_h_36_route_product pa_s_hj32_h_36_route_product. ((((exists pa_h_hj32_h_36_route_product_factor. pa_h_hj32_h_36_route_product_factor + S (pa_p_hj32_h_36_route_product) = S ((S (pa_i_hj32_h_36_route_product)) * pa_c_hj32_h_36_route)) /\ exists pa_q_hj32_h_36_route_product_factor. pa_b_hj32_h_36_route = pa_q_hj32_h_36_route_product_factor * S ((S (pa_i_hj32_h_36_route_product)) * pa_c_hj32_h_36_route) + (pa_p_hj32_h_36_route_product))) /\ ((((exists pa_h_hj32_h_36_route_product_partial. pa_h_hj32_h_36_route_product_partial + S (pa_r_hj32_h_36_route_product) = S ((S (pa_i_hj32_h_36_route_product)) * pa_v_hj32_h_36_route_product)) /\ exists pa_q_hj32_h_36_route_product_partial. pa_u_hj32_h_36_route_product = pa_q_hj32_h_36_route_product_partial * S ((S (pa_i_hj32_h_36_route_product)) * pa_v_hj32_h_36_route_product) + (pa_r_hj32_h_36_route_product))) /\ ((((exists pa_h_hj32_h_36_route_product_successor. pa_h_hj32_h_36_route_product_successor + S (pa_s_hj32_h_36_route_product) = S ((S (S pa_i_hj32_h_36_route_product)) * pa_v_hj32_h_36_route_product)) /\ exists pa_q_hj32_h_36_route_product_successor. pa_u_hj32_h_36_route_product = pa_q_hj32_h_36_route_product_successor * S ((S (S pa_i_hj32_h_36_route_product)) * pa_v_hj32_h_36_route_product) + (pa_s_hj32_h_36_route_product))) /\ pa_s_hj32_h_36_route_product = pa_r_hj32_h_36_route_product * pa_p_hj32_h_36_route_product)))))))
  9. 0009have hh_base : 36 + 1 = 37
  10. 0010norm_num
  11. 0011have hh_exponent : 2 * 36 + 2 = 2 * 37
  12. 0012norm_num
  13. 0013rewrite <- hh_exponent
  14. 0014rewrite <- hh_exponent
  15. 0015rewrite <- hh_exponent
  16. 0016rewrite <- hh_exponent
  17. 0017rewrite <- hh_base
  18. 0018rewrite <- hh_base
  19. 0019exact hh
  20. 0020have h36t_p44 : ∃ hj32_local_value_h36t_p44. Pow(44,2 · 37,hj32_local_value_h36t_p44)
    Exact native replay linehave h36t_p44 : exists hj32_local_value_h36t_p44. (exists pa_b_hj32_local_total_h36t_p44 pa_c_hj32_local_total_h36t_p44. ((forall pa_i_hj32_local_total_h36t_p44_repeat. (exists pa_lt_hj32_local_total_h36t_p44_repeat_bound. pa_lt_hj32_local_total_h36t_p44_repeat_bound + S pa_i_hj32_local_total_h36t_p44_repeat = 2 * 37) -> (((exists pa_h_hj32_local_total_h36t_p44_repeat_decoded. pa_h_hj32_local_total_h36t_p44_repeat_decoded + S (44) = S ((S (pa_i_hj32_local_total_h36t_p44_repeat)) * pa_c_hj32_local_total_h36t_p44)) /\ exists pa_q_hj32_local_total_h36t_p44_repeat_decoded. pa_b_hj32_local_total_h36t_p44 = pa_q_hj32_local_total_h36t_p44_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p44_repeat)) * pa_c_hj32_local_total_h36t_p44) + (44)))) /\ (exists pa_u_hj32_local_total_h36t_p44_product pa_v_hj32_local_total_h36t_p44_product. ((((exists pa_h_hj32_local_total_h36t_p44_product_start. pa_h_hj32_local_total_h36t_p44_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p44_product)) /\ exists pa_q_hj32_local_total_h36t_p44_product_start. pa_u_hj32_local_total_h36t_p44_product = pa_q_hj32_local_total_h36t_p44_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p44_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p44_product_terminal. pa_h_hj32_local_total_h36t_p44_product_terminal + S (hj32_local_value_h36t_p44) = S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p44_product)) /\ exists pa_q_hj32_local_total_h36t_p44_product_terminal. pa_u_hj32_local_total_h36t_p44_product = pa_q_hj32_local_total_h36t_p44_product_terminal * S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p44_product) + (hj32_local_value_h36t_p44))) /\ forall pa_i_hj32_local_total_h36t_p44_product. (exists pa_lt_hj32_local_total_h36t_p44_product_bound. pa_lt_hj32_local_total_h36t_p44_product_bound + S pa_i_hj32_local_total_h36t_p44_product = 2 * 37) -> exists pa_p_hj32_local_total_h36t_p44_product pa_r_hj32_local_total_h36t_p44_product pa_s_hj32_local_total_h36t_p44_product. ((((exists pa_h_hj32_local_total_h36t_p44_product_factor. pa_h_hj32_local_total_h36t_p44_product_factor + S (pa_p_hj32_local_total_h36t_p44_product) = S ((S (pa_i_hj32_local_total_h36t_p44_product)) * pa_c_hj32_local_total_h36t_p44)) /\ exists pa_q_hj32_local_total_h36t_p44_product_factor. pa_b_hj32_local_total_h36t_p44 = pa_q_hj32_local_total_h36t_p44_product_factor * S ((S (pa_i_hj32_local_total_h36t_p44_product)) * pa_c_hj32_local_total_h36t_p44) + (pa_p_hj32_local_total_h36t_p44_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p44_product_partial. pa_h_hj32_local_total_h36t_p44_product_partial + S (pa_r_hj32_local_total_h36t_p44_product) = S ((S (pa_i_hj32_local_total_h36t_p44_product)) * pa_v_hj32_local_total_h36t_p44_product)) /\ exists pa_q_hj32_local_total_h36t_p44_product_partial. pa_u_hj32_local_total_h36t_p44_product = pa_q_hj32_local_total_h36t_p44_product_partial * S ((S (pa_i_hj32_local_total_h36t_p44_product)) * pa_v_hj32_local_total_h36t_p44_product) + (pa_r_hj32_local_total_h36t_p44_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p44_product_successor. pa_h_hj32_local_total_h36t_p44_product_successor + S (pa_s_hj32_local_total_h36t_p44_product) = S ((S (S pa_i_hj32_local_total_h36t_p44_product)) * pa_v_hj32_local_total_h36t_p44_product)) /\ exists pa_q_hj32_local_total_h36t_p44_product_successor. pa_u_hj32_local_total_h36t_p44_product = pa_q_hj32_local_total_h36t_p44_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p44_product)) * pa_v_hj32_local_total_h36t_p44_product) + (pa_s_hj32_local_total_h36t_p44_product))) /\ pa_s_hj32_local_total_h36t_p44_product = pa_r_hj32_local_total_h36t_p44_product * pa_p_hj32_local_total_h36t_p44_product))))))))
  21. 0021specialize htotal 44
  22. 0022specialize htotal 2 * 37
  23. 0023exact htotal
  24. 0024cases h36t_p44
  25. 0025have h36t_base : Lt(36,44)
    Exact native replay linehave h36t_base : exists bqb_le_gap_hj32_h36t_base. bqb_le_gap_hj32_h36t_base + (37) = (44)
  26. 0026exists 7
  27. 0027norm_num
  28. 0028have h36t_to_44 : Le(h,x)
    Exact native replay linehave h36t_to_44 : exists bqb_le_gap_hj32_local_base_bound_h36t_to_44. bqb_le_gap_hj32_local_base_bound_h36t_to_44 + (h) = (x)
  29. 0029specialize pow_base_monotone 37
  30. 0030specialize pow_base_monotone 44
  31. 0031specialize pow_base_monotone 2 * 37
  32. 0032specialize pow_base_monotone h
  33. 0033specialize pow_base_monotone x
  34. 0034apply pow_base_monotone
  35. 0035exact h36t_base
  36. 0036exact hh_route
  37. 0037exact h36t_p44_witness
  38. 0038have h36t_p4_exp : ∃ hj32_local_value_h36t_p4_exp. Pow(4,2 · 37,hj32_local_value_h36t_p4_exp)
    Exact native replay linehave h36t_p4_exp : exists hj32_local_value_h36t_p4_exp. (exists pa_b_hj32_local_total_h36t_p4_exp pa_c_hj32_local_total_h36t_p4_exp. ((forall pa_i_hj32_local_total_h36t_p4_exp_repeat. (exists pa_lt_hj32_local_total_h36t_p4_exp_repeat_bound. pa_lt_hj32_local_total_h36t_p4_exp_repeat_bound + S pa_i_hj32_local_total_h36t_p4_exp_repeat = 2 * 37) -> (((exists pa_h_hj32_local_total_h36t_p4_exp_repeat_decoded. pa_h_hj32_local_total_h36t_p4_exp_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h36t_p4_exp_repeat)) * pa_c_hj32_local_total_h36t_p4_exp)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_repeat_decoded. pa_b_hj32_local_total_h36t_p4_exp = pa_q_hj32_local_total_h36t_p4_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p4_exp_repeat)) * pa_c_hj32_local_total_h36t_p4_exp) + (4)))) /\ (exists pa_u_hj32_local_total_h36t_p4_exp_product pa_v_hj32_local_total_h36t_p4_exp_product. ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_start. pa_h_hj32_local_total_h36t_p4_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_start. pa_u_hj32_local_total_h36t_p4_exp_product = pa_q_hj32_local_total_h36t_p4_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p4_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_terminal. pa_h_hj32_local_total_h36t_p4_exp_product_terminal + S (hj32_local_value_h36t_p4_exp) = S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_terminal. pa_u_hj32_local_total_h36t_p4_exp_product = pa_q_hj32_local_total_h36t_p4_exp_product_terminal * S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p4_exp_product) + (hj32_local_value_h36t_p4_exp))) /\ forall pa_i_hj32_local_total_h36t_p4_exp_product. (exists pa_lt_hj32_local_total_h36t_p4_exp_product_bound. pa_lt_hj32_local_total_h36t_p4_exp_product_bound + S pa_i_hj32_local_total_h36t_p4_exp_product = 2 * 37) -> exists pa_p_hj32_local_total_h36t_p4_exp_product pa_r_hj32_local_total_h36t_p4_exp_product pa_s_hj32_local_total_h36t_p4_exp_product. ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_factor. pa_h_hj32_local_total_h36t_p4_exp_product_factor + S (pa_p_hj32_local_total_h36t_p4_exp_product) = S ((S (pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_c_hj32_local_total_h36t_p4_exp)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_factor. pa_b_hj32_local_total_h36t_p4_exp = pa_q_hj32_local_total_h36t_p4_exp_product_factor * S ((S (pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_c_hj32_local_total_h36t_p4_exp) + (pa_p_hj32_local_total_h36t_p4_exp_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_partial. pa_h_hj32_local_total_h36t_p4_exp_product_partial + S (pa_r_hj32_local_total_h36t_p4_exp_product) = S ((S (pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_v_hj32_local_total_h36t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_partial. pa_u_hj32_local_total_h36t_p4_exp_product = pa_q_hj32_local_total_h36t_p4_exp_product_partial * S ((S (pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_v_hj32_local_total_h36t_p4_exp_product) + (pa_r_hj32_local_total_h36t_p4_exp_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_successor. pa_h_hj32_local_total_h36t_p4_exp_product_successor + S (pa_s_hj32_local_total_h36t_p4_exp_product) = S ((S (S pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_v_hj32_local_total_h36t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_successor. pa_u_hj32_local_total_h36t_p4_exp_product = pa_q_hj32_local_total_h36t_p4_exp_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_v_hj32_local_total_h36t_p4_exp_product) + (pa_s_hj32_local_total_h36t_p4_exp_product))) /\ pa_s_hj32_local_total_h36t_p4_exp_product = pa_r_hj32_local_total_h36t_p4_exp_product * pa_p_hj32_local_total_h36t_p4_exp_product))))))))
  39. 0039specialize htotal 4
  40. 0040specialize htotal 2 * 37
  41. 0041exact htotal
  42. 0042cases h36t_p4_exp
  43. 0043have h36t_p11_exp : ∃ hj32_local_value_h36t_p11_exp. Pow(11,2 · 37,hj32_local_value_h36t_p11_exp)
    Exact native replay linehave h36t_p11_exp : exists hj32_local_value_h36t_p11_exp. (exists pa_b_hj32_local_total_h36t_p11_exp pa_c_hj32_local_total_h36t_p11_exp. ((forall pa_i_hj32_local_total_h36t_p11_exp_repeat. (exists pa_lt_hj32_local_total_h36t_p11_exp_repeat_bound. pa_lt_hj32_local_total_h36t_p11_exp_repeat_bound + S pa_i_hj32_local_total_h36t_p11_exp_repeat = 2 * 37) -> (((exists pa_h_hj32_local_total_h36t_p11_exp_repeat_decoded. pa_h_hj32_local_total_h36t_p11_exp_repeat_decoded + S (11) = S ((S (pa_i_hj32_local_total_h36t_p11_exp_repeat)) * pa_c_hj32_local_total_h36t_p11_exp)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_repeat_decoded. pa_b_hj32_local_total_h36t_p11_exp = pa_q_hj32_local_total_h36t_p11_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p11_exp_repeat)) * pa_c_hj32_local_total_h36t_p11_exp) + (11)))) /\ (exists pa_u_hj32_local_total_h36t_p11_exp_product pa_v_hj32_local_total_h36t_p11_exp_product. ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_start. pa_h_hj32_local_total_h36t_p11_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_start. pa_u_hj32_local_total_h36t_p11_exp_product = pa_q_hj32_local_total_h36t_p11_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p11_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_terminal. pa_h_hj32_local_total_h36t_p11_exp_product_terminal + S (hj32_local_value_h36t_p11_exp) = S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_terminal. pa_u_hj32_local_total_h36t_p11_exp_product = pa_q_hj32_local_total_h36t_p11_exp_product_terminal * S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p11_exp_product) + (hj32_local_value_h36t_p11_exp))) /\ forall pa_i_hj32_local_total_h36t_p11_exp_product. (exists pa_lt_hj32_local_total_h36t_p11_exp_product_bound. pa_lt_hj32_local_total_h36t_p11_exp_product_bound + S pa_i_hj32_local_total_h36t_p11_exp_product = 2 * 37) -> exists pa_p_hj32_local_total_h36t_p11_exp_product pa_r_hj32_local_total_h36t_p11_exp_product pa_s_hj32_local_total_h36t_p11_exp_product. ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_factor. pa_h_hj32_local_total_h36t_p11_exp_product_factor + S (pa_p_hj32_local_total_h36t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_c_hj32_local_total_h36t_p11_exp)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_factor. pa_b_hj32_local_total_h36t_p11_exp = pa_q_hj32_local_total_h36t_p11_exp_product_factor * S ((S (pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_c_hj32_local_total_h36t_p11_exp) + (pa_p_hj32_local_total_h36t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_partial. pa_h_hj32_local_total_h36t_p11_exp_product_partial + S (pa_r_hj32_local_total_h36t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_v_hj32_local_total_h36t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_partial. pa_u_hj32_local_total_h36t_p11_exp_product = pa_q_hj32_local_total_h36t_p11_exp_product_partial * S ((S (pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_v_hj32_local_total_h36t_p11_exp_product) + (pa_r_hj32_local_total_h36t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_successor. pa_h_hj32_local_total_h36t_p11_exp_product_successor + S (pa_s_hj32_local_total_h36t_p11_exp_product) = S ((S (S pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_v_hj32_local_total_h36t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_successor. pa_u_hj32_local_total_h36t_p11_exp_product = pa_q_hj32_local_total_h36t_p11_exp_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_v_hj32_local_total_h36t_p11_exp_product) + (pa_s_hj32_local_total_h36t_p11_exp_product))) /\ pa_s_hj32_local_total_h36t_p11_exp_product = pa_r_hj32_local_total_h36t_p11_exp_product * pa_p_hj32_local_total_h36t_p11_exp_product))))))))
  44. 0044specialize htotal 11
  45. 0045specialize htotal 2 * 37
  46. 0046exact htotal
  47. 0047cases h36t_p11_exp
  48. 0048have h36t_p44_product_graph : Pow(4 · 11,2 · 37,x)
    Exact native replay linehave h36t_p44_product_graph : exists pa_b_hj32_local_product_h36t_p44_product pa_c_hj32_local_product_h36t_p44_product. ((forall pa_i_hj32_local_product_h36t_p44_product_repeat. (exists pa_lt_hj32_local_product_h36t_p44_product_repeat_bound. pa_lt_hj32_local_product_h36t_p44_product_repeat_bound + S pa_i_hj32_local_product_h36t_p44_product_repeat = 2 * 37) -> (((exists pa_h_hj32_local_product_h36t_p44_product_repeat_decoded. pa_h_hj32_local_product_h36t_p44_product_repeat_decoded + S (4 * 11) = S ((S (pa_i_hj32_local_product_h36t_p44_product_repeat)) * pa_c_hj32_local_product_h36t_p44_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_repeat_decoded. pa_b_hj32_local_product_h36t_p44_product = pa_q_hj32_local_product_h36t_p44_product_repeat_decoded * S ((S (pa_i_hj32_local_product_h36t_p44_product_repeat)) * pa_c_hj32_local_product_h36t_p44_product) + (4 * 11)))) /\ (exists pa_u_hj32_local_product_h36t_p44_product_product pa_v_hj32_local_product_h36t_p44_product_product. ((((exists pa_h_hj32_local_product_h36t_p44_product_product_start. pa_h_hj32_local_product_h36t_p44_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_h36t_p44_product_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_start. pa_u_hj32_local_product_h36t_p44_product_product = pa_q_hj32_local_product_h36t_p44_product_product_start * S ((S (0)) * pa_v_hj32_local_product_h36t_p44_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_h36t_p44_product_product_terminal. pa_h_hj32_local_product_h36t_p44_product_product_terminal + S (x) = S ((S (2 * 37)) * pa_v_hj32_local_product_h36t_p44_product_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_terminal. pa_u_hj32_local_product_h36t_p44_product_product = pa_q_hj32_local_product_h36t_p44_product_product_terminal * S ((S (2 * 37)) * pa_v_hj32_local_product_h36t_p44_product_product) + (x))) /\ forall pa_i_hj32_local_product_h36t_p44_product_product. (exists pa_lt_hj32_local_product_h36t_p44_product_product_bound. pa_lt_hj32_local_product_h36t_p44_product_product_bound + S pa_i_hj32_local_product_h36t_p44_product_product = 2 * 37) -> exists pa_p_hj32_local_product_h36t_p44_product_product pa_r_hj32_local_product_h36t_p44_product_product pa_s_hj32_local_product_h36t_p44_product_product. ((((exists pa_h_hj32_local_product_h36t_p44_product_product_factor. pa_h_hj32_local_product_h36t_p44_product_product_factor + S (pa_p_hj32_local_product_h36t_p44_product_product) = S ((S (pa_i_hj32_local_product_h36t_p44_product_product)) * pa_c_hj32_local_product_h36t_p44_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_factor. pa_b_hj32_local_product_h36t_p44_product = pa_q_hj32_local_product_h36t_p44_product_product_factor * S ((S (pa_i_hj32_local_product_h36t_p44_product_product)) * pa_c_hj32_local_product_h36t_p44_product) + (pa_p_hj32_local_product_h36t_p44_product_product))) /\ ((((exists pa_h_hj32_local_product_h36t_p44_product_product_partial. pa_h_hj32_local_product_h36t_p44_product_product_partial + S (pa_r_hj32_local_product_h36t_p44_product_product) = S ((S (pa_i_hj32_local_product_h36t_p44_product_product)) * pa_v_hj32_local_product_h36t_p44_product_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_partial. pa_u_hj32_local_product_h36t_p44_product_product = pa_q_hj32_local_product_h36t_p44_product_product_partial * S ((S (pa_i_hj32_local_product_h36t_p44_product_product)) * pa_v_hj32_local_product_h36t_p44_product_product) + (pa_r_hj32_local_product_h36t_p44_product_product))) /\ ((((exists pa_h_hj32_local_product_h36t_p44_product_product_successor. pa_h_hj32_local_product_h36t_p44_product_product_successor + S (pa_s_hj32_local_product_h36t_p44_product_product) = S ((S (S pa_i_hj32_local_product_h36t_p44_product_product)) * pa_v_hj32_local_product_h36t_p44_product_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_successor. pa_u_hj32_local_product_h36t_p44_product_product = pa_q_hj32_local_product_h36t_p44_product_product_successor * S ((S (S pa_i_hj32_local_product_h36t_p44_product_product)) * pa_v_hj32_local_product_h36t_p44_product_product) + (pa_s_hj32_local_product_h36t_p44_product_product))) /\ pa_s_hj32_local_product_h36t_p44_product_product = pa_r_hj32_local_product_h36t_p44_product_product * pa_p_hj32_local_product_h36t_p44_product_product)))))))
  49. 0049have h36t_p44_product_base : 4 * 11 = 44
  50. 0050norm_num
  51. 0051rewrite h36t_p44_product_base
  52. 0052rewrite h36t_p44_product_base
  53. 0053exact h36t_p44_witness
  54. 0054have h36t_p44_product : x = x1 * x2
  55. 0055specialize pow_mul_base 4
  56. 0056specialize pow_mul_base 11
  57. 0057specialize pow_mul_base 2 * 37
  58. 0058specialize pow_mul_base x1
  59. 0059specialize pow_mul_base x2
  60. 0060specialize pow_mul_base x
  61. 0061apply pow_mul_base
  62. 0062exact h36t_p4_exp_witness
  63. 0063exact h36t_p11_exp_witness
  64. 0064exact h36t_p44_product_graph
  65. 0065have h36t_p4_tail : ∃ hj32_local_value_h36t_p4_tail. Pow(4,2 · (5 · 13),hj32_local_value_h36t_p4_tail)
    Exact native replay linehave h36t_p4_tail : exists hj32_local_value_h36t_p4_tail. (exists pa_b_hj32_local_total_h36t_p4_tail pa_c_hj32_local_total_h36t_p4_tail. ((forall pa_i_hj32_local_total_h36t_p4_tail_repeat. (exists pa_lt_hj32_local_total_h36t_p4_tail_repeat_bound. pa_lt_hj32_local_total_h36t_p4_tail_repeat_bound + S pa_i_hj32_local_total_h36t_p4_tail_repeat = 2 * (5 * 13)) -> (((exists pa_h_hj32_local_total_h36t_p4_tail_repeat_decoded. pa_h_hj32_local_total_h36t_p4_tail_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h36t_p4_tail_repeat)) * pa_c_hj32_local_total_h36t_p4_tail)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_repeat_decoded. pa_b_hj32_local_total_h36t_p4_tail = pa_q_hj32_local_total_h36t_p4_tail_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p4_tail_repeat)) * pa_c_hj32_local_total_h36t_p4_tail) + (4)))) /\ (exists pa_u_hj32_local_total_h36t_p4_tail_product pa_v_hj32_local_total_h36t_p4_tail_product. ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_start. pa_h_hj32_local_total_h36t_p4_tail_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_start. pa_u_hj32_local_total_h36t_p4_tail_product = pa_q_hj32_local_total_h36t_p4_tail_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p4_tail_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_terminal. pa_h_hj32_local_total_h36t_p4_tail_product_terminal + S (hj32_local_value_h36t_p4_tail) = S ((S (2 * (5 * 13))) * pa_v_hj32_local_total_h36t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_terminal. pa_u_hj32_local_total_h36t_p4_tail_product = pa_q_hj32_local_total_h36t_p4_tail_product_terminal * S ((S (2 * (5 * 13))) * pa_v_hj32_local_total_h36t_p4_tail_product) + (hj32_local_value_h36t_p4_tail))) /\ forall pa_i_hj32_local_total_h36t_p4_tail_product. (exists pa_lt_hj32_local_total_h36t_p4_tail_product_bound. pa_lt_hj32_local_total_h36t_p4_tail_product_bound + S pa_i_hj32_local_total_h36t_p4_tail_product = 2 * (5 * 13)) -> exists pa_p_hj32_local_total_h36t_p4_tail_product pa_r_hj32_local_total_h36t_p4_tail_product pa_s_hj32_local_total_h36t_p4_tail_product. ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_factor. pa_h_hj32_local_total_h36t_p4_tail_product_factor + S (pa_p_hj32_local_total_h36t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_c_hj32_local_total_h36t_p4_tail)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_factor. pa_b_hj32_local_total_h36t_p4_tail = pa_q_hj32_local_total_h36t_p4_tail_product_factor * S ((S (pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_c_hj32_local_total_h36t_p4_tail) + (pa_p_hj32_local_total_h36t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_partial. pa_h_hj32_local_total_h36t_p4_tail_product_partial + S (pa_r_hj32_local_total_h36t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_v_hj32_local_total_h36t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_partial. pa_u_hj32_local_total_h36t_p4_tail_product = pa_q_hj32_local_total_h36t_p4_tail_product_partial * S ((S (pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_v_hj32_local_total_h36t_p4_tail_product) + (pa_r_hj32_local_total_h36t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_successor. pa_h_hj32_local_total_h36t_p4_tail_product_successor + S (pa_s_hj32_local_total_h36t_p4_tail_product) = S ((S (S pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_v_hj32_local_total_h36t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_successor. pa_u_hj32_local_total_h36t_p4_tail_product = pa_q_hj32_local_total_h36t_p4_tail_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_v_hj32_local_total_h36t_p4_tail_product) + (pa_s_hj32_local_total_h36t_p4_tail_product))) /\ pa_s_hj32_local_total_h36t_p4_tail_product = pa_r_hj32_local_total_h36t_p4_tail_product * pa_p_hj32_local_total_h36t_p4_tail_product))))))))
  66. 0066specialize htotal 4
  67. 0067specialize htotal 2 * (5 * 13)
  68. 0068exact htotal
  69. 0069cases h36t_p4_tail
  70. 0070have h36t_tail_power : Pow(4,14 · 9 + 3 + 1,x3)
    Exact native replay linehave h36t_tail_power : exists pa_b_hj32_h36t_tail_power pa_c_hj32_h36t_tail_power. ((forall pa_i_hj32_h36t_tail_power_repeat. (exists pa_lt_hj32_h36t_tail_power_repeat_bound. pa_lt_hj32_h36t_tail_power_repeat_bound + S pa_i_hj32_h36t_tail_power_repeat = (14 * 9 + 3) + 1) -> (((exists pa_h_hj32_h36t_tail_power_repeat_decoded. pa_h_hj32_h36t_tail_power_repeat_decoded + S (4) = S ((S (pa_i_hj32_h36t_tail_power_repeat)) * pa_c_hj32_h36t_tail_power)) /\ exists pa_q_hj32_h36t_tail_power_repeat_decoded. pa_b_hj32_h36t_tail_power = pa_q_hj32_h36t_tail_power_repeat_decoded * S ((S (pa_i_hj32_h36t_tail_power_repeat)) * pa_c_hj32_h36t_tail_power) + (4)))) /\ (exists pa_u_hj32_h36t_tail_power_product pa_v_hj32_h36t_tail_power_product. ((((exists pa_h_hj32_h36t_tail_power_product_start. pa_h_hj32_h36t_tail_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_h36t_tail_power_product)) /\ exists pa_q_hj32_h36t_tail_power_product_start. pa_u_hj32_h36t_tail_power_product = pa_q_hj32_h36t_tail_power_product_start * S ((S (0)) * pa_v_hj32_h36t_tail_power_product) + (1))) /\ ((((exists pa_h_hj32_h36t_tail_power_product_terminal. pa_h_hj32_h36t_tail_power_product_terminal + S (x3) = S ((S ((14 * 9 + 3) + 1)) * pa_v_hj32_h36t_tail_power_product)) /\ exists pa_q_hj32_h36t_tail_power_product_terminal. pa_u_hj32_h36t_tail_power_product = pa_q_hj32_h36t_tail_power_product_terminal * S ((S ((14 * 9 + 3) + 1)) * pa_v_hj32_h36t_tail_power_product) + (x3))) /\ forall pa_i_hj32_h36t_tail_power_product. (exists pa_lt_hj32_h36t_tail_power_product_bound. pa_lt_hj32_h36t_tail_power_product_bound + S pa_i_hj32_h36t_tail_power_product = (14 * 9 + 3) + 1) -> exists pa_p_hj32_h36t_tail_power_product pa_r_hj32_h36t_tail_power_product pa_s_hj32_h36t_tail_power_product. ((((exists pa_h_hj32_h36t_tail_power_product_factor. pa_h_hj32_h36t_tail_power_product_factor + S (pa_p_hj32_h36t_tail_power_product) = S ((S (pa_i_hj32_h36t_tail_power_product)) * pa_c_hj32_h36t_tail_power)) /\ exists pa_q_hj32_h36t_tail_power_product_factor. pa_b_hj32_h36t_tail_power = pa_q_hj32_h36t_tail_power_product_factor * S ((S (pa_i_hj32_h36t_tail_power_product)) * pa_c_hj32_h36t_tail_power) + (pa_p_hj32_h36t_tail_power_product))) /\ ((((exists pa_h_hj32_h36t_tail_power_product_partial. pa_h_hj32_h36t_tail_power_product_partial + S (pa_r_hj32_h36t_tail_power_product) = S ((S (pa_i_hj32_h36t_tail_power_product)) * pa_v_hj32_h36t_tail_power_product)) /\ exists pa_q_hj32_h36t_tail_power_product_partial. pa_u_hj32_h36t_tail_power_product = pa_q_hj32_h36t_tail_power_product_partial * S ((S (pa_i_hj32_h36t_tail_power_product)) * pa_v_hj32_h36t_tail_power_product) + (pa_r_hj32_h36t_tail_power_product))) /\ ((((exists pa_h_hj32_h36t_tail_power_product_successor. pa_h_hj32_h36t_tail_power_product_successor + S (pa_s_hj32_h36t_tail_power_product) = S ((S (S pa_i_hj32_h36t_tail_power_product)) * pa_v_hj32_h36t_tail_power_product)) /\ exists pa_q_hj32_h36t_tail_power_product_successor. pa_u_hj32_h36t_tail_power_product = pa_q_hj32_h36t_tail_power_product_successor * S ((S (S pa_i_hj32_h36t_tail_power_product)) * pa_v_hj32_h36t_tail_power_product) + (pa_s_hj32_h36t_tail_power_product))) /\ pa_s_hj32_h36t_tail_power_product = pa_r_hj32_h36t_tail_power_product * pa_p_hj32_h36t_tail_power_product)))))))
  71. 0071have h36t_tail_exponent : (14 * 9 + 3) + 1 = 2 * (5 * 13)
  72. 0072have h36t_tail_left : (14 * 9 + 3) + 1 = 2 * (7 * 9 + 2)
  73. 0073have h36t_tail_assoc : (14 * 9 + 3) + 1 = 14 * 9 + (3 + 1)
  74. 0074specialize add_assoc (14 * 9)
  75. 0075specialize add_assoc 3
  76. 0076specialize add_assoc 1
  77. 0077apply add_assoc
  78. 0078rewrite h36t_tail_assoc
  79. 0079have h36t_four : 3 + 1 = 2 * 2
  80. 0080norm_num
  81. 0081rewrite h36t_four
  82. 0082have h36t_fourteen : 14 = 2 * 7
  83. 0083norm_num
  84. 0084rewrite h36t_fourteen
  85. 0085have h36t_assoc_mul : (2 * 7) * 9 = 2 * (7 * 9)
  86. 0086specialize mul_assoc 2
  87. 0087specialize mul_assoc 7
  88. 0088specialize mul_assoc 9
  89. 0089apply mul_assoc
  90. 0090rewrite h36t_assoc_mul
  91. 0091have h36t_factor : 2 * (7 * 9 + 2) = 2 * (7 * 9) + 2 * 2
  92. 0092specialize mul_add 2
  93. 0093specialize mul_add (7 * 9)
  94. 0094specialize mul_add 2
  95. 0095apply mul_add
  96. 0096rewrite <- h36t_factor
  97. 0097refl
  98. 0098have h36t_tail_right : 2 * (7 * 9 + 2) = 2 * (5 * 13)
  99. 0099have h36t_inside : 7 * 9 + 2 = 5 * 13
  100. 0100norm_num
  101. 0101rewrite h36t_inside
  102. 0102refl
  103. 0103trans 2 * (7 * 9 + 2)
  104. 0104exact h36t_tail_left
  105. 0105exact h36t_tail_right
  106. 0106rewrite h36t_tail_exponent
  107. 0107rewrite h36t_tail_exponent
  108. 0108rewrite h36t_tail_exponent
  109. 0109rewrite h36t_tail_exponent
  110. 0110exact h36t_p4_tail_witness
  111. 0111have h36t_parity : 7 * 37 = 2 * (14 * 9 + 3) + 1
  112. 0112have h36t_left : 7 * 37 = 28 * 9 + 7
  113. 0113have h36t_root : 37 = 4 * 9 + 1
  114. 0114norm_num
  115. 0115rewrite h36t_root
  116. 0116have h36t_left_distrib : 7 * (4 * 9 + 1) = 7 * (4 * 9) + 7 * 1
  117. 0117specialize mul_add 7
  118. 0118specialize mul_add (4 * 9)
  119. 0119specialize mul_add 1
  120. 0120apply mul_add
  121. 0121rewrite h36t_left_distrib
  122. 0122have h36t_left_assoc : 7 * (4 * 9) = (7 * 4) * 9
  123. 0123symm
  124. 0124specialize mul_assoc 7
  125. 0125specialize mul_assoc 4
  126. 0126specialize mul_assoc 9
  127. 0127apply mul_assoc
  128. 0128rewrite h36t_left_assoc
  129. 0129have h36t_twenty_eight : 7 * 4 = 28
  130. 0130norm_num
  131. 0131rewrite h36t_twenty_eight
  132. 0132have h36t_seven : 7 * 1 = 7
  133. 0133norm_num
  134. 0134rewrite h36t_seven
  135. 0135refl
  136. 0136have h36t_right : 2 * (14 * 9 + 3) + 1 = 28 * 9 + 7
  137. 0137have h36t_right_distrib : 2 * (14 * 9 + 3) = 2 * (14 * 9) + 2 * 3
  138. 0138specialize mul_add 2
  139. 0139specialize mul_add (14 * 9)
  140. 0140specialize mul_add 3
  141. 0141apply mul_add
  142. 0142rewrite h36t_right_distrib
  143. 0143have h36t_right_assoc : 2 * (14 * 9) = (2 * 14) * 9
  144. 0144symm
  145. 0145specialize mul_assoc 2
  146. 0146specialize mul_assoc 14
  147. 0147specialize mul_assoc 9
  148. 0148apply mul_assoc
  149. 0149rewrite h36t_right_assoc
  150. 0150have h36t_right_twenty_eight : 2 * 14 = 28
  151. 0151norm_num
  152. 0152rewrite h36t_right_twenty_eight
  153. 0153have h36t_right_add : (28 * 9 + 2 * 3) + 1 = 28 * 9 + (2 * 3 + 1)
  154. 0154specialize add_assoc (28 * 9)
  155. 0155specialize add_assoc (2 * 3)
  156. 0156specialize add_assoc 1
  157. 0157apply add_assoc
  158. 0158rewrite h36t_right_add
  159. 0159have h36t_right_seven : 2 * 3 + 1 = 7
  160. 0160norm_num
  161. 0161rewrite h36t_right_seven
  162. 0162refl
  163. 0163trans 28 * 9 + 7
  164. 0164exact h36t_left
  165. 0165symm
  166. 0166exact h36t_right
  167. 0167have h36t_eleven_bound : Le(x2,x3)
    Exact native replay linehave h36t_eleven_bound : exists bqb_le_gap_hj32_h36t_eleven_bound. bqb_le_gap_hj32_h36t_eleven_bound + (x2) = (x3)
  168. 0168specialize pow_eleven_double_block_le_pow_four_odd_from_total 37
  169. 0169specialize pow_eleven_double_block_le_pow_four_odd_from_total (14 * 9 + 3)
  170. 0170specialize pow_eleven_double_block_le_pow_four_odd_from_total x2
  171. 0171specialize pow_eleven_double_block_le_pow_four_odd_from_total x3
  172. 0172apply pow_eleven_double_block_le_pow_four_odd_from_total
  173. 0173exact htotal
  174. 0174exact h36t_parity
  175. 0175exact h36t_p11_exp_witness
  176. 0176exact h36t_tail_power
  177. 0177have h36t_four_refl : Le(x1,x1)
    Exact native replay linehave h36t_four_refl : exists bqb_le_gap_hj32_h36t_four_refl. bqb_le_gap_hj32_h36t_four_refl + (x1) = (x1)
  178. 0178specialize le_refl x1
  179. 0179exact le_refl
  180. 0180have h36t_product_bound : Le(x1 · x2,x1 · x3)
    Exact native replay linehave h36t_product_bound : exists bqb_le_gap_hj32_local_product_bound_h36t_product_bound. bqb_le_gap_hj32_local_product_bound_h36t_product_bound + (x1 * x2) = (x1 * x3)
  181. 0181specialize mul_le_mul x1
  182. 0182specialize mul_le_mul x1
  183. 0183specialize mul_le_mul x2
  184. 0184specialize mul_le_mul x3
  185. 0185apply mul_le_mul
  186. 0186exact h36t_four_refl
  187. 0187exact h36t_eleven_bound
  188. 0188have h36t_p4_budget : ∃ hj32_local_value_h36t_p4_budget. Pow(4,2 · 37 + 2 · (5 · 13),hj32_local_value_h36t_p4_budget)
    Exact native replay linehave h36t_p4_budget : exists hj32_local_value_h36t_p4_budget. (exists pa_b_hj32_local_total_h36t_p4_budget pa_c_hj32_local_total_h36t_p4_budget. ((forall pa_i_hj32_local_total_h36t_p4_budget_repeat. (exists pa_lt_hj32_local_total_h36t_p4_budget_repeat_bound. pa_lt_hj32_local_total_h36t_p4_budget_repeat_bound + S pa_i_hj32_local_total_h36t_p4_budget_repeat = 2 * 37 + 2 * (5 * 13)) -> (((exists pa_h_hj32_local_total_h36t_p4_budget_repeat_decoded. pa_h_hj32_local_total_h36t_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h36t_p4_budget_repeat)) * pa_c_hj32_local_total_h36t_p4_budget)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_repeat_decoded. pa_b_hj32_local_total_h36t_p4_budget = pa_q_hj32_local_total_h36t_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p4_budget_repeat)) * pa_c_hj32_local_total_h36t_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h36t_p4_budget_product pa_v_hj32_local_total_h36t_p4_budget_product. ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_start. pa_h_hj32_local_total_h36t_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_start. pa_u_hj32_local_total_h36t_p4_budget_product = pa_q_hj32_local_total_h36t_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_terminal. pa_h_hj32_local_total_h36t_p4_budget_product_terminal + S (hj32_local_value_h36t_p4_budget) = S ((S (2 * 37 + 2 * (5 * 13))) * pa_v_hj32_local_total_h36t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_terminal. pa_u_hj32_local_total_h36t_p4_budget_product = pa_q_hj32_local_total_h36t_p4_budget_product_terminal * S ((S (2 * 37 + 2 * (5 * 13))) * pa_v_hj32_local_total_h36t_p4_budget_product) + (hj32_local_value_h36t_p4_budget))) /\ forall pa_i_hj32_local_total_h36t_p4_budget_product. (exists pa_lt_hj32_local_total_h36t_p4_budget_product_bound. pa_lt_hj32_local_total_h36t_p4_budget_product_bound + S pa_i_hj32_local_total_h36t_p4_budget_product = 2 * 37 + 2 * (5 * 13)) -> exists pa_p_hj32_local_total_h36t_p4_budget_product pa_r_hj32_local_total_h36t_p4_budget_product pa_s_hj32_local_total_h36t_p4_budget_product. ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_factor. pa_h_hj32_local_total_h36t_p4_budget_product_factor + S (pa_p_hj32_local_total_h36t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_c_hj32_local_total_h36t_p4_budget)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_factor. pa_b_hj32_local_total_h36t_p4_budget = pa_q_hj32_local_total_h36t_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_c_hj32_local_total_h36t_p4_budget) + (pa_p_hj32_local_total_h36t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_partial. pa_h_hj32_local_total_h36t_p4_budget_product_partial + S (pa_r_hj32_local_total_h36t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_v_hj32_local_total_h36t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_partial. pa_u_hj32_local_total_h36t_p4_budget_product = pa_q_hj32_local_total_h36t_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_v_hj32_local_total_h36t_p4_budget_product) + (pa_r_hj32_local_total_h36t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_successor. pa_h_hj32_local_total_h36t_p4_budget_product_successor + S (pa_s_hj32_local_total_h36t_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_v_hj32_local_total_h36t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_successor. pa_u_hj32_local_total_h36t_p4_budget_product = pa_q_hj32_local_total_h36t_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_v_hj32_local_total_h36t_p4_budget_product) + (pa_s_hj32_local_total_h36t_p4_budget_product))) /\ pa_s_hj32_local_total_h36t_p4_budget_product = pa_r_hj32_local_total_h36t_p4_budget_product * pa_p_hj32_local_total_h36t_p4_budget_product))))))))
  189. 0189specialize htotal 4
  190. 0190specialize htotal 2 * 37 + 2 * (5 * 13)
  191. 0191exact htotal
  192. 0192cases h36t_p4_budget
  193. 0193have h36t_budget_product : x4 = x1 * x3
  194. 0194specialize pow_add 4
  195. 0195specialize pow_add 2 * 37
  196. 0196specialize pow_add 2 * (5 * 13)
  197. 0197specialize pow_add 2 * 37 + 2 * (5 * 13)
  198. 0198specialize pow_add x1
  199. 0199specialize pow_add x3
  200. 0200specialize pow_add x4
  201. 0201apply pow_add
  202. 0202refl
  203. 0203exact h36t_p4_exp_witness
  204. 0204exact h36t_p4_tail_witness
  205. 0205exact h36t_p4_budget_witness
  206. 0206rewrite <- h36t_p44_product at h36t_product_bound
  207. 0207rewrite <- h36t_budget_product at h36t_product_bound
  208. 0208have h36t_to_budget : Le(h,x4)
    Exact native replay linehave h36t_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h36t_to_budget. bqb_le_gap_hj32_local_trans_bound_h36t_to_budget + (h) = (x4)
  209. 0209specialize le_trans h
  210. 0210specialize le_trans x
  211. 0211specialize le_trans x4
  212. 0212apply le_trans
  213. 0213exact h36t_to_44
  214. 0214exact h36t_product_bound
  215. 0215have hscaled : Le(6 · (2 · 37 + 2 · (5 · 13)),36 · 36)
    Exact native replay linehave hscaled : exists bqb_le_gap_hj32_scaled_budget_root_36. bqb_le_gap_hj32_scaled_budget_root_36 + (6 * (2 * 37 + 2 * (5 * 13))) = (36 * 36)
  216. 0216apply bertrand_scaled_budget_root_36
  217. 0217have hbudget_exponent : Le(2 · 37 + 2 · (5 · 13),e)
    Exact native replay linehave hbudget_exponent : exists bqb_le_gap_hj32_h_36_budget_exponent. bqb_le_gap_hj32_h_36_budget_exponent + (2 * 37 + 2 * (5 * 13)) = (e)
  218. 0218specialize ceil_div_six_budget_of_scaled_le (36 * 36)
  219. 0219specialize ceil_div_six_budget_of_scaled_le (2 * 37 + 2 * (5 * 13))
  220. 0220specialize ceil_div_six_budget_of_scaled_le e
  221. 0221apply ceil_div_six_budget_of_scaled_le
  222. 0222exact hceiling
  223. 0223exact hscaled
  224. 0224have h36_budget_growth : Le(x4,u)
    Exact native replay linehave h36_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h36_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h36_budget_growth + (x4) = (u)
  225. 0225specialize pow_exponent_monotone_from_total 4
  226. 0226specialize pow_exponent_monotone_from_total 2 * 37 + 2 * (5 * 13)
  227. 0227specialize pow_exponent_monotone_from_total e
  228. 0228specialize pow_exponent_monotone_from_total x4
  229. 0229specialize pow_exponent_monotone_from_total u
  230. 0230apply pow_exponent_monotone_from_total
  231. 0231exact htotal
  232. 0232exists 3
  233. 0233norm_num
  234. 0234exact hbudget_exponent
  235. 0235exact h36t_p4_budget_witness
  236. 0236exact hu
  237. 0237have h36_result : Le(h,u)
    Exact native replay linehave h36_result : exists bqb_le_gap_hj32_local_trans_bound_h36_result. bqb_le_gap_hj32_local_trans_bound_h36_result + (h) = (u)
  238. 0238specialize le_trans h
  239. 0239specialize le_trans x4
  240. 0240specialize le_trans u
  241. 0241apply le_trans
  242. 0242exact h36t_to_budget
  243. 0243exact h36_budget_growth
  244. 0244exact h36_result