BT00WP · Bertrand theorem

bertrand_h_root_32_from_total

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

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

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(32 · 32,e) → Pow(32 + 1,2 · 32 + 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 PD0020 Pow

16 occurrences

Exact expanded native-PA statement
forall e h u. (forall bpt_a_hj32_h_root_32 bpt_e_hj32_h_root_32. exists bpt_x_hj32_h_root_32. (exists ff_b_bpt_value_hj32_h_root_32 ff_c_bpt_value_hj32_h_root_32. ((forall ff_i_bpt_value_hj32_h_root_32_repeat. (exists ff_lt_bpt_value_hj32_h_root_32_repeat_bound. ff_lt_bpt_value_hj32_h_root_32_repeat_bound + S ff_i_bpt_value_hj32_h_root_32_repeat = bpt_e_hj32_h_root_32) -> (((exists ff_h_bpt_value_hj32_h_root_32_repeat_decoded. ff_h_bpt_value_hj32_h_root_32_repeat_decoded + S (bpt_a_hj32_h_root_32) = S ((S (ff_i_bpt_value_hj32_h_root_32_repeat)) * ff_c_bpt_value_hj32_h_root_32)) /\ exists ff_q_bpt_value_hj32_h_root_32_repeat_decoded. ff_b_bpt_value_hj32_h_root_32 = ff_q_bpt_value_hj32_h_root_32_repeat_decoded * S ((S (ff_i_bpt_value_hj32_h_root_32_repeat)) * ff_c_bpt_value_hj32_h_root_32) + (bpt_a_hj32_h_root_32)))) /\ (exists ff_u_bpt_value_hj32_h_root_32_product ff_v_bpt_value_hj32_h_root_32_product. ((((exists ff_h_bpt_value_hj32_h_root_32_product_start. ff_h_bpt_value_hj32_h_root_32_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_h_root_32_product)) /\ exists ff_q_bpt_value_hj32_h_root_32_product_start. ff_u_bpt_value_hj32_h_root_32_product = ff_q_bpt_value_hj32_h_root_32_product_start * S ((S (0)) * ff_v_bpt_value_hj32_h_root_32_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_h_root_32_product_terminal. ff_h_bpt_value_hj32_h_root_32_product_terminal + S (bpt_x_hj32_h_root_32) = S ((S (bpt_e_hj32_h_root_32)) * ff_v_bpt_value_hj32_h_root_32_product)) /\ exists ff_q_bpt_value_hj32_h_root_32_product_terminal. ff_u_bpt_value_hj32_h_root_32_product = ff_q_bpt_value_hj32_h_root_32_product_terminal * S ((S (bpt_e_hj32_h_root_32)) * ff_v_bpt_value_hj32_h_root_32_product) + (bpt_x_hj32_h_root_32))) /\ forall ff_i_bpt_value_hj32_h_root_32_product. (exists ff_lt_bpt_value_hj32_h_root_32_product_bound. ff_lt_bpt_value_hj32_h_root_32_product_bound + S ff_i_bpt_value_hj32_h_root_32_product = bpt_e_hj32_h_root_32) -> exists ff_p_bpt_value_hj32_h_root_32_product ff_r_bpt_value_hj32_h_root_32_product ff_s_bpt_value_hj32_h_root_32_product. ((((exists ff_h_bpt_value_hj32_h_root_32_product_factor. ff_h_bpt_value_hj32_h_root_32_product_factor + S (ff_p_bpt_value_hj32_h_root_32_product) = S ((S (ff_i_bpt_value_hj32_h_root_32_product)) * ff_c_bpt_value_hj32_h_root_32)) /\ exists ff_q_bpt_value_hj32_h_root_32_product_factor. ff_b_bpt_value_hj32_h_root_32 = ff_q_bpt_value_hj32_h_root_32_product_factor * S ((S (ff_i_bpt_value_hj32_h_root_32_product)) * ff_c_bpt_value_hj32_h_root_32) + (ff_p_bpt_value_hj32_h_root_32_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_32_product_partial. ff_h_bpt_value_hj32_h_root_32_product_partial + S (ff_r_bpt_value_hj32_h_root_32_product) = S ((S (ff_i_bpt_value_hj32_h_root_32_product)) * ff_v_bpt_value_hj32_h_root_32_product)) /\ exists ff_q_bpt_value_hj32_h_root_32_product_partial. ff_u_bpt_value_hj32_h_root_32_product = ff_q_bpt_value_hj32_h_root_32_product_partial * S ((S (ff_i_bpt_value_hj32_h_root_32_product)) * ff_v_bpt_value_hj32_h_root_32_product) + (ff_r_bpt_value_hj32_h_root_32_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_32_product_successor. ff_h_bpt_value_hj32_h_root_32_product_successor + S (ff_s_bpt_value_hj32_h_root_32_product) = S ((S (S ff_i_bpt_value_hj32_h_root_32_product)) * ff_v_bpt_value_hj32_h_root_32_product)) /\ exists ff_q_bpt_value_hj32_h_root_32_product_successor. ff_u_bpt_value_hj32_h_root_32_product = ff_q_bpt_value_hj32_h_root_32_product_successor * S ((S (S ff_i_bpt_value_hj32_h_root_32_product)) * ff_v_bpt_value_hj32_h_root_32_product) + (ff_s_bpt_value_hj32_h_root_32_product))) /\ ff_s_bpt_value_hj32_h_root_32_product = ff_r_bpt_value_hj32_h_root_32_product * ff_p_bpt_value_hj32_h_root_32_product))))))))) -> (((exists bcs_lower_gap_hj32_h_root_32_ceiling. bcs_lower_gap_hj32_h_root_32_ceiling + (32 * 32) = 6 * (e)) /\ exists bcs_upper_gap_hj32_h_root_32_ceiling. bcs_upper_gap_hj32_h_root_32_ceiling + S (6 * (e)) = (32 * 32) + 6)) -> (exists pa_b_hj32_h_root_32_h pa_c_hj32_h_root_32_h. ((forall pa_i_hj32_h_root_32_h_repeat. (exists pa_lt_hj32_h_root_32_h_repeat_bound. pa_lt_hj32_h_root_32_h_repeat_bound + S pa_i_hj32_h_root_32_h_repeat = 2 * 32 + 2) -> (((exists pa_h_hj32_h_root_32_h_repeat_decoded. pa_h_hj32_h_root_32_h_repeat_decoded + S (32 + 1) = S ((S (pa_i_hj32_h_root_32_h_repeat)) * pa_c_hj32_h_root_32_h)) /\ exists pa_q_hj32_h_root_32_h_repeat_decoded. pa_b_hj32_h_root_32_h = pa_q_hj32_h_root_32_h_repeat_decoded * S ((S (pa_i_hj32_h_root_32_h_repeat)) * pa_c_hj32_h_root_32_h) + (32 + 1)))) /\ (exists pa_u_hj32_h_root_32_h_product pa_v_hj32_h_root_32_h_product. ((((exists pa_h_hj32_h_root_32_h_product_start. pa_h_hj32_h_root_32_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_32_h_product)) /\ exists pa_q_hj32_h_root_32_h_product_start. pa_u_hj32_h_root_32_h_product = pa_q_hj32_h_root_32_h_product_start * S ((S (0)) * pa_v_hj32_h_root_32_h_product) + (1))) /\ ((((exists pa_h_hj32_h_root_32_h_product_terminal. pa_h_hj32_h_root_32_h_product_terminal + S (h) = S ((S (2 * 32 + 2)) * pa_v_hj32_h_root_32_h_product)) /\ exists pa_q_hj32_h_root_32_h_product_terminal. pa_u_hj32_h_root_32_h_product = pa_q_hj32_h_root_32_h_product_terminal * S ((S (2 * 32 + 2)) * pa_v_hj32_h_root_32_h_product) + (h))) /\ forall pa_i_hj32_h_root_32_h_product. (exists pa_lt_hj32_h_root_32_h_product_bound. pa_lt_hj32_h_root_32_h_product_bound + S pa_i_hj32_h_root_32_h_product = 2 * 32 + 2) -> exists pa_p_hj32_h_root_32_h_product pa_r_hj32_h_root_32_h_product pa_s_hj32_h_root_32_h_product. ((((exists pa_h_hj32_h_root_32_h_product_factor. pa_h_hj32_h_root_32_h_product_factor + S (pa_p_hj32_h_root_32_h_product) = S ((S (pa_i_hj32_h_root_32_h_product)) * pa_c_hj32_h_root_32_h)) /\ exists pa_q_hj32_h_root_32_h_product_factor. pa_b_hj32_h_root_32_h = pa_q_hj32_h_root_32_h_product_factor * S ((S (pa_i_hj32_h_root_32_h_product)) * pa_c_hj32_h_root_32_h) + (pa_p_hj32_h_root_32_h_product))) /\ ((((exists pa_h_hj32_h_root_32_h_product_partial. pa_h_hj32_h_root_32_h_product_partial + S (pa_r_hj32_h_root_32_h_product) = S ((S (pa_i_hj32_h_root_32_h_product)) * pa_v_hj32_h_root_32_h_product)) /\ exists pa_q_hj32_h_root_32_h_product_partial. pa_u_hj32_h_root_32_h_product = pa_q_hj32_h_root_32_h_product_partial * S ((S (pa_i_hj32_h_root_32_h_product)) * pa_v_hj32_h_root_32_h_product) + (pa_r_hj32_h_root_32_h_product))) /\ ((((exists pa_h_hj32_h_root_32_h_product_successor. pa_h_hj32_h_root_32_h_product_successor + S (pa_s_hj32_h_root_32_h_product) = S ((S (S pa_i_hj32_h_root_32_h_product)) * pa_v_hj32_h_root_32_h_product)) /\ exists pa_q_hj32_h_root_32_h_product_successor. pa_u_hj32_h_root_32_h_product = pa_q_hj32_h_root_32_h_product_successor * S ((S (S pa_i_hj32_h_root_32_h_product)) * pa_v_hj32_h_root_32_h_product) + (pa_s_hj32_h_root_32_h_product))) /\ pa_s_hj32_h_root_32_h_product = pa_r_hj32_h_root_32_h_product * pa_p_hj32_h_root_32_h_product)))))))) -> (exists pa_b_hj32_h_root_32_u pa_c_hj32_h_root_32_u. ((forall pa_i_hj32_h_root_32_u_repeat. (exists pa_lt_hj32_h_root_32_u_repeat_bound. pa_lt_hj32_h_root_32_u_repeat_bound + S pa_i_hj32_h_root_32_u_repeat = e) -> (((exists pa_h_hj32_h_root_32_u_repeat_decoded. pa_h_hj32_h_root_32_u_repeat_decoded + S (4) = S ((S (pa_i_hj32_h_root_32_u_repeat)) * pa_c_hj32_h_root_32_u)) /\ exists pa_q_hj32_h_root_32_u_repeat_decoded. pa_b_hj32_h_root_32_u = pa_q_hj32_h_root_32_u_repeat_decoded * S ((S (pa_i_hj32_h_root_32_u_repeat)) * pa_c_hj32_h_root_32_u) + (4)))) /\ (exists pa_u_hj32_h_root_32_u_product pa_v_hj32_h_root_32_u_product. ((((exists pa_h_hj32_h_root_32_u_product_start. pa_h_hj32_h_root_32_u_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_32_u_product)) /\ exists pa_q_hj32_h_root_32_u_product_start. pa_u_hj32_h_root_32_u_product = pa_q_hj32_h_root_32_u_product_start * S ((S (0)) * pa_v_hj32_h_root_32_u_product) + (1))) /\ ((((exists pa_h_hj32_h_root_32_u_product_terminal. pa_h_hj32_h_root_32_u_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_h_root_32_u_product)) /\ exists pa_q_hj32_h_root_32_u_product_terminal. pa_u_hj32_h_root_32_u_product = pa_q_hj32_h_root_32_u_product_terminal * S ((S (e)) * pa_v_hj32_h_root_32_u_product) + (u))) /\ forall pa_i_hj32_h_root_32_u_product. (exists pa_lt_hj32_h_root_32_u_product_bound. pa_lt_hj32_h_root_32_u_product_bound + S pa_i_hj32_h_root_32_u_product = e) -> exists pa_p_hj32_h_root_32_u_product pa_r_hj32_h_root_32_u_product pa_s_hj32_h_root_32_u_product. ((((exists pa_h_hj32_h_root_32_u_product_factor. pa_h_hj32_h_root_32_u_product_factor + S (pa_p_hj32_h_root_32_u_product) = S ((S (pa_i_hj32_h_root_32_u_product)) * pa_c_hj32_h_root_32_u)) /\ exists pa_q_hj32_h_root_32_u_product_factor. pa_b_hj32_h_root_32_u = pa_q_hj32_h_root_32_u_product_factor * S ((S (pa_i_hj32_h_root_32_u_product)) * pa_c_hj32_h_root_32_u) + (pa_p_hj32_h_root_32_u_product))) /\ ((((exists pa_h_hj32_h_root_32_u_product_partial. pa_h_hj32_h_root_32_u_product_partial + S (pa_r_hj32_h_root_32_u_product) = S ((S (pa_i_hj32_h_root_32_u_product)) * pa_v_hj32_h_root_32_u_product)) /\ exists pa_q_hj32_h_root_32_u_product_partial. pa_u_hj32_h_root_32_u_product = pa_q_hj32_h_root_32_u_product_partial * S ((S (pa_i_hj32_h_root_32_u_product)) * pa_v_hj32_h_root_32_u_product) + (pa_r_hj32_h_root_32_u_product))) /\ ((((exists pa_h_hj32_h_root_32_u_product_successor. pa_h_hj32_h_root_32_u_product_successor + S (pa_s_hj32_h_root_32_u_product) = S ((S (S pa_i_hj32_h_root_32_u_product)) * pa_v_hj32_h_root_32_u_product)) /\ exists pa_q_hj32_h_root_32_u_product_successor. pa_u_hj32_h_root_32_u_product = pa_q_hj32_h_root_32_u_product_successor * S ((S (S pa_i_hj32_h_root_32_u_product)) * pa_v_hj32_h_root_32_u_product) + (pa_s_hj32_h_root_32_u_product))) /\ pa_s_hj32_h_root_32_u_product = pa_r_hj32_h_root_32_u_product * pa_p_hj32_h_root_32_u_product)))))))) -> (exists bqb_le_gap_hj32_h_root_32_result. bqb_le_gap_hj32_h_root_32_result + (h) = (u))

Proof neighborhood

Direct theorem prerequisites

BT00W8 bertrand_scaled_budget_root_32 BT00WE ceil_div_six_budget_of_scaled_le BT00WH pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total BT00WM pow_eleven_double_block_le_pow_four_odd_from_total BT00QV pow_mul_base BT009X pow_add BT00SN pow_exponent_monotone_from_total BT00PV mul_le_mul 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

204 script commands · 48 reading checkpoints · 36 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 (12)
bertrand scaled budget root 32ceil div six budget of scaled lepow three five block plus one le pow four four block plus one from totalpow eleven double block le pow four odd from totalpow mul basepow addpow exponent monotone from totalmul le mulle 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(33,2 · 33,h)Definitions: Pow(33,2 · 33,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 : 32 + 1 = 33
  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 * 32 + 2 = 2 * 33
  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 h32t_p3_expL20–23

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

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

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

  1. L24
    cases h32t_p3_exp
07Establish h32t_p11_expL25–28

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

  1. L25
    have h32t_p11_exp : ∃ hj32_local_value_h32t_p11_exp. Pow(11,2 · 33,hj32_local_value_h32t_p11_exp)Definitions: Pow(11,2 · 33,hj32_local_value_h32t_p11_exp)Original native command in the exact edition
  2. L26
    specialize htotal 11
  3. L27
    specialize htotal 2 * 33
  4. L28
    exact htotal
08Separate the logical casesL29–29

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

  1. L29
    cases h32t_p11_exp
09Establish h32t_product_graphL30–30

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

  1. L30
    have h32t_product_graph : Pow(3 · 11,2 · 33,h)Definitions: Pow(3 · 11,2 · 33,h)Original native command in the exact edition
10Establish h32t_product_baseL31–35

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

  1. L31
    have h32t_product_base : 3 * 11 = 33
  2. L32
    norm_num
  3. L33
    rewrite h32t_product_base
  4. L34
    rewrite h32t_product_base
  5. L35
    exact hh_route
11Establish h32t_productL36–45

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

  1. L36
    have h32t_product : h = x * x1
  2. L37
    specialize pow_mul_base 3
  3. L38
    specialize pow_mul_base 11
  4. L39
    specialize pow_mul_base 2 * 33
  5. L40
    specialize pow_mul_base x
  6. L41
    specialize pow_mul_base x1
  7. L42
    specialize pow_mul_base h
  8. L43
    apply pow_mul_base
  9. L44
    exact h32t_p3_exp_witness
  10. L45
    exact h32t_p11_exp_witness
12Use earlier factsL46–46

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

  1. L46
    exact h32t_product_graph
13Establish h32t_three_powerL47–47

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

  1. L47
    have h32t_three_power : Pow(3,5 · 13 + 1,x)Definitions: Pow(3,5 · 13 + 1,x)Original native command in the exact edition
14Establish h32t_three_exponentL48–54

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

  1. L48
    have h32t_three_exponent : 2 * 33 = 5 * 13 + 1
  2. L49
    norm_num
  3. L50
    rewrite <- h32t_three_exponent
  4. L51
    rewrite <- h32t_three_exponent
  5. L52
    rewrite <- h32t_three_exponent
  6. L53
    rewrite <- h32t_three_exponent
  7. L54
    exact h32t_p3_exp_witness
15Establish h32t_p4_headL55–58

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

  1. L55
    have h32t_p4_head : ∃ hj32_local_value_h32t_p4_head. Pow(4,4 · 13 + 1,hj32_local_value_h32t_p4_head)Definitions: Pow(4,4 · 13 + 1,hj32_local_value_h32t_p4_head)Original native command in the exact edition
  2. L56
    specialize htotal 4
  3. L57
    specialize htotal 4 * 13 + 1
  4. L58
    exact htotal
16Separate the logical casesL59–59

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

  1. L59
    cases h32t_p4_head
17Establish h32t_three_boundL60–67

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow three five block plus one le pow four four block plus one from total.

  1. L60
    have h32t_three_bound : Le(x,x2)Definitions: Le(x,x2)Original native command in the exact edition
  2. L61
    specialize pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total 13
  3. L62
    specialize pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total x
  4. L63
    specialize pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total x2
  5. L64
    apply pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total
  6. L65
    exact htotal
  7. L66
    exact h32t_three_power
  8. L67
    exact h32t_p4_head_witness
18Establish h32t_p4_tailL68–71

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

  1. L68
    have h32t_p4_tail : ∃ hj32_local_value_h32t_p4_tail. Pow(4,4 · 29,hj32_local_value_h32t_p4_tail)Definitions: Pow(4,4 · 29,hj32_local_value_h32t_p4_tail)Original native command in the exact edition
  2. L69
    specialize htotal 4
  3. L70
    specialize htotal 4 * 29
  4. L71
    exact htotal
19Separate the logical casesL72–72

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

  1. L72
    cases h32t_p4_tail
20Establish h32t_tail_powerL73–73

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

  1. L73
    have h32t_tail_power : Pow(4,14 · 8 + 3 + 1,x3)Definitions: Pow(4,14 · 8 + 3 + 1,x3)Original native command in the exact edition
21Establish h32t_tail_exponentL74–80

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

  1. L74
    have h32t_tail_exponent : (14 * 8 + 3) + 1 = 4 * 29
  2. L75
    norm_num
  3. L76
    rewrite h32t_tail_exponent
  4. L77
    rewrite h32t_tail_exponent
  5. L78
    rewrite h32t_tail_exponent
  6. L79
    rewrite h32t_tail_exponent
  7. L80
    exact h32t_p4_tail_witness
22Establish h32t_parityL81–81

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

  1. L81
    have h32t_parity : 7 * 33 = 2 * (14 * 8 + 3) + 1
23Establish h32t_parity_leftL82–82

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

  1. L82
    have h32t_parity_left : 7 * 33 = 28 * 8 + 7
24Establish h32t_rootL83–85

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

  1. L83
    have h32t_root : 33 = 4 * 8 + 1
  2. L84
    norm_num
  3. L85
    rewrite h32t_root
25Establish h32t_left_distribL86–91

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

  1. L86
    have h32t_left_distrib : 7 * (4 * 8 + 1) = 7 * (4 * 8) + 7 * 1
  2. L87
    specialize mul_add 7
  3. L88
    specialize mul_add (4 * 8)
  4. L89
    specialize mul_add 1
  5. L90
    apply mul_add
  6. L91
    rewrite h32t_left_distrib
26Establish h32t_left_assocL92–98

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

  1. L92
    have h32t_left_assoc : 7 * (4 * 8) = (7 * 4) * 8
  2. L93
    symm
  3. L94
    specialize mul_assoc 7
  4. L95
    specialize mul_assoc 4
  5. L96
    specialize mul_assoc 8
  6. L97
    apply mul_assoc
  7. L98
    rewrite h32t_left_assoc
27Establish h32t_twenty_eightL99–101

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

  1. L99
    have h32t_twenty_eight : 7 * 4 = 28
  2. L100
    norm_num
  3. L101
    rewrite h32t_twenty_eight
28Establish h32t_sevenL102–105

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

  1. L102
    have h32t_seven : 7 * 1 = 7
  2. L103
    norm_num
  3. L104
    rewrite h32t_seven
  4. L105
    refl
29Establish h32t_parity_rightL106–106

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

  1. L106
    have h32t_parity_right : 2 * (14 * 8 + 3) + 1 = 28 * 8 + 7
30Establish h32t_right_distribL107–112

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

  1. L107
    have h32t_right_distrib : 2 * (14 * 8 + 3) = 2 * (14 * 8) + 2 * 3
  2. L108
    specialize mul_add 2
  3. L109
    specialize mul_add (14 * 8)
  4. L110
    specialize mul_add 3
  5. L111
    apply mul_add
  6. L112
    rewrite h32t_right_distrib
31Establish h32t_right_assocL113–119

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

  1. L113
    have h32t_right_assoc : 2 * (14 * 8) = (2 * 14) * 8
  2. L114
    symm
  3. L115
    specialize mul_assoc 2
  4. L116
    specialize mul_assoc 14
  5. L117
    specialize mul_assoc 8
  6. L118
    apply mul_assoc
  7. L119
    rewrite h32t_right_assoc
32Establish h32t_right_twenty_eightL120–122

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

  1. L120
    have h32t_right_twenty_eight : 2 * 14 = 28
  2. L121
    norm_num
  3. L122
    rewrite h32t_right_twenty_eight
33Establish h32t_right_assoc_addL123–128

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

  1. L123
    have h32t_right_assoc_add : (28 * 8 + 2 * 3) + 1 = 28 * 8 + (2 * 3 + 1)
  2. L124
    specialize add_assoc (28 * 8)
  3. L125
    specialize add_assoc (2 * 3)
  4. L126
    specialize add_assoc 1
  5. L127
    apply add_assoc
  6. L128
    rewrite h32t_right_assoc_add
34Establish h32t_right_sevenL129–136

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

  1. L129
    have h32t_right_seven : 2 * 3 + 1 = 7
  2. L130
    norm_num
  3. L131
    rewrite h32t_right_seven
  4. L132
    refl
  5. L133
    trans 28 * 8 + 7
  6. L134
    exact h32t_parity_left
  7. L135
    symm
  8. L136
    exact h32t_parity_right
35Establish h32t_eleven_boundL137–146

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. L137
    have h32t_eleven_bound : Le(x1,x3)Definitions: Le(x1,x3)Original native command in the exact edition
  2. L138
    specialize pow_eleven_double_block_le_pow_four_odd_from_total 33
  3. L139
    specialize pow_eleven_double_block_le_pow_four_odd_from_total (14 * 8 + 3)
  4. L140
    specialize pow_eleven_double_block_le_pow_four_odd_from_total x1
  5. L141
    specialize pow_eleven_double_block_le_pow_four_odd_from_total x3
  6. L142
    apply pow_eleven_double_block_le_pow_four_odd_from_total
  7. L143
    exact htotal
  8. L144
    exact h32t_parity
  9. L145
    exact h32t_p11_exp_witness
  10. L146
    exact h32t_tail_power
36Establish h32t_total_boundL147–154

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

  1. L147
    have h32t_total_bound : Le(x · x1,x2 · x3)Definitions: Le(x · x1,x2 · x3)Original native command in the exact edition
  2. L148
    specialize mul_le_mul x
  3. L149
    specialize mul_le_mul x2
  4. L150
    specialize mul_le_mul x1
  5. L151
    specialize mul_le_mul x3
  6. L152
    apply mul_le_mul
  7. L153
    exact h32t_three_bound
  8. L154
    exact h32t_eleven_bound
37Establish h32t_p4_budgetL155–158

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

  1. L155
    have h32t_p4_budget : ∃ hj32_local_value_h32t_p4_budget. Pow(4,4 · 13 + 1 + 4 · 29,hj32_local_value_h32t_p4_budget)Definitions: Pow(4,4 · 13 + 1 + 4 · 29,hj32_local_value_h32t_p4_budget)Original native command in the exact edition
  2. L156
    specialize htotal 4
  3. L157
    specialize htotal (4 * 13 + 1) + 4 * 29
  4. L158
    exact htotal
38Separate the logical casesL159–159

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

  1. L159
    cases h32t_p4_budget
39Establish h32t_budget_productL160–169

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

  1. L160
    have h32t_budget_product : x4 = x2 * x3
  2. L161
    specialize pow_add 4
  3. L162
    specialize pow_add 4 * 13 + 1
  4. L163
    specialize pow_add 4 * 29
  5. L164
    specialize pow_add (4 * 13 + 1) + 4 * 29
  6. L165
    specialize pow_add x2
  7. L166
    specialize pow_add x3
  8. L167
    specialize pow_add x4
  9. L168
    apply pow_add
  10. L169
    refl
40Use earlier factsL170–172

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

  1. L170
    exact h32t_p4_head_witness
  2. L171
    exact h32t_p4_tail_witness
  3. L172
    exact h32t_p4_budget_witness
41Calculate and transport equalitiesL173–174

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

  1. L173
    rewrite <- h32t_product at h32t_total_bound
  2. L174
    rewrite <- h32t_budget_product at h32t_total_bound
42Establish hscaledL175–176

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

  1. L175
    have hscaled : Le(6 · (4 · 13 + 1 + 4 · 29),32 · 32)Definitions: Le(6 · (4 · 13 + 1 + 4 · 29),32 · 32)Original native command in the exact edition
  2. L176
    apply bertrand_scaled_budget_root_32
43Establish hbudget_exponentL177–183

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. L177
    have hbudget_exponent : Le(4 · 13 + 1 + 4 · 29,e)Definitions: Le(4 · 13 + 1 + 4 · 29,e)Original native command in the exact edition
  2. L178
    specialize ceil_div_six_budget_of_scaled_le (32 * 32)
  3. L179
    specialize ceil_div_six_budget_of_scaled_le ((4 * 13 + 1) + 4 * 29)
  4. L180
    specialize ceil_div_six_budget_of_scaled_le e
  5. L181
    apply ceil_div_six_budget_of_scaled_le
  6. L182
    exact hceiling
  7. L183
    exact hscaled
44Establish h32_budget_growthL184–191

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

  1. L184
    have h32_budget_growth : Le(x4,u)Definitions: Le(x4,u)Original native command in the exact edition
  2. L185
    specialize pow_exponent_monotone_from_total 4
  3. L186
    specialize pow_exponent_monotone_from_total (4 * 13 + 1) + 4 * 29
  4. L187
    specialize pow_exponent_monotone_from_total e
  5. L188
    specialize pow_exponent_monotone_from_total x4
  6. L189
    specialize pow_exponent_monotone_from_total u
  7. L190
    apply pow_exponent_monotone_from_total
  8. L191
    exact htotal
45Construct an explicit witnessL192–192

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

  1. L192
    exists 3
46Calculate and transport equalitiesL193–193

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

  1. L193
    norm_num
47Use earlier factsL194–196

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

  1. L194
    exact hbudget_exponent
  2. L195
    exact h32t_p4_budget_witness
  3. L196
    exact hu
48Establish h32_resultL197–204

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

  1. L197
    have h32_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L198
    specialize le_trans h
  3. L199
    specialize le_trans x4
  4. L200
    specialize le_trans u
  5. L201
    apply le_trans
  6. L202
    exact h32t_total_bound
  7. L203
    exact h32_budget_growth
  8. L204
    exact h32_result

Library-wide reading audit

Original defined command ledger · 204 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(33,2 · 33,h)
    Exact native replay linehave hh_route : exists pa_b_hj32_h_32_route pa_c_hj32_h_32_route. ((forall pa_i_hj32_h_32_route_repeat. (exists pa_lt_hj32_h_32_route_repeat_bound. pa_lt_hj32_h_32_route_repeat_bound + S pa_i_hj32_h_32_route_repeat = 2 * 33) -> (((exists pa_h_hj32_h_32_route_repeat_decoded. pa_h_hj32_h_32_route_repeat_decoded + S (33) = S ((S (pa_i_hj32_h_32_route_repeat)) * pa_c_hj32_h_32_route)) /\ exists pa_q_hj32_h_32_route_repeat_decoded. pa_b_hj32_h_32_route = pa_q_hj32_h_32_route_repeat_decoded * S ((S (pa_i_hj32_h_32_route_repeat)) * pa_c_hj32_h_32_route) + (33)))) /\ (exists pa_u_hj32_h_32_route_product pa_v_hj32_h_32_route_product. ((((exists pa_h_hj32_h_32_route_product_start. pa_h_hj32_h_32_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_32_route_product)) /\ exists pa_q_hj32_h_32_route_product_start. pa_u_hj32_h_32_route_product = pa_q_hj32_h_32_route_product_start * S ((S (0)) * pa_v_hj32_h_32_route_product) + (1))) /\ ((((exists pa_h_hj32_h_32_route_product_terminal. pa_h_hj32_h_32_route_product_terminal + S (h) = S ((S (2 * 33)) * pa_v_hj32_h_32_route_product)) /\ exists pa_q_hj32_h_32_route_product_terminal. pa_u_hj32_h_32_route_product = pa_q_hj32_h_32_route_product_terminal * S ((S (2 * 33)) * pa_v_hj32_h_32_route_product) + (h))) /\ forall pa_i_hj32_h_32_route_product. (exists pa_lt_hj32_h_32_route_product_bound. pa_lt_hj32_h_32_route_product_bound + S pa_i_hj32_h_32_route_product = 2 * 33) -> exists pa_p_hj32_h_32_route_product pa_r_hj32_h_32_route_product pa_s_hj32_h_32_route_product. ((((exists pa_h_hj32_h_32_route_product_factor. pa_h_hj32_h_32_route_product_factor + S (pa_p_hj32_h_32_route_product) = S ((S (pa_i_hj32_h_32_route_product)) * pa_c_hj32_h_32_route)) /\ exists pa_q_hj32_h_32_route_product_factor. pa_b_hj32_h_32_route = pa_q_hj32_h_32_route_product_factor * S ((S (pa_i_hj32_h_32_route_product)) * pa_c_hj32_h_32_route) + (pa_p_hj32_h_32_route_product))) /\ ((((exists pa_h_hj32_h_32_route_product_partial. pa_h_hj32_h_32_route_product_partial + S (pa_r_hj32_h_32_route_product) = S ((S (pa_i_hj32_h_32_route_product)) * pa_v_hj32_h_32_route_product)) /\ exists pa_q_hj32_h_32_route_product_partial. pa_u_hj32_h_32_route_product = pa_q_hj32_h_32_route_product_partial * S ((S (pa_i_hj32_h_32_route_product)) * pa_v_hj32_h_32_route_product) + (pa_r_hj32_h_32_route_product))) /\ ((((exists pa_h_hj32_h_32_route_product_successor. pa_h_hj32_h_32_route_product_successor + S (pa_s_hj32_h_32_route_product) = S ((S (S pa_i_hj32_h_32_route_product)) * pa_v_hj32_h_32_route_product)) /\ exists pa_q_hj32_h_32_route_product_successor. pa_u_hj32_h_32_route_product = pa_q_hj32_h_32_route_product_successor * S ((S (S pa_i_hj32_h_32_route_product)) * pa_v_hj32_h_32_route_product) + (pa_s_hj32_h_32_route_product))) /\ pa_s_hj32_h_32_route_product = pa_r_hj32_h_32_route_product * pa_p_hj32_h_32_route_product)))))))
  9. 0009have hh_base : 32 + 1 = 33
  10. 0010norm_num
  11. 0011have hh_exponent : 2 * 32 + 2 = 2 * 33
  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 h32t_p3_exp : ∃ hj32_local_value_h32t_p3_exp. Pow(3,2 · 33,hj32_local_value_h32t_p3_exp)
    Exact native replay linehave h32t_p3_exp : exists hj32_local_value_h32t_p3_exp. (exists pa_b_hj32_local_total_h32t_p3_exp pa_c_hj32_local_total_h32t_p3_exp. ((forall pa_i_hj32_local_total_h32t_p3_exp_repeat. (exists pa_lt_hj32_local_total_h32t_p3_exp_repeat_bound. pa_lt_hj32_local_total_h32t_p3_exp_repeat_bound + S pa_i_hj32_local_total_h32t_p3_exp_repeat = 2 * 33) -> (((exists pa_h_hj32_local_total_h32t_p3_exp_repeat_decoded. pa_h_hj32_local_total_h32t_p3_exp_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_h32t_p3_exp_repeat)) * pa_c_hj32_local_total_h32t_p3_exp)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_repeat_decoded. pa_b_hj32_local_total_h32t_p3_exp = pa_q_hj32_local_total_h32t_p3_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p3_exp_repeat)) * pa_c_hj32_local_total_h32t_p3_exp) + (3)))) /\ (exists pa_u_hj32_local_total_h32t_p3_exp_product pa_v_hj32_local_total_h32t_p3_exp_product. ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_start. pa_h_hj32_local_total_h32t_p3_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p3_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_start. pa_u_hj32_local_total_h32t_p3_exp_product = pa_q_hj32_local_total_h32t_p3_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p3_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_terminal. pa_h_hj32_local_total_h32t_p3_exp_product_terminal + S (hj32_local_value_h32t_p3_exp) = S ((S (2 * 33)) * pa_v_hj32_local_total_h32t_p3_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_terminal. pa_u_hj32_local_total_h32t_p3_exp_product = pa_q_hj32_local_total_h32t_p3_exp_product_terminal * S ((S (2 * 33)) * pa_v_hj32_local_total_h32t_p3_exp_product) + (hj32_local_value_h32t_p3_exp))) /\ forall pa_i_hj32_local_total_h32t_p3_exp_product. (exists pa_lt_hj32_local_total_h32t_p3_exp_product_bound. pa_lt_hj32_local_total_h32t_p3_exp_product_bound + S pa_i_hj32_local_total_h32t_p3_exp_product = 2 * 33) -> exists pa_p_hj32_local_total_h32t_p3_exp_product pa_r_hj32_local_total_h32t_p3_exp_product pa_s_hj32_local_total_h32t_p3_exp_product. ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_factor. pa_h_hj32_local_total_h32t_p3_exp_product_factor + S (pa_p_hj32_local_total_h32t_p3_exp_product) = S ((S (pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_c_hj32_local_total_h32t_p3_exp)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_factor. pa_b_hj32_local_total_h32t_p3_exp = pa_q_hj32_local_total_h32t_p3_exp_product_factor * S ((S (pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_c_hj32_local_total_h32t_p3_exp) + (pa_p_hj32_local_total_h32t_p3_exp_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_partial. pa_h_hj32_local_total_h32t_p3_exp_product_partial + S (pa_r_hj32_local_total_h32t_p3_exp_product) = S ((S (pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_v_hj32_local_total_h32t_p3_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_partial. pa_u_hj32_local_total_h32t_p3_exp_product = pa_q_hj32_local_total_h32t_p3_exp_product_partial * S ((S (pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_v_hj32_local_total_h32t_p3_exp_product) + (pa_r_hj32_local_total_h32t_p3_exp_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_successor. pa_h_hj32_local_total_h32t_p3_exp_product_successor + S (pa_s_hj32_local_total_h32t_p3_exp_product) = S ((S (S pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_v_hj32_local_total_h32t_p3_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_successor. pa_u_hj32_local_total_h32t_p3_exp_product = pa_q_hj32_local_total_h32t_p3_exp_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_v_hj32_local_total_h32t_p3_exp_product) + (pa_s_hj32_local_total_h32t_p3_exp_product))) /\ pa_s_hj32_local_total_h32t_p3_exp_product = pa_r_hj32_local_total_h32t_p3_exp_product * pa_p_hj32_local_total_h32t_p3_exp_product))))))))
  21. 0021specialize htotal 3
  22. 0022specialize htotal 2 * 33
  23. 0023exact htotal
  24. 0024cases h32t_p3_exp
  25. 0025have h32t_p11_exp : ∃ hj32_local_value_h32t_p11_exp. Pow(11,2 · 33,hj32_local_value_h32t_p11_exp)
    Exact native replay linehave h32t_p11_exp : exists hj32_local_value_h32t_p11_exp. (exists pa_b_hj32_local_total_h32t_p11_exp pa_c_hj32_local_total_h32t_p11_exp. ((forall pa_i_hj32_local_total_h32t_p11_exp_repeat. (exists pa_lt_hj32_local_total_h32t_p11_exp_repeat_bound. pa_lt_hj32_local_total_h32t_p11_exp_repeat_bound + S pa_i_hj32_local_total_h32t_p11_exp_repeat = 2 * 33) -> (((exists pa_h_hj32_local_total_h32t_p11_exp_repeat_decoded. pa_h_hj32_local_total_h32t_p11_exp_repeat_decoded + S (11) = S ((S (pa_i_hj32_local_total_h32t_p11_exp_repeat)) * pa_c_hj32_local_total_h32t_p11_exp)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_repeat_decoded. pa_b_hj32_local_total_h32t_p11_exp = pa_q_hj32_local_total_h32t_p11_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p11_exp_repeat)) * pa_c_hj32_local_total_h32t_p11_exp) + (11)))) /\ (exists pa_u_hj32_local_total_h32t_p11_exp_product pa_v_hj32_local_total_h32t_p11_exp_product. ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_start. pa_h_hj32_local_total_h32t_p11_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_start. pa_u_hj32_local_total_h32t_p11_exp_product = pa_q_hj32_local_total_h32t_p11_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p11_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_terminal. pa_h_hj32_local_total_h32t_p11_exp_product_terminal + S (hj32_local_value_h32t_p11_exp) = S ((S (2 * 33)) * pa_v_hj32_local_total_h32t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_terminal. pa_u_hj32_local_total_h32t_p11_exp_product = pa_q_hj32_local_total_h32t_p11_exp_product_terminal * S ((S (2 * 33)) * pa_v_hj32_local_total_h32t_p11_exp_product) + (hj32_local_value_h32t_p11_exp))) /\ forall pa_i_hj32_local_total_h32t_p11_exp_product. (exists pa_lt_hj32_local_total_h32t_p11_exp_product_bound. pa_lt_hj32_local_total_h32t_p11_exp_product_bound + S pa_i_hj32_local_total_h32t_p11_exp_product = 2 * 33) -> exists pa_p_hj32_local_total_h32t_p11_exp_product pa_r_hj32_local_total_h32t_p11_exp_product pa_s_hj32_local_total_h32t_p11_exp_product. ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_factor. pa_h_hj32_local_total_h32t_p11_exp_product_factor + S (pa_p_hj32_local_total_h32t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_c_hj32_local_total_h32t_p11_exp)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_factor. pa_b_hj32_local_total_h32t_p11_exp = pa_q_hj32_local_total_h32t_p11_exp_product_factor * S ((S (pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_c_hj32_local_total_h32t_p11_exp) + (pa_p_hj32_local_total_h32t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_partial. pa_h_hj32_local_total_h32t_p11_exp_product_partial + S (pa_r_hj32_local_total_h32t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_v_hj32_local_total_h32t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_partial. pa_u_hj32_local_total_h32t_p11_exp_product = pa_q_hj32_local_total_h32t_p11_exp_product_partial * S ((S (pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_v_hj32_local_total_h32t_p11_exp_product) + (pa_r_hj32_local_total_h32t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_successor. pa_h_hj32_local_total_h32t_p11_exp_product_successor + S (pa_s_hj32_local_total_h32t_p11_exp_product) = S ((S (S pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_v_hj32_local_total_h32t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_successor. pa_u_hj32_local_total_h32t_p11_exp_product = pa_q_hj32_local_total_h32t_p11_exp_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_v_hj32_local_total_h32t_p11_exp_product) + (pa_s_hj32_local_total_h32t_p11_exp_product))) /\ pa_s_hj32_local_total_h32t_p11_exp_product = pa_r_hj32_local_total_h32t_p11_exp_product * pa_p_hj32_local_total_h32t_p11_exp_product))))))))
  26. 0026specialize htotal 11
  27. 0027specialize htotal 2 * 33
  28. 0028exact htotal
  29. 0029cases h32t_p11_exp
  30. 0030have h32t_product_graph : Pow(3 · 11,2 · 33,h)
    Exact native replay linehave h32t_product_graph : exists pa_b_hj32_local_product_h32t_product pa_c_hj32_local_product_h32t_product. ((forall pa_i_hj32_local_product_h32t_product_repeat. (exists pa_lt_hj32_local_product_h32t_product_repeat_bound. pa_lt_hj32_local_product_h32t_product_repeat_bound + S pa_i_hj32_local_product_h32t_product_repeat = 2 * 33) -> (((exists pa_h_hj32_local_product_h32t_product_repeat_decoded. pa_h_hj32_local_product_h32t_product_repeat_decoded + S (3 * 11) = S ((S (pa_i_hj32_local_product_h32t_product_repeat)) * pa_c_hj32_local_product_h32t_product)) /\ exists pa_q_hj32_local_product_h32t_product_repeat_decoded. pa_b_hj32_local_product_h32t_product = pa_q_hj32_local_product_h32t_product_repeat_decoded * S ((S (pa_i_hj32_local_product_h32t_product_repeat)) * pa_c_hj32_local_product_h32t_product) + (3 * 11)))) /\ (exists pa_u_hj32_local_product_h32t_product_product pa_v_hj32_local_product_h32t_product_product. ((((exists pa_h_hj32_local_product_h32t_product_product_start. pa_h_hj32_local_product_h32t_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_h32t_product_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_start. pa_u_hj32_local_product_h32t_product_product = pa_q_hj32_local_product_h32t_product_product_start * S ((S (0)) * pa_v_hj32_local_product_h32t_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_h32t_product_product_terminal. pa_h_hj32_local_product_h32t_product_product_terminal + S (h) = S ((S (2 * 33)) * pa_v_hj32_local_product_h32t_product_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_terminal. pa_u_hj32_local_product_h32t_product_product = pa_q_hj32_local_product_h32t_product_product_terminal * S ((S (2 * 33)) * pa_v_hj32_local_product_h32t_product_product) + (h))) /\ forall pa_i_hj32_local_product_h32t_product_product. (exists pa_lt_hj32_local_product_h32t_product_product_bound. pa_lt_hj32_local_product_h32t_product_product_bound + S pa_i_hj32_local_product_h32t_product_product = 2 * 33) -> exists pa_p_hj32_local_product_h32t_product_product pa_r_hj32_local_product_h32t_product_product pa_s_hj32_local_product_h32t_product_product. ((((exists pa_h_hj32_local_product_h32t_product_product_factor. pa_h_hj32_local_product_h32t_product_product_factor + S (pa_p_hj32_local_product_h32t_product_product) = S ((S (pa_i_hj32_local_product_h32t_product_product)) * pa_c_hj32_local_product_h32t_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_factor. pa_b_hj32_local_product_h32t_product = pa_q_hj32_local_product_h32t_product_product_factor * S ((S (pa_i_hj32_local_product_h32t_product_product)) * pa_c_hj32_local_product_h32t_product) + (pa_p_hj32_local_product_h32t_product_product))) /\ ((((exists pa_h_hj32_local_product_h32t_product_product_partial. pa_h_hj32_local_product_h32t_product_product_partial + S (pa_r_hj32_local_product_h32t_product_product) = S ((S (pa_i_hj32_local_product_h32t_product_product)) * pa_v_hj32_local_product_h32t_product_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_partial. pa_u_hj32_local_product_h32t_product_product = pa_q_hj32_local_product_h32t_product_product_partial * S ((S (pa_i_hj32_local_product_h32t_product_product)) * pa_v_hj32_local_product_h32t_product_product) + (pa_r_hj32_local_product_h32t_product_product))) /\ ((((exists pa_h_hj32_local_product_h32t_product_product_successor. pa_h_hj32_local_product_h32t_product_product_successor + S (pa_s_hj32_local_product_h32t_product_product) = S ((S (S pa_i_hj32_local_product_h32t_product_product)) * pa_v_hj32_local_product_h32t_product_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_successor. pa_u_hj32_local_product_h32t_product_product = pa_q_hj32_local_product_h32t_product_product_successor * S ((S (S pa_i_hj32_local_product_h32t_product_product)) * pa_v_hj32_local_product_h32t_product_product) + (pa_s_hj32_local_product_h32t_product_product))) /\ pa_s_hj32_local_product_h32t_product_product = pa_r_hj32_local_product_h32t_product_product * pa_p_hj32_local_product_h32t_product_product)))))))
  31. 0031have h32t_product_base : 3 * 11 = 33
  32. 0032norm_num
  33. 0033rewrite h32t_product_base
  34. 0034rewrite h32t_product_base
  35. 0035exact hh_route
  36. 0036have h32t_product : h = x * x1
  37. 0037specialize pow_mul_base 3
  38. 0038specialize pow_mul_base 11
  39. 0039specialize pow_mul_base 2 * 33
  40. 0040specialize pow_mul_base x
  41. 0041specialize pow_mul_base x1
  42. 0042specialize pow_mul_base h
  43. 0043apply pow_mul_base
  44. 0044exact h32t_p3_exp_witness
  45. 0045exact h32t_p11_exp_witness
  46. 0046exact h32t_product_graph
  47. 0047have h32t_three_power : Pow(3,5 · 13 + 1,x)
    Exact native replay linehave h32t_three_power : exists pa_b_hj32_h32t_three_power pa_c_hj32_h32t_three_power. ((forall pa_i_hj32_h32t_three_power_repeat. (exists pa_lt_hj32_h32t_three_power_repeat_bound. pa_lt_hj32_h32t_three_power_repeat_bound + S pa_i_hj32_h32t_three_power_repeat = 5 * 13 + 1) -> (((exists pa_h_hj32_h32t_three_power_repeat_decoded. pa_h_hj32_h32t_three_power_repeat_decoded + S (3) = S ((S (pa_i_hj32_h32t_three_power_repeat)) * pa_c_hj32_h32t_three_power)) /\ exists pa_q_hj32_h32t_three_power_repeat_decoded. pa_b_hj32_h32t_three_power = pa_q_hj32_h32t_three_power_repeat_decoded * S ((S (pa_i_hj32_h32t_three_power_repeat)) * pa_c_hj32_h32t_three_power) + (3)))) /\ (exists pa_u_hj32_h32t_three_power_product pa_v_hj32_h32t_three_power_product. ((((exists pa_h_hj32_h32t_three_power_product_start. pa_h_hj32_h32t_three_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_h32t_three_power_product)) /\ exists pa_q_hj32_h32t_three_power_product_start. pa_u_hj32_h32t_three_power_product = pa_q_hj32_h32t_three_power_product_start * S ((S (0)) * pa_v_hj32_h32t_three_power_product) + (1))) /\ ((((exists pa_h_hj32_h32t_three_power_product_terminal. pa_h_hj32_h32t_three_power_product_terminal + S (x) = S ((S (5 * 13 + 1)) * pa_v_hj32_h32t_three_power_product)) /\ exists pa_q_hj32_h32t_three_power_product_terminal. pa_u_hj32_h32t_three_power_product = pa_q_hj32_h32t_three_power_product_terminal * S ((S (5 * 13 + 1)) * pa_v_hj32_h32t_three_power_product) + (x))) /\ forall pa_i_hj32_h32t_three_power_product. (exists pa_lt_hj32_h32t_three_power_product_bound. pa_lt_hj32_h32t_three_power_product_bound + S pa_i_hj32_h32t_three_power_product = 5 * 13 + 1) -> exists pa_p_hj32_h32t_three_power_product pa_r_hj32_h32t_three_power_product pa_s_hj32_h32t_three_power_product. ((((exists pa_h_hj32_h32t_three_power_product_factor. pa_h_hj32_h32t_three_power_product_factor + S (pa_p_hj32_h32t_three_power_product) = S ((S (pa_i_hj32_h32t_three_power_product)) * pa_c_hj32_h32t_three_power)) /\ exists pa_q_hj32_h32t_three_power_product_factor. pa_b_hj32_h32t_three_power = pa_q_hj32_h32t_three_power_product_factor * S ((S (pa_i_hj32_h32t_three_power_product)) * pa_c_hj32_h32t_three_power) + (pa_p_hj32_h32t_three_power_product))) /\ ((((exists pa_h_hj32_h32t_three_power_product_partial. pa_h_hj32_h32t_three_power_product_partial + S (pa_r_hj32_h32t_three_power_product) = S ((S (pa_i_hj32_h32t_three_power_product)) * pa_v_hj32_h32t_three_power_product)) /\ exists pa_q_hj32_h32t_three_power_product_partial. pa_u_hj32_h32t_three_power_product = pa_q_hj32_h32t_three_power_product_partial * S ((S (pa_i_hj32_h32t_three_power_product)) * pa_v_hj32_h32t_three_power_product) + (pa_r_hj32_h32t_three_power_product))) /\ ((((exists pa_h_hj32_h32t_three_power_product_successor. pa_h_hj32_h32t_three_power_product_successor + S (pa_s_hj32_h32t_three_power_product) = S ((S (S pa_i_hj32_h32t_three_power_product)) * pa_v_hj32_h32t_three_power_product)) /\ exists pa_q_hj32_h32t_three_power_product_successor. pa_u_hj32_h32t_three_power_product = pa_q_hj32_h32t_three_power_product_successor * S ((S (S pa_i_hj32_h32t_three_power_product)) * pa_v_hj32_h32t_three_power_product) + (pa_s_hj32_h32t_three_power_product))) /\ pa_s_hj32_h32t_three_power_product = pa_r_hj32_h32t_three_power_product * pa_p_hj32_h32t_three_power_product)))))))
  48. 0048have h32t_three_exponent : 2 * 33 = 5 * 13 + 1
  49. 0049norm_num
  50. 0050rewrite <- h32t_three_exponent
  51. 0051rewrite <- h32t_three_exponent
  52. 0052rewrite <- h32t_three_exponent
  53. 0053rewrite <- h32t_three_exponent
  54. 0054exact h32t_p3_exp_witness
  55. 0055have h32t_p4_head : ∃ hj32_local_value_h32t_p4_head. Pow(4,4 · 13 + 1,hj32_local_value_h32t_p4_head)
    Exact native replay linehave h32t_p4_head : exists hj32_local_value_h32t_p4_head. (exists pa_b_hj32_local_total_h32t_p4_head pa_c_hj32_local_total_h32t_p4_head. ((forall pa_i_hj32_local_total_h32t_p4_head_repeat. (exists pa_lt_hj32_local_total_h32t_p4_head_repeat_bound. pa_lt_hj32_local_total_h32t_p4_head_repeat_bound + S pa_i_hj32_local_total_h32t_p4_head_repeat = 4 * 13 + 1) -> (((exists pa_h_hj32_local_total_h32t_p4_head_repeat_decoded. pa_h_hj32_local_total_h32t_p4_head_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h32t_p4_head_repeat)) * pa_c_hj32_local_total_h32t_p4_head)) /\ exists pa_q_hj32_local_total_h32t_p4_head_repeat_decoded. pa_b_hj32_local_total_h32t_p4_head = pa_q_hj32_local_total_h32t_p4_head_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p4_head_repeat)) * pa_c_hj32_local_total_h32t_p4_head) + (4)))) /\ (exists pa_u_hj32_local_total_h32t_p4_head_product pa_v_hj32_local_total_h32t_p4_head_product. ((((exists pa_h_hj32_local_total_h32t_p4_head_product_start. pa_h_hj32_local_total_h32t_p4_head_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p4_head_product)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_start. pa_u_hj32_local_total_h32t_p4_head_product = pa_q_hj32_local_total_h32t_p4_head_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p4_head_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_head_product_terminal. pa_h_hj32_local_total_h32t_p4_head_product_terminal + S (hj32_local_value_h32t_p4_head) = S ((S (4 * 13 + 1)) * pa_v_hj32_local_total_h32t_p4_head_product)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_terminal. pa_u_hj32_local_total_h32t_p4_head_product = pa_q_hj32_local_total_h32t_p4_head_product_terminal * S ((S (4 * 13 + 1)) * pa_v_hj32_local_total_h32t_p4_head_product) + (hj32_local_value_h32t_p4_head))) /\ forall pa_i_hj32_local_total_h32t_p4_head_product. (exists pa_lt_hj32_local_total_h32t_p4_head_product_bound. pa_lt_hj32_local_total_h32t_p4_head_product_bound + S pa_i_hj32_local_total_h32t_p4_head_product = 4 * 13 + 1) -> exists pa_p_hj32_local_total_h32t_p4_head_product pa_r_hj32_local_total_h32t_p4_head_product pa_s_hj32_local_total_h32t_p4_head_product. ((((exists pa_h_hj32_local_total_h32t_p4_head_product_factor. pa_h_hj32_local_total_h32t_p4_head_product_factor + S (pa_p_hj32_local_total_h32t_p4_head_product) = S ((S (pa_i_hj32_local_total_h32t_p4_head_product)) * pa_c_hj32_local_total_h32t_p4_head)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_factor. pa_b_hj32_local_total_h32t_p4_head = pa_q_hj32_local_total_h32t_p4_head_product_factor * S ((S (pa_i_hj32_local_total_h32t_p4_head_product)) * pa_c_hj32_local_total_h32t_p4_head) + (pa_p_hj32_local_total_h32t_p4_head_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_head_product_partial. pa_h_hj32_local_total_h32t_p4_head_product_partial + S (pa_r_hj32_local_total_h32t_p4_head_product) = S ((S (pa_i_hj32_local_total_h32t_p4_head_product)) * pa_v_hj32_local_total_h32t_p4_head_product)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_partial. pa_u_hj32_local_total_h32t_p4_head_product = pa_q_hj32_local_total_h32t_p4_head_product_partial * S ((S (pa_i_hj32_local_total_h32t_p4_head_product)) * pa_v_hj32_local_total_h32t_p4_head_product) + (pa_r_hj32_local_total_h32t_p4_head_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_head_product_successor. pa_h_hj32_local_total_h32t_p4_head_product_successor + S (pa_s_hj32_local_total_h32t_p4_head_product) = S ((S (S pa_i_hj32_local_total_h32t_p4_head_product)) * pa_v_hj32_local_total_h32t_p4_head_product)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_successor. pa_u_hj32_local_total_h32t_p4_head_product = pa_q_hj32_local_total_h32t_p4_head_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p4_head_product)) * pa_v_hj32_local_total_h32t_p4_head_product) + (pa_s_hj32_local_total_h32t_p4_head_product))) /\ pa_s_hj32_local_total_h32t_p4_head_product = pa_r_hj32_local_total_h32t_p4_head_product * pa_p_hj32_local_total_h32t_p4_head_product))))))))
  56. 0056specialize htotal 4
  57. 0057specialize htotal 4 * 13 + 1
  58. 0058exact htotal
  59. 0059cases h32t_p4_head
  60. 0060have h32t_three_bound : Le(x,x2)
    Exact native replay linehave h32t_three_bound : exists bqb_le_gap_hj32_h32t_three_bound. bqb_le_gap_hj32_h32t_three_bound + (x) = (x2)
  61. 0061specialize pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total 13
  62. 0062specialize pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total x
  63. 0063specialize pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total x2
  64. 0064apply pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total
  65. 0065exact htotal
  66. 0066exact h32t_three_power
  67. 0067exact h32t_p4_head_witness
  68. 0068have h32t_p4_tail : ∃ hj32_local_value_h32t_p4_tail. Pow(4,4 · 29,hj32_local_value_h32t_p4_tail)
    Exact native replay linehave h32t_p4_tail : exists hj32_local_value_h32t_p4_tail. (exists pa_b_hj32_local_total_h32t_p4_tail pa_c_hj32_local_total_h32t_p4_tail. ((forall pa_i_hj32_local_total_h32t_p4_tail_repeat. (exists pa_lt_hj32_local_total_h32t_p4_tail_repeat_bound. pa_lt_hj32_local_total_h32t_p4_tail_repeat_bound + S pa_i_hj32_local_total_h32t_p4_tail_repeat = 4 * 29) -> (((exists pa_h_hj32_local_total_h32t_p4_tail_repeat_decoded. pa_h_hj32_local_total_h32t_p4_tail_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h32t_p4_tail_repeat)) * pa_c_hj32_local_total_h32t_p4_tail)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_repeat_decoded. pa_b_hj32_local_total_h32t_p4_tail = pa_q_hj32_local_total_h32t_p4_tail_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p4_tail_repeat)) * pa_c_hj32_local_total_h32t_p4_tail) + (4)))) /\ (exists pa_u_hj32_local_total_h32t_p4_tail_product pa_v_hj32_local_total_h32t_p4_tail_product. ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_start. pa_h_hj32_local_total_h32t_p4_tail_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_start. pa_u_hj32_local_total_h32t_p4_tail_product = pa_q_hj32_local_total_h32t_p4_tail_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p4_tail_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_terminal. pa_h_hj32_local_total_h32t_p4_tail_product_terminal + S (hj32_local_value_h32t_p4_tail) = S ((S (4 * 29)) * pa_v_hj32_local_total_h32t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_terminal. pa_u_hj32_local_total_h32t_p4_tail_product = pa_q_hj32_local_total_h32t_p4_tail_product_terminal * S ((S (4 * 29)) * pa_v_hj32_local_total_h32t_p4_tail_product) + (hj32_local_value_h32t_p4_tail))) /\ forall pa_i_hj32_local_total_h32t_p4_tail_product. (exists pa_lt_hj32_local_total_h32t_p4_tail_product_bound. pa_lt_hj32_local_total_h32t_p4_tail_product_bound + S pa_i_hj32_local_total_h32t_p4_tail_product = 4 * 29) -> exists pa_p_hj32_local_total_h32t_p4_tail_product pa_r_hj32_local_total_h32t_p4_tail_product pa_s_hj32_local_total_h32t_p4_tail_product. ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_factor. pa_h_hj32_local_total_h32t_p4_tail_product_factor + S (pa_p_hj32_local_total_h32t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_c_hj32_local_total_h32t_p4_tail)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_factor. pa_b_hj32_local_total_h32t_p4_tail = pa_q_hj32_local_total_h32t_p4_tail_product_factor * S ((S (pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_c_hj32_local_total_h32t_p4_tail) + (pa_p_hj32_local_total_h32t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_partial. pa_h_hj32_local_total_h32t_p4_tail_product_partial + S (pa_r_hj32_local_total_h32t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_v_hj32_local_total_h32t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_partial. pa_u_hj32_local_total_h32t_p4_tail_product = pa_q_hj32_local_total_h32t_p4_tail_product_partial * S ((S (pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_v_hj32_local_total_h32t_p4_tail_product) + (pa_r_hj32_local_total_h32t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_successor. pa_h_hj32_local_total_h32t_p4_tail_product_successor + S (pa_s_hj32_local_total_h32t_p4_tail_product) = S ((S (S pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_v_hj32_local_total_h32t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_successor. pa_u_hj32_local_total_h32t_p4_tail_product = pa_q_hj32_local_total_h32t_p4_tail_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_v_hj32_local_total_h32t_p4_tail_product) + (pa_s_hj32_local_total_h32t_p4_tail_product))) /\ pa_s_hj32_local_total_h32t_p4_tail_product = pa_r_hj32_local_total_h32t_p4_tail_product * pa_p_hj32_local_total_h32t_p4_tail_product))))))))
  69. 0069specialize htotal 4
  70. 0070specialize htotal 4 * 29
  71. 0071exact htotal
  72. 0072cases h32t_p4_tail
  73. 0073have h32t_tail_power : Pow(4,14 · 8 + 3 + 1,x3)
    Exact native replay linehave h32t_tail_power : exists pa_b_hj32_h32t_tail_power pa_c_hj32_h32t_tail_power. ((forall pa_i_hj32_h32t_tail_power_repeat. (exists pa_lt_hj32_h32t_tail_power_repeat_bound. pa_lt_hj32_h32t_tail_power_repeat_bound + S pa_i_hj32_h32t_tail_power_repeat = (14 * 8 + 3) + 1) -> (((exists pa_h_hj32_h32t_tail_power_repeat_decoded. pa_h_hj32_h32t_tail_power_repeat_decoded + S (4) = S ((S (pa_i_hj32_h32t_tail_power_repeat)) * pa_c_hj32_h32t_tail_power)) /\ exists pa_q_hj32_h32t_tail_power_repeat_decoded. pa_b_hj32_h32t_tail_power = pa_q_hj32_h32t_tail_power_repeat_decoded * S ((S (pa_i_hj32_h32t_tail_power_repeat)) * pa_c_hj32_h32t_tail_power) + (4)))) /\ (exists pa_u_hj32_h32t_tail_power_product pa_v_hj32_h32t_tail_power_product. ((((exists pa_h_hj32_h32t_tail_power_product_start. pa_h_hj32_h32t_tail_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_h32t_tail_power_product)) /\ exists pa_q_hj32_h32t_tail_power_product_start. pa_u_hj32_h32t_tail_power_product = pa_q_hj32_h32t_tail_power_product_start * S ((S (0)) * pa_v_hj32_h32t_tail_power_product) + (1))) /\ ((((exists pa_h_hj32_h32t_tail_power_product_terminal. pa_h_hj32_h32t_tail_power_product_terminal + S (x3) = S ((S ((14 * 8 + 3) + 1)) * pa_v_hj32_h32t_tail_power_product)) /\ exists pa_q_hj32_h32t_tail_power_product_terminal. pa_u_hj32_h32t_tail_power_product = pa_q_hj32_h32t_tail_power_product_terminal * S ((S ((14 * 8 + 3) + 1)) * pa_v_hj32_h32t_tail_power_product) + (x3))) /\ forall pa_i_hj32_h32t_tail_power_product. (exists pa_lt_hj32_h32t_tail_power_product_bound. pa_lt_hj32_h32t_tail_power_product_bound + S pa_i_hj32_h32t_tail_power_product = (14 * 8 + 3) + 1) -> exists pa_p_hj32_h32t_tail_power_product pa_r_hj32_h32t_tail_power_product pa_s_hj32_h32t_tail_power_product. ((((exists pa_h_hj32_h32t_tail_power_product_factor. pa_h_hj32_h32t_tail_power_product_factor + S (pa_p_hj32_h32t_tail_power_product) = S ((S (pa_i_hj32_h32t_tail_power_product)) * pa_c_hj32_h32t_tail_power)) /\ exists pa_q_hj32_h32t_tail_power_product_factor. pa_b_hj32_h32t_tail_power = pa_q_hj32_h32t_tail_power_product_factor * S ((S (pa_i_hj32_h32t_tail_power_product)) * pa_c_hj32_h32t_tail_power) + (pa_p_hj32_h32t_tail_power_product))) /\ ((((exists pa_h_hj32_h32t_tail_power_product_partial. pa_h_hj32_h32t_tail_power_product_partial + S (pa_r_hj32_h32t_tail_power_product) = S ((S (pa_i_hj32_h32t_tail_power_product)) * pa_v_hj32_h32t_tail_power_product)) /\ exists pa_q_hj32_h32t_tail_power_product_partial. pa_u_hj32_h32t_tail_power_product = pa_q_hj32_h32t_tail_power_product_partial * S ((S (pa_i_hj32_h32t_tail_power_product)) * pa_v_hj32_h32t_tail_power_product) + (pa_r_hj32_h32t_tail_power_product))) /\ ((((exists pa_h_hj32_h32t_tail_power_product_successor. pa_h_hj32_h32t_tail_power_product_successor + S (pa_s_hj32_h32t_tail_power_product) = S ((S (S pa_i_hj32_h32t_tail_power_product)) * pa_v_hj32_h32t_tail_power_product)) /\ exists pa_q_hj32_h32t_tail_power_product_successor. pa_u_hj32_h32t_tail_power_product = pa_q_hj32_h32t_tail_power_product_successor * S ((S (S pa_i_hj32_h32t_tail_power_product)) * pa_v_hj32_h32t_tail_power_product) + (pa_s_hj32_h32t_tail_power_product))) /\ pa_s_hj32_h32t_tail_power_product = pa_r_hj32_h32t_tail_power_product * pa_p_hj32_h32t_tail_power_product)))))))
  74. 0074have h32t_tail_exponent : (14 * 8 + 3) + 1 = 4 * 29
  75. 0075norm_num
  76. 0076rewrite h32t_tail_exponent
  77. 0077rewrite h32t_tail_exponent
  78. 0078rewrite h32t_tail_exponent
  79. 0079rewrite h32t_tail_exponent
  80. 0080exact h32t_p4_tail_witness
  81. 0081have h32t_parity : 7 * 33 = 2 * (14 * 8 + 3) + 1
  82. 0082have h32t_parity_left : 7 * 33 = 28 * 8 + 7
  83. 0083have h32t_root : 33 = 4 * 8 + 1
  84. 0084norm_num
  85. 0085rewrite h32t_root
  86. 0086have h32t_left_distrib : 7 * (4 * 8 + 1) = 7 * (4 * 8) + 7 * 1
  87. 0087specialize mul_add 7
  88. 0088specialize mul_add (4 * 8)
  89. 0089specialize mul_add 1
  90. 0090apply mul_add
  91. 0091rewrite h32t_left_distrib
  92. 0092have h32t_left_assoc : 7 * (4 * 8) = (7 * 4) * 8
  93. 0093symm
  94. 0094specialize mul_assoc 7
  95. 0095specialize mul_assoc 4
  96. 0096specialize mul_assoc 8
  97. 0097apply mul_assoc
  98. 0098rewrite h32t_left_assoc
  99. 0099have h32t_twenty_eight : 7 * 4 = 28
  100. 0100norm_num
  101. 0101rewrite h32t_twenty_eight
  102. 0102have h32t_seven : 7 * 1 = 7
  103. 0103norm_num
  104. 0104rewrite h32t_seven
  105. 0105refl
  106. 0106have h32t_parity_right : 2 * (14 * 8 + 3) + 1 = 28 * 8 + 7
  107. 0107have h32t_right_distrib : 2 * (14 * 8 + 3) = 2 * (14 * 8) + 2 * 3
  108. 0108specialize mul_add 2
  109. 0109specialize mul_add (14 * 8)
  110. 0110specialize mul_add 3
  111. 0111apply mul_add
  112. 0112rewrite h32t_right_distrib
  113. 0113have h32t_right_assoc : 2 * (14 * 8) = (2 * 14) * 8
  114. 0114symm
  115. 0115specialize mul_assoc 2
  116. 0116specialize mul_assoc 14
  117. 0117specialize mul_assoc 8
  118. 0118apply mul_assoc
  119. 0119rewrite h32t_right_assoc
  120. 0120have h32t_right_twenty_eight : 2 * 14 = 28
  121. 0121norm_num
  122. 0122rewrite h32t_right_twenty_eight
  123. 0123have h32t_right_assoc_add : (28 * 8 + 2 * 3) + 1 = 28 * 8 + (2 * 3 + 1)
  124. 0124specialize add_assoc (28 * 8)
  125. 0125specialize add_assoc (2 * 3)
  126. 0126specialize add_assoc 1
  127. 0127apply add_assoc
  128. 0128rewrite h32t_right_assoc_add
  129. 0129have h32t_right_seven : 2 * 3 + 1 = 7
  130. 0130norm_num
  131. 0131rewrite h32t_right_seven
  132. 0132refl
  133. 0133trans 28 * 8 + 7
  134. 0134exact h32t_parity_left
  135. 0135symm
  136. 0136exact h32t_parity_right
  137. 0137have h32t_eleven_bound : Le(x1,x3)
    Exact native replay linehave h32t_eleven_bound : exists bqb_le_gap_hj32_h32t_eleven_bound. bqb_le_gap_hj32_h32t_eleven_bound + (x1) = (x3)
  138. 0138specialize pow_eleven_double_block_le_pow_four_odd_from_total 33
  139. 0139specialize pow_eleven_double_block_le_pow_four_odd_from_total (14 * 8 + 3)
  140. 0140specialize pow_eleven_double_block_le_pow_four_odd_from_total x1
  141. 0141specialize pow_eleven_double_block_le_pow_four_odd_from_total x3
  142. 0142apply pow_eleven_double_block_le_pow_four_odd_from_total
  143. 0143exact htotal
  144. 0144exact h32t_parity
  145. 0145exact h32t_p11_exp_witness
  146. 0146exact h32t_tail_power
  147. 0147have h32t_total_bound : Le(x · x1,x2 · x3)
    Exact native replay linehave h32t_total_bound : exists bqb_le_gap_hj32_local_product_bound_h32t_total_bound. bqb_le_gap_hj32_local_product_bound_h32t_total_bound + (x * x1) = (x2 * x3)
  148. 0148specialize mul_le_mul x
  149. 0149specialize mul_le_mul x2
  150. 0150specialize mul_le_mul x1
  151. 0151specialize mul_le_mul x3
  152. 0152apply mul_le_mul
  153. 0153exact h32t_three_bound
  154. 0154exact h32t_eleven_bound
  155. 0155have h32t_p4_budget : ∃ hj32_local_value_h32t_p4_budget. Pow(4,4 · 13 + 1 + 4 · 29,hj32_local_value_h32t_p4_budget)
    Exact native replay linehave h32t_p4_budget : exists hj32_local_value_h32t_p4_budget. (exists pa_b_hj32_local_total_h32t_p4_budget pa_c_hj32_local_total_h32t_p4_budget. ((forall pa_i_hj32_local_total_h32t_p4_budget_repeat. (exists pa_lt_hj32_local_total_h32t_p4_budget_repeat_bound. pa_lt_hj32_local_total_h32t_p4_budget_repeat_bound + S pa_i_hj32_local_total_h32t_p4_budget_repeat = (4 * 13 + 1) + 4 * 29) -> (((exists pa_h_hj32_local_total_h32t_p4_budget_repeat_decoded. pa_h_hj32_local_total_h32t_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h32t_p4_budget_repeat)) * pa_c_hj32_local_total_h32t_p4_budget)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_repeat_decoded. pa_b_hj32_local_total_h32t_p4_budget = pa_q_hj32_local_total_h32t_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p4_budget_repeat)) * pa_c_hj32_local_total_h32t_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h32t_p4_budget_product pa_v_hj32_local_total_h32t_p4_budget_product. ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_start. pa_h_hj32_local_total_h32t_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_start. pa_u_hj32_local_total_h32t_p4_budget_product = pa_q_hj32_local_total_h32t_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_terminal. pa_h_hj32_local_total_h32t_p4_budget_product_terminal + S (hj32_local_value_h32t_p4_budget) = S ((S ((4 * 13 + 1) + 4 * 29)) * pa_v_hj32_local_total_h32t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_terminal. pa_u_hj32_local_total_h32t_p4_budget_product = pa_q_hj32_local_total_h32t_p4_budget_product_terminal * S ((S ((4 * 13 + 1) + 4 * 29)) * pa_v_hj32_local_total_h32t_p4_budget_product) + (hj32_local_value_h32t_p4_budget))) /\ forall pa_i_hj32_local_total_h32t_p4_budget_product. (exists pa_lt_hj32_local_total_h32t_p4_budget_product_bound. pa_lt_hj32_local_total_h32t_p4_budget_product_bound + S pa_i_hj32_local_total_h32t_p4_budget_product = (4 * 13 + 1) + 4 * 29) -> exists pa_p_hj32_local_total_h32t_p4_budget_product pa_r_hj32_local_total_h32t_p4_budget_product pa_s_hj32_local_total_h32t_p4_budget_product. ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_factor. pa_h_hj32_local_total_h32t_p4_budget_product_factor + S (pa_p_hj32_local_total_h32t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_c_hj32_local_total_h32t_p4_budget)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_factor. pa_b_hj32_local_total_h32t_p4_budget = pa_q_hj32_local_total_h32t_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_c_hj32_local_total_h32t_p4_budget) + (pa_p_hj32_local_total_h32t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_partial. pa_h_hj32_local_total_h32t_p4_budget_product_partial + S (pa_r_hj32_local_total_h32t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_v_hj32_local_total_h32t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_partial. pa_u_hj32_local_total_h32t_p4_budget_product = pa_q_hj32_local_total_h32t_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_v_hj32_local_total_h32t_p4_budget_product) + (pa_r_hj32_local_total_h32t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_successor. pa_h_hj32_local_total_h32t_p4_budget_product_successor + S (pa_s_hj32_local_total_h32t_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_v_hj32_local_total_h32t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_successor. pa_u_hj32_local_total_h32t_p4_budget_product = pa_q_hj32_local_total_h32t_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_v_hj32_local_total_h32t_p4_budget_product) + (pa_s_hj32_local_total_h32t_p4_budget_product))) /\ pa_s_hj32_local_total_h32t_p4_budget_product = pa_r_hj32_local_total_h32t_p4_budget_product * pa_p_hj32_local_total_h32t_p4_budget_product))))))))
  156. 0156specialize htotal 4
  157. 0157specialize htotal (4 * 13 + 1) + 4 * 29
  158. 0158exact htotal
  159. 0159cases h32t_p4_budget
  160. 0160have h32t_budget_product : x4 = x2 * x3
  161. 0161specialize pow_add 4
  162. 0162specialize pow_add 4 * 13 + 1
  163. 0163specialize pow_add 4 * 29
  164. 0164specialize pow_add (4 * 13 + 1) + 4 * 29
  165. 0165specialize pow_add x2
  166. 0166specialize pow_add x3
  167. 0167specialize pow_add x4
  168. 0168apply pow_add
  169. 0169refl
  170. 0170exact h32t_p4_head_witness
  171. 0171exact h32t_p4_tail_witness
  172. 0172exact h32t_p4_budget_witness
  173. 0173rewrite <- h32t_product at h32t_total_bound
  174. 0174rewrite <- h32t_budget_product at h32t_total_bound
  175. 0175have hscaled : Le(6 · (4 · 13 + 1 + 4 · 29),32 · 32)
    Exact native replay linehave hscaled : exists bqb_le_gap_hj32_scaled_budget_root_32. bqb_le_gap_hj32_scaled_budget_root_32 + (6 * ((4 * 13 + 1) + 4 * 29)) = (32 * 32)
  176. 0176apply bertrand_scaled_budget_root_32
  177. 0177have hbudget_exponent : Le(4 · 13 + 1 + 4 · 29,e)
    Exact native replay linehave hbudget_exponent : exists bqb_le_gap_hj32_h_32_budget_exponent. bqb_le_gap_hj32_h_32_budget_exponent + ((4 * 13 + 1) + 4 * 29) = (e)
  178. 0178specialize ceil_div_six_budget_of_scaled_le (32 * 32)
  179. 0179specialize ceil_div_six_budget_of_scaled_le ((4 * 13 + 1) + 4 * 29)
  180. 0180specialize ceil_div_six_budget_of_scaled_le e
  181. 0181apply ceil_div_six_budget_of_scaled_le
  182. 0182exact hceiling
  183. 0183exact hscaled
  184. 0184have h32_budget_growth : Le(x4,u)
    Exact native replay linehave h32_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h32_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h32_budget_growth + (x4) = (u)
  185. 0185specialize pow_exponent_monotone_from_total 4
  186. 0186specialize pow_exponent_monotone_from_total (4 * 13 + 1) + 4 * 29
  187. 0187specialize pow_exponent_monotone_from_total e
  188. 0188specialize pow_exponent_monotone_from_total x4
  189. 0189specialize pow_exponent_monotone_from_total u
  190. 0190apply pow_exponent_monotone_from_total
  191. 0191exact htotal
  192. 0192exists 3
  193. 0193norm_num
  194. 0194exact hbudget_exponent
  195. 0195exact h32t_p4_budget_witness
  196. 0196exact hu
  197. 0197have h32_result : Le(h,u)
    Exact native replay linehave h32_result : exists bqb_le_gap_hj32_local_trans_bound_h32_result. bqb_le_gap_hj32_local_trans_bound_h32_result + (h) = (u)
  198. 0198specialize le_trans h
  199. 0199specialize le_trans x4
  200. 0200specialize le_trans u
  201. 0201apply le_trans
  202. 0202exact h32t_total_bound
  203. 0203exact h32_budget_growth
  204. 0204exact h32_result