BT00WS · Bertrand theorem

bertrand_h_root_35_from_total

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

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

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(35 · 35,e) → Pow(35 + 1,2 · 35 + 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_35 bpt_e_hj32_h_root_35. exists bpt_x_hj32_h_root_35. (exists ff_b_bpt_value_hj32_h_root_35 ff_c_bpt_value_hj32_h_root_35. ((forall ff_i_bpt_value_hj32_h_root_35_repeat. (exists ff_lt_bpt_value_hj32_h_root_35_repeat_bound. ff_lt_bpt_value_hj32_h_root_35_repeat_bound + S ff_i_bpt_value_hj32_h_root_35_repeat = bpt_e_hj32_h_root_35) -> (((exists ff_h_bpt_value_hj32_h_root_35_repeat_decoded. ff_h_bpt_value_hj32_h_root_35_repeat_decoded + S (bpt_a_hj32_h_root_35) = S ((S (ff_i_bpt_value_hj32_h_root_35_repeat)) * ff_c_bpt_value_hj32_h_root_35)) /\ exists ff_q_bpt_value_hj32_h_root_35_repeat_decoded. ff_b_bpt_value_hj32_h_root_35 = ff_q_bpt_value_hj32_h_root_35_repeat_decoded * S ((S (ff_i_bpt_value_hj32_h_root_35_repeat)) * ff_c_bpt_value_hj32_h_root_35) + (bpt_a_hj32_h_root_35)))) /\ (exists ff_u_bpt_value_hj32_h_root_35_product ff_v_bpt_value_hj32_h_root_35_product. ((((exists ff_h_bpt_value_hj32_h_root_35_product_start. ff_h_bpt_value_hj32_h_root_35_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_h_root_35_product)) /\ exists ff_q_bpt_value_hj32_h_root_35_product_start. ff_u_bpt_value_hj32_h_root_35_product = ff_q_bpt_value_hj32_h_root_35_product_start * S ((S (0)) * ff_v_bpt_value_hj32_h_root_35_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_h_root_35_product_terminal. ff_h_bpt_value_hj32_h_root_35_product_terminal + S (bpt_x_hj32_h_root_35) = S ((S (bpt_e_hj32_h_root_35)) * ff_v_bpt_value_hj32_h_root_35_product)) /\ exists ff_q_bpt_value_hj32_h_root_35_product_terminal. ff_u_bpt_value_hj32_h_root_35_product = ff_q_bpt_value_hj32_h_root_35_product_terminal * S ((S (bpt_e_hj32_h_root_35)) * ff_v_bpt_value_hj32_h_root_35_product) + (bpt_x_hj32_h_root_35))) /\ forall ff_i_bpt_value_hj32_h_root_35_product. (exists ff_lt_bpt_value_hj32_h_root_35_product_bound. ff_lt_bpt_value_hj32_h_root_35_product_bound + S ff_i_bpt_value_hj32_h_root_35_product = bpt_e_hj32_h_root_35) -> exists ff_p_bpt_value_hj32_h_root_35_product ff_r_bpt_value_hj32_h_root_35_product ff_s_bpt_value_hj32_h_root_35_product. ((((exists ff_h_bpt_value_hj32_h_root_35_product_factor. ff_h_bpt_value_hj32_h_root_35_product_factor + S (ff_p_bpt_value_hj32_h_root_35_product) = S ((S (ff_i_bpt_value_hj32_h_root_35_product)) * ff_c_bpt_value_hj32_h_root_35)) /\ exists ff_q_bpt_value_hj32_h_root_35_product_factor. ff_b_bpt_value_hj32_h_root_35 = ff_q_bpt_value_hj32_h_root_35_product_factor * S ((S (ff_i_bpt_value_hj32_h_root_35_product)) * ff_c_bpt_value_hj32_h_root_35) + (ff_p_bpt_value_hj32_h_root_35_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_35_product_partial. ff_h_bpt_value_hj32_h_root_35_product_partial + S (ff_r_bpt_value_hj32_h_root_35_product) = S ((S (ff_i_bpt_value_hj32_h_root_35_product)) * ff_v_bpt_value_hj32_h_root_35_product)) /\ exists ff_q_bpt_value_hj32_h_root_35_product_partial. ff_u_bpt_value_hj32_h_root_35_product = ff_q_bpt_value_hj32_h_root_35_product_partial * S ((S (ff_i_bpt_value_hj32_h_root_35_product)) * ff_v_bpt_value_hj32_h_root_35_product) + (ff_r_bpt_value_hj32_h_root_35_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_35_product_successor. ff_h_bpt_value_hj32_h_root_35_product_successor + S (ff_s_bpt_value_hj32_h_root_35_product) = S ((S (S ff_i_bpt_value_hj32_h_root_35_product)) * ff_v_bpt_value_hj32_h_root_35_product)) /\ exists ff_q_bpt_value_hj32_h_root_35_product_successor. ff_u_bpt_value_hj32_h_root_35_product = ff_q_bpt_value_hj32_h_root_35_product_successor * S ((S (S ff_i_bpt_value_hj32_h_root_35_product)) * ff_v_bpt_value_hj32_h_root_35_product) + (ff_s_bpt_value_hj32_h_root_35_product))) /\ ff_s_bpt_value_hj32_h_root_35_product = ff_r_bpt_value_hj32_h_root_35_product * ff_p_bpt_value_hj32_h_root_35_product))))))))) -> (((exists bcs_lower_gap_hj32_h_root_35_ceiling. bcs_lower_gap_hj32_h_root_35_ceiling + (35 * 35) = 6 * (e)) /\ exists bcs_upper_gap_hj32_h_root_35_ceiling. bcs_upper_gap_hj32_h_root_35_ceiling + S (6 * (e)) = (35 * 35) + 6)) -> (exists pa_b_hj32_h_root_35_h pa_c_hj32_h_root_35_h. ((forall pa_i_hj32_h_root_35_h_repeat. (exists pa_lt_hj32_h_root_35_h_repeat_bound. pa_lt_hj32_h_root_35_h_repeat_bound + S pa_i_hj32_h_root_35_h_repeat = 2 * 35 + 2) -> (((exists pa_h_hj32_h_root_35_h_repeat_decoded. pa_h_hj32_h_root_35_h_repeat_decoded + S (35 + 1) = S ((S (pa_i_hj32_h_root_35_h_repeat)) * pa_c_hj32_h_root_35_h)) /\ exists pa_q_hj32_h_root_35_h_repeat_decoded. pa_b_hj32_h_root_35_h = pa_q_hj32_h_root_35_h_repeat_decoded * S ((S (pa_i_hj32_h_root_35_h_repeat)) * pa_c_hj32_h_root_35_h) + (35 + 1)))) /\ (exists pa_u_hj32_h_root_35_h_product pa_v_hj32_h_root_35_h_product. ((((exists pa_h_hj32_h_root_35_h_product_start. pa_h_hj32_h_root_35_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_35_h_product)) /\ exists pa_q_hj32_h_root_35_h_product_start. pa_u_hj32_h_root_35_h_product = pa_q_hj32_h_root_35_h_product_start * S ((S (0)) * pa_v_hj32_h_root_35_h_product) + (1))) /\ ((((exists pa_h_hj32_h_root_35_h_product_terminal. pa_h_hj32_h_root_35_h_product_terminal + S (h) = S ((S (2 * 35 + 2)) * pa_v_hj32_h_root_35_h_product)) /\ exists pa_q_hj32_h_root_35_h_product_terminal. pa_u_hj32_h_root_35_h_product = pa_q_hj32_h_root_35_h_product_terminal * S ((S (2 * 35 + 2)) * pa_v_hj32_h_root_35_h_product) + (h))) /\ forall pa_i_hj32_h_root_35_h_product. (exists pa_lt_hj32_h_root_35_h_product_bound. pa_lt_hj32_h_root_35_h_product_bound + S pa_i_hj32_h_root_35_h_product = 2 * 35 + 2) -> exists pa_p_hj32_h_root_35_h_product pa_r_hj32_h_root_35_h_product pa_s_hj32_h_root_35_h_product. ((((exists pa_h_hj32_h_root_35_h_product_factor. pa_h_hj32_h_root_35_h_product_factor + S (pa_p_hj32_h_root_35_h_product) = S ((S (pa_i_hj32_h_root_35_h_product)) * pa_c_hj32_h_root_35_h)) /\ exists pa_q_hj32_h_root_35_h_product_factor. pa_b_hj32_h_root_35_h = pa_q_hj32_h_root_35_h_product_factor * S ((S (pa_i_hj32_h_root_35_h_product)) * pa_c_hj32_h_root_35_h) + (pa_p_hj32_h_root_35_h_product))) /\ ((((exists pa_h_hj32_h_root_35_h_product_partial. pa_h_hj32_h_root_35_h_product_partial + S (pa_r_hj32_h_root_35_h_product) = S ((S (pa_i_hj32_h_root_35_h_product)) * pa_v_hj32_h_root_35_h_product)) /\ exists pa_q_hj32_h_root_35_h_product_partial. pa_u_hj32_h_root_35_h_product = pa_q_hj32_h_root_35_h_product_partial * S ((S (pa_i_hj32_h_root_35_h_product)) * pa_v_hj32_h_root_35_h_product) + (pa_r_hj32_h_root_35_h_product))) /\ ((((exists pa_h_hj32_h_root_35_h_product_successor. pa_h_hj32_h_root_35_h_product_successor + S (pa_s_hj32_h_root_35_h_product) = S ((S (S pa_i_hj32_h_root_35_h_product)) * pa_v_hj32_h_root_35_h_product)) /\ exists pa_q_hj32_h_root_35_h_product_successor. pa_u_hj32_h_root_35_h_product = pa_q_hj32_h_root_35_h_product_successor * S ((S (S pa_i_hj32_h_root_35_h_product)) * pa_v_hj32_h_root_35_h_product) + (pa_s_hj32_h_root_35_h_product))) /\ pa_s_hj32_h_root_35_h_product = pa_r_hj32_h_root_35_h_product * pa_p_hj32_h_root_35_h_product)))))))) -> (exists pa_b_hj32_h_root_35_u pa_c_hj32_h_root_35_u. ((forall pa_i_hj32_h_root_35_u_repeat. (exists pa_lt_hj32_h_root_35_u_repeat_bound. pa_lt_hj32_h_root_35_u_repeat_bound + S pa_i_hj32_h_root_35_u_repeat = e) -> (((exists pa_h_hj32_h_root_35_u_repeat_decoded. pa_h_hj32_h_root_35_u_repeat_decoded + S (4) = S ((S (pa_i_hj32_h_root_35_u_repeat)) * pa_c_hj32_h_root_35_u)) /\ exists pa_q_hj32_h_root_35_u_repeat_decoded. pa_b_hj32_h_root_35_u = pa_q_hj32_h_root_35_u_repeat_decoded * S ((S (pa_i_hj32_h_root_35_u_repeat)) * pa_c_hj32_h_root_35_u) + (4)))) /\ (exists pa_u_hj32_h_root_35_u_product pa_v_hj32_h_root_35_u_product. ((((exists pa_h_hj32_h_root_35_u_product_start. pa_h_hj32_h_root_35_u_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_35_u_product)) /\ exists pa_q_hj32_h_root_35_u_product_start. pa_u_hj32_h_root_35_u_product = pa_q_hj32_h_root_35_u_product_start * S ((S (0)) * pa_v_hj32_h_root_35_u_product) + (1))) /\ ((((exists pa_h_hj32_h_root_35_u_product_terminal. pa_h_hj32_h_root_35_u_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_h_root_35_u_product)) /\ exists pa_q_hj32_h_root_35_u_product_terminal. pa_u_hj32_h_root_35_u_product = pa_q_hj32_h_root_35_u_product_terminal * S ((S (e)) * pa_v_hj32_h_root_35_u_product) + (u))) /\ forall pa_i_hj32_h_root_35_u_product. (exists pa_lt_hj32_h_root_35_u_product_bound. pa_lt_hj32_h_root_35_u_product_bound + S pa_i_hj32_h_root_35_u_product = e) -> exists pa_p_hj32_h_root_35_u_product pa_r_hj32_h_root_35_u_product pa_s_hj32_h_root_35_u_product. ((((exists pa_h_hj32_h_root_35_u_product_factor. pa_h_hj32_h_root_35_u_product_factor + S (pa_p_hj32_h_root_35_u_product) = S ((S (pa_i_hj32_h_root_35_u_product)) * pa_c_hj32_h_root_35_u)) /\ exists pa_q_hj32_h_root_35_u_product_factor. pa_b_hj32_h_root_35_u = pa_q_hj32_h_root_35_u_product_factor * S ((S (pa_i_hj32_h_root_35_u_product)) * pa_c_hj32_h_root_35_u) + (pa_p_hj32_h_root_35_u_product))) /\ ((((exists pa_h_hj32_h_root_35_u_product_partial. pa_h_hj32_h_root_35_u_product_partial + S (pa_r_hj32_h_root_35_u_product) = S ((S (pa_i_hj32_h_root_35_u_product)) * pa_v_hj32_h_root_35_u_product)) /\ exists pa_q_hj32_h_root_35_u_product_partial. pa_u_hj32_h_root_35_u_product = pa_q_hj32_h_root_35_u_product_partial * S ((S (pa_i_hj32_h_root_35_u_product)) * pa_v_hj32_h_root_35_u_product) + (pa_r_hj32_h_root_35_u_product))) /\ ((((exists pa_h_hj32_h_root_35_u_product_successor. pa_h_hj32_h_root_35_u_product_successor + S (pa_s_hj32_h_root_35_u_product) = S ((S (S pa_i_hj32_h_root_35_u_product)) * pa_v_hj32_h_root_35_u_product)) /\ exists pa_q_hj32_h_root_35_u_product_successor. pa_u_hj32_h_root_35_u_product = pa_q_hj32_h_root_35_u_product_successor * S ((S (S pa_i_hj32_h_root_35_u_product)) * pa_v_hj32_h_root_35_u_product) + (pa_s_hj32_h_root_35_u_product))) /\ pa_s_hj32_h_root_35_u_product = pa_r_hj32_h_root_35_u_product * pa_p_hj32_h_root_35_u_product)))))))) -> (exists bqb_le_gap_hj32_h_root_35_result. bqb_le_gap_hj32_h_root_35_result + (h) = (u))

Proof neighborhood

Direct theorem prerequisites

BT00WB bertrand_scaled_budget_root_35 BT00WE ceil_div_six_budget_of_scaled_le BT00WO pow_thirty_six_double_block_eq_pow_six_four_block_from_total BT00WN pow_six_ten_block_le_pow_four_thirteen_block_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT009X pow_add BT00PY pow_base_monotone BT00SN pow_exponent_monotone_from_total BT00PV mul_le_mul BT000F le_trans BT0007 mul_add BT0008 mul_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

201 script commands · 47 reading checkpoints · 32 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 35ceil div six budget of scaled lepow thirty six double block eq pow six four block from totalpow six ten block le pow four thirteen block from totalpow six four le pow four six from totalpow addpow base monotonepow exponent monotone from totalmul le mulle transmul addmul 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(36,2 · 36,h)Definitions: Pow(36,2 · 36,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 : 35 + 1 = 36
  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 * 35 + 2 = 2 * 36
  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 h35s_p36L20–23

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

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

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

  1. L24
    cases h35s_p36
07Establish h35s_baseL25–25

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

  1. L25
    have h35s_base : Lt(35,36)Definitions: Lt(35,36)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 0
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 h35s_to_36L28–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 h35s_to_36 : Le(h,x)Definitions: Le(h,x)Original native command in the exact edition
  2. L29
    specialize pow_base_monotone 36
  3. L30
    specialize pow_base_monotone 36
  4. L31
    specialize pow_base_monotone 2 * 36
  5. L32
    specialize pow_base_monotone h
  6. L33
    specialize pow_base_monotone x
  7. L34
    apply pow_base_monotone
  8. L35
    exact h35s_base
  9. L36
    exact hh_route
  10. L37
    exact h35s_p36_witness
11Establish h35s_p6_totalL38–41

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

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

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

  1. L42
    cases h35s_p6_total
13Establish h35s_conversionL43–51

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

  1. L43
    have h35s_conversion : x = x1
  2. L44
    specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total 36
  3. L45
    specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x
  4. L46
    specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x1
  5. L47
    apply pow_thirty_six_double_block_eq_pow_six_four_block_from_total
  6. L48
    exact htotal
  7. L49
    exact h35s_p36_witness
  8. L50
    exact h35s_p6_total_witness
  9. L51
    rewrite h35s_conversion at h35s_to_36
14Establish h35s_p6_mainL52–55

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

  1. L52
    have h35s_p6_main : ∃ hj32_local_value_h35s_p6_main. Pow(6,10 · 14,hj32_local_value_h35s_p6_main)Definitions: Pow(6,10 · 14,hj32_local_value_h35s_p6_main)Original native command in the exact edition
  2. L53
    specialize htotal 6
  3. L54
    specialize htotal 10 * 14
  4. L55
    exact htotal
15Separate the logical casesL56–56

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

  1. L56
    cases h35s_p6_main
16Establish h35s_p4_mainL57–60

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

  1. L57
    have h35s_p4_main : ∃ hj32_local_value_h35s_p4_main. Pow(4,13 · 14,hj32_local_value_h35s_p4_main)Definitions: Pow(4,13 · 14,hj32_local_value_h35s_p4_main)Original native command in the exact edition
  2. L58
    specialize htotal 4
  3. L59
    specialize htotal 13 * 14
  4. L60
    exact htotal
17Separate the logical casesL61–61

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

  1. L61
    cases h35s_p4_main
18Establish h35s_main_boundL62–69

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

  1. L62
    have h35s_main_bound : Le(x2,x3)Definitions: Le(x2,x3)Original native command in the exact edition
  2. L63
    specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 14
  3. L64
    specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x2
  4. L65
    specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x3
  5. L66
    apply pow_six_ten_block_le_pow_four_thirteen_block_from_total
  6. L67
    exact htotal
  7. L68
    exact h35s_p6_main_witness
  8. L69
    exact h35s_p4_main_witness
19Establish h35s_p6_residualL70–73

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

  1. L70
    have h35s_p6_residual : ∃ hj32_local_value_h35s_p6_residual. Pow(6,4,hj32_local_value_h35s_p6_residual)Definitions: Pow(6,4,hj32_local_value_h35s_p6_residual)Original native command in the exact edition
  2. L71
    specialize htotal 6
  3. L72
    specialize htotal 4
  4. L73
    exact htotal
20Separate the logical casesL74–74

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

  1. L74
    cases h35s_p6_residual
21Establish h35s_p4_residualL75–78

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

  1. L75
    have h35s_p4_residual : ∃ hj32_local_value_h35s_p4_residual. Pow(4,6,hj32_local_value_h35s_p4_residual)Definitions: Pow(4,6,hj32_local_value_h35s_p4_residual)Original native command in the exact edition
  2. L76
    specialize htotal 4
  3. L77
    specialize htotal 6
  4. L78
    exact htotal
22Separate the logical casesL79–79

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

  1. L79
    cases h35s_p4_residual
23Establish h35s_residual_boundL80–86

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

  1. L80
    have h35s_residual_bound : Le(x4,x5)Definitions: Le(x4,x5)Original native command in the exact edition
  2. L81
    specialize pow_six_four_le_pow_four_six_from_total x4
  3. L82
    specialize pow_six_four_le_pow_four_six_from_total x5
  4. L83
    apply pow_six_four_le_pow_four_six_from_total
  5. L84
    exact htotal
  6. L85
    exact h35s_p6_residual_witness
  7. L86
    exact h35s_p4_residual_witness
24Establish h35s_exponentL87–87

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

  1. L87
    have h35s_exponent : 4 * 36 = 10 * 14 + 4
25Establish h35s_thirty_sixL88–90

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

  1. L88
    have h35s_thirty_six : 36 = 5 * 7 + 1
  2. L89
    norm_num
  3. L90
    rewrite h35s_thirty_six
26Establish h35s_distribL91–96

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

  1. L91
    have h35s_distrib : 4 * (5 * 7 + 1) = 4 * (5 * 7) + 4 * 1
  2. L92
    specialize mul_add 4
  3. L93
    specialize mul_add (5 * 7)
  4. L94
    specialize mul_add 1
  5. L95
    apply mul_add
  6. L96
    rewrite h35s_distrib
27Establish h35s_left_assocL97–103

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

  1. L97
    have h35s_left_assoc : 4 * (5 * 7) = (4 * 5) * 7
  2. L98
    symm
  3. L99
    specialize mul_assoc 4
  4. L100
    specialize mul_assoc 5
  5. L101
    specialize mul_assoc 7
  6. L102
    apply mul_assoc
  7. L103
    rewrite h35s_left_assoc
28Establish h35s_fourteenL104–106

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

  1. L104
    have h35s_fourteen : 14 = 2 * 7
  2. L105
    norm_num
  3. L106
    rewrite h35s_fourteen
29Establish h35s_right_assocL107–113

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

  1. L107
    have h35s_right_assoc : 10 * (2 * 7) = (10 * 2) * 7
  2. L108
    symm
  3. L109
    specialize mul_assoc 10
  4. L110
    specialize mul_assoc 2
  5. L111
    specialize mul_assoc 7
  6. L112
    apply mul_assoc
  7. L113
    rewrite h35s_right_assoc
30Establish h35s_right_twentyL114–116

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

  1. L114
    have h35s_right_twenty : 10 * 2 = 20
  2. L115
    norm_num
  3. L116
    rewrite h35s_right_twenty
31Establish h35s_twentyL117–119

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

  1. L117
    have h35s_twenty : 4 * 5 = 20
  2. L118
    norm_num
  3. L119
    rewrite h35s_twenty
32Establish h35s_fourL120–123

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

  1. L120
    have h35s_four : 4 * 1 = 4
  2. L121
    norm_num
  3. L122
    rewrite h35s_four
  4. L123
    refl
33Establish h35s_left_productL124–133

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

  1. L124
    have h35s_left_product : x1 = x2 * x4
  2. L125
    specialize pow_add 6
  3. L126
    specialize pow_add 10 * 14
  4. L127
    specialize pow_add 4
  5. L128
    specialize pow_add 4 * 36
  6. L129
    specialize pow_add x2
  7. L130
    specialize pow_add x4
  8. L131
    specialize pow_add x1
  9. L132
    apply pow_add
  10. L133
    exact h35s_exponent
34Use earlier factsL134–136

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

  1. L134
    exact h35s_p6_main_witness
  2. L135
    exact h35s_p6_residual_witness
  3. L136
    exact h35s_p6_total_witness
35Establish h35s_p4_budgetL137–140

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

  1. L137
    have h35s_p4_budget : ∃ hj32_local_value_h35s_p4_budget. Pow(4,13 · 14 + 6,hj32_local_value_h35s_p4_budget)Definitions: Pow(4,13 · 14 + 6,hj32_local_value_h35s_p4_budget)Original native command in the exact edition
  2. L138
    specialize htotal 4
  3. L139
    specialize htotal 13 * 14 + 6
  4. L140
    exact htotal
36Separate the logical casesL141–141

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

  1. L141
    cases h35s_p4_budget
37Establish h35s_right_productL142–151

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

  1. L142
    have h35s_right_product : x6 = x3 * x5
  2. L143
    specialize pow_add 4
  3. L144
    specialize pow_add 13 * 14
  4. L145
    specialize pow_add 6
  5. L146
    specialize pow_add 13 * 14 + 6
  6. L147
    specialize pow_add x3
  7. L148
    specialize pow_add x5
  8. L149
    specialize pow_add x6
  9. L150
    apply pow_add
  10. L151
    refl
38Use earlier factsL152–154

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

  1. L152
    exact h35s_p4_main_witness
  2. L153
    exact h35s_p4_residual_witness
  3. L154
    exact h35s_p4_budget_witness
39Establish h35s_six_boundL155–164

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

  1. L155
    have h35s_six_bound : Le(x2 · x4,x3 · x5)Definitions: Le(x2 · x4,x3 · x5)Original native command in the exact edition
  2. L156
    specialize mul_le_mul x2
  3. L157
    specialize mul_le_mul x3
  4. L158
    specialize mul_le_mul x4
  5. L159
    specialize mul_le_mul x5
  6. L160
    apply mul_le_mul
  7. L161
    exact h35s_main_bound
  8. L162
    exact h35s_residual_bound
  9. L163
    rewrite <- h35s_left_product at h35s_six_bound
  10. L164
    rewrite <- h35s_right_product at h35s_six_bound
40Establish h35s_to_budgetL165–171

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

  1. L165
    have h35s_to_budget : Le(h,x6)Definitions: Le(h,x6)Original native command in the exact edition
  2. L166
    specialize le_trans h
  3. L167
    specialize le_trans x1
  4. L168
    specialize le_trans x6
  5. L169
    apply le_trans
  6. L170
    exact h35s_to_36
  7. L171
    exact h35s_six_bound
41Establish hscaledL172–173

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

  1. L172
    have hscaled : Le(6 · (13 · 14 + 6),35 · 35)Definitions: Le(6 · (13 · 14 + 6),35 · 35)Original native command in the exact edition
  2. L173
    apply bertrand_scaled_budget_root_35
42Establish hbudget_exponentL174–180

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. L174
    have hbudget_exponent : Le(13 · 14 + 6,e)Definitions: Le(13 · 14 + 6,e)Original native command in the exact edition
  2. L175
    specialize ceil_div_six_budget_of_scaled_le (35 * 35)
  3. L176
    specialize ceil_div_six_budget_of_scaled_le (13 * 14 + 6)
  4. L177
    specialize ceil_div_six_budget_of_scaled_le e
  5. L178
    apply ceil_div_six_budget_of_scaled_le
  6. L179
    exact hceiling
  7. L180
    exact hscaled
43Establish h35_budget_growthL181–188

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

  1. L181
    have h35_budget_growth : Le(x6,u)Definitions: Le(x6,u)Original native command in the exact edition
  2. L182
    specialize pow_exponent_monotone_from_total 4
  3. L183
    specialize pow_exponent_monotone_from_total 13 * 14 + 6
  4. L184
    specialize pow_exponent_monotone_from_total e
  5. L185
    specialize pow_exponent_monotone_from_total x6
  6. L186
    specialize pow_exponent_monotone_from_total u
  7. L187
    apply pow_exponent_monotone_from_total
  8. L188
    exact htotal
44Construct an explicit witnessL189–189

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

  1. L189
    exists 3
45Calculate and transport equalitiesL190–190

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

  1. L190
    norm_num
46Use earlier factsL191–193

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

  1. L191
    exact hbudget_exponent
  2. L192
    exact h35s_p4_budget_witness
  3. L193
    exact hu
47Establish h35_resultL194–201

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

  1. L194
    have h35_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L195
    specialize le_trans h
  3. L196
    specialize le_trans x6
  4. L197
    specialize le_trans u
  5. L198
    apply le_trans
  6. L199
    exact h35s_to_budget
  7. L200
    exact h35_budget_growth
  8. L201
    exact h35_result

Library-wide reading audit

Original defined command ledger · 201 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(36,2 · 36,h)
    Exact native replay linehave hh_route : exists pa_b_hj32_h_35_route pa_c_hj32_h_35_route. ((forall pa_i_hj32_h_35_route_repeat. (exists pa_lt_hj32_h_35_route_repeat_bound. pa_lt_hj32_h_35_route_repeat_bound + S pa_i_hj32_h_35_route_repeat = 2 * 36) -> (((exists pa_h_hj32_h_35_route_repeat_decoded. pa_h_hj32_h_35_route_repeat_decoded + S (36) = S ((S (pa_i_hj32_h_35_route_repeat)) * pa_c_hj32_h_35_route)) /\ exists pa_q_hj32_h_35_route_repeat_decoded. pa_b_hj32_h_35_route = pa_q_hj32_h_35_route_repeat_decoded * S ((S (pa_i_hj32_h_35_route_repeat)) * pa_c_hj32_h_35_route) + (36)))) /\ (exists pa_u_hj32_h_35_route_product pa_v_hj32_h_35_route_product. ((((exists pa_h_hj32_h_35_route_product_start. pa_h_hj32_h_35_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_35_route_product)) /\ exists pa_q_hj32_h_35_route_product_start. pa_u_hj32_h_35_route_product = pa_q_hj32_h_35_route_product_start * S ((S (0)) * pa_v_hj32_h_35_route_product) + (1))) /\ ((((exists pa_h_hj32_h_35_route_product_terminal. pa_h_hj32_h_35_route_product_terminal + S (h) = S ((S (2 * 36)) * pa_v_hj32_h_35_route_product)) /\ exists pa_q_hj32_h_35_route_product_terminal. pa_u_hj32_h_35_route_product = pa_q_hj32_h_35_route_product_terminal * S ((S (2 * 36)) * pa_v_hj32_h_35_route_product) + (h))) /\ forall pa_i_hj32_h_35_route_product. (exists pa_lt_hj32_h_35_route_product_bound. pa_lt_hj32_h_35_route_product_bound + S pa_i_hj32_h_35_route_product = 2 * 36) -> exists pa_p_hj32_h_35_route_product pa_r_hj32_h_35_route_product pa_s_hj32_h_35_route_product. ((((exists pa_h_hj32_h_35_route_product_factor. pa_h_hj32_h_35_route_product_factor + S (pa_p_hj32_h_35_route_product) = S ((S (pa_i_hj32_h_35_route_product)) * pa_c_hj32_h_35_route)) /\ exists pa_q_hj32_h_35_route_product_factor. pa_b_hj32_h_35_route = pa_q_hj32_h_35_route_product_factor * S ((S (pa_i_hj32_h_35_route_product)) * pa_c_hj32_h_35_route) + (pa_p_hj32_h_35_route_product))) /\ ((((exists pa_h_hj32_h_35_route_product_partial. pa_h_hj32_h_35_route_product_partial + S (pa_r_hj32_h_35_route_product) = S ((S (pa_i_hj32_h_35_route_product)) * pa_v_hj32_h_35_route_product)) /\ exists pa_q_hj32_h_35_route_product_partial. pa_u_hj32_h_35_route_product = pa_q_hj32_h_35_route_product_partial * S ((S (pa_i_hj32_h_35_route_product)) * pa_v_hj32_h_35_route_product) + (pa_r_hj32_h_35_route_product))) /\ ((((exists pa_h_hj32_h_35_route_product_successor. pa_h_hj32_h_35_route_product_successor + S (pa_s_hj32_h_35_route_product) = S ((S (S pa_i_hj32_h_35_route_product)) * pa_v_hj32_h_35_route_product)) /\ exists pa_q_hj32_h_35_route_product_successor. pa_u_hj32_h_35_route_product = pa_q_hj32_h_35_route_product_successor * S ((S (S pa_i_hj32_h_35_route_product)) * pa_v_hj32_h_35_route_product) + (pa_s_hj32_h_35_route_product))) /\ pa_s_hj32_h_35_route_product = pa_r_hj32_h_35_route_product * pa_p_hj32_h_35_route_product)))))))
  9. 0009have hh_base : 35 + 1 = 36
  10. 0010norm_num
  11. 0011have hh_exponent : 2 * 35 + 2 = 2 * 36
  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 h35s_p36 : ∃ hj32_local_value_h35s_p36. Pow(36,2 · 36,hj32_local_value_h35s_p36)
    Exact native replay linehave h35s_p36 : exists hj32_local_value_h35s_p36. (exists pa_b_hj32_local_total_h35s_p36 pa_c_hj32_local_total_h35s_p36. ((forall pa_i_hj32_local_total_h35s_p36_repeat. (exists pa_lt_hj32_local_total_h35s_p36_repeat_bound. pa_lt_hj32_local_total_h35s_p36_repeat_bound + S pa_i_hj32_local_total_h35s_p36_repeat = 2 * 36) -> (((exists pa_h_hj32_local_total_h35s_p36_repeat_decoded. pa_h_hj32_local_total_h35s_p36_repeat_decoded + S (36) = S ((S (pa_i_hj32_local_total_h35s_p36_repeat)) * pa_c_hj32_local_total_h35s_p36)) /\ exists pa_q_hj32_local_total_h35s_p36_repeat_decoded. pa_b_hj32_local_total_h35s_p36 = pa_q_hj32_local_total_h35s_p36_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p36_repeat)) * pa_c_hj32_local_total_h35s_p36) + (36)))) /\ (exists pa_u_hj32_local_total_h35s_p36_product pa_v_hj32_local_total_h35s_p36_product. ((((exists pa_h_hj32_local_total_h35s_p36_product_start. pa_h_hj32_local_total_h35s_p36_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p36_product)) /\ exists pa_q_hj32_local_total_h35s_p36_product_start. pa_u_hj32_local_total_h35s_p36_product = pa_q_hj32_local_total_h35s_p36_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p36_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p36_product_terminal. pa_h_hj32_local_total_h35s_p36_product_terminal + S (hj32_local_value_h35s_p36) = S ((S (2 * 36)) * pa_v_hj32_local_total_h35s_p36_product)) /\ exists pa_q_hj32_local_total_h35s_p36_product_terminal. pa_u_hj32_local_total_h35s_p36_product = pa_q_hj32_local_total_h35s_p36_product_terminal * S ((S (2 * 36)) * pa_v_hj32_local_total_h35s_p36_product) + (hj32_local_value_h35s_p36))) /\ forall pa_i_hj32_local_total_h35s_p36_product. (exists pa_lt_hj32_local_total_h35s_p36_product_bound. pa_lt_hj32_local_total_h35s_p36_product_bound + S pa_i_hj32_local_total_h35s_p36_product = 2 * 36) -> exists pa_p_hj32_local_total_h35s_p36_product pa_r_hj32_local_total_h35s_p36_product pa_s_hj32_local_total_h35s_p36_product. ((((exists pa_h_hj32_local_total_h35s_p36_product_factor. pa_h_hj32_local_total_h35s_p36_product_factor + S (pa_p_hj32_local_total_h35s_p36_product) = S ((S (pa_i_hj32_local_total_h35s_p36_product)) * pa_c_hj32_local_total_h35s_p36)) /\ exists pa_q_hj32_local_total_h35s_p36_product_factor. pa_b_hj32_local_total_h35s_p36 = pa_q_hj32_local_total_h35s_p36_product_factor * S ((S (pa_i_hj32_local_total_h35s_p36_product)) * pa_c_hj32_local_total_h35s_p36) + (pa_p_hj32_local_total_h35s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p36_product_partial. pa_h_hj32_local_total_h35s_p36_product_partial + S (pa_r_hj32_local_total_h35s_p36_product) = S ((S (pa_i_hj32_local_total_h35s_p36_product)) * pa_v_hj32_local_total_h35s_p36_product)) /\ exists pa_q_hj32_local_total_h35s_p36_product_partial. pa_u_hj32_local_total_h35s_p36_product = pa_q_hj32_local_total_h35s_p36_product_partial * S ((S (pa_i_hj32_local_total_h35s_p36_product)) * pa_v_hj32_local_total_h35s_p36_product) + (pa_r_hj32_local_total_h35s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p36_product_successor. pa_h_hj32_local_total_h35s_p36_product_successor + S (pa_s_hj32_local_total_h35s_p36_product) = S ((S (S pa_i_hj32_local_total_h35s_p36_product)) * pa_v_hj32_local_total_h35s_p36_product)) /\ exists pa_q_hj32_local_total_h35s_p36_product_successor. pa_u_hj32_local_total_h35s_p36_product = pa_q_hj32_local_total_h35s_p36_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p36_product)) * pa_v_hj32_local_total_h35s_p36_product) + (pa_s_hj32_local_total_h35s_p36_product))) /\ pa_s_hj32_local_total_h35s_p36_product = pa_r_hj32_local_total_h35s_p36_product * pa_p_hj32_local_total_h35s_p36_product))))))))
  21. 0021specialize htotal 36
  22. 0022specialize htotal 2 * 36
  23. 0023exact htotal
  24. 0024cases h35s_p36
  25. 0025have h35s_base : Lt(35,36)
    Exact native replay linehave h35s_base : exists bqb_le_gap_hj32_h35s_base. bqb_le_gap_hj32_h35s_base + (36) = (36)
  26. 0026exists 0
  27. 0027norm_num
  28. 0028have h35s_to_36 : Le(h,x)
    Exact native replay linehave h35s_to_36 : exists bqb_le_gap_hj32_local_base_bound_h35s_to_36. bqb_le_gap_hj32_local_base_bound_h35s_to_36 + (h) = (x)
  29. 0029specialize pow_base_monotone 36
  30. 0030specialize pow_base_monotone 36
  31. 0031specialize pow_base_monotone 2 * 36
  32. 0032specialize pow_base_monotone h
  33. 0033specialize pow_base_monotone x
  34. 0034apply pow_base_monotone
  35. 0035exact h35s_base
  36. 0036exact hh_route
  37. 0037exact h35s_p36_witness
  38. 0038have h35s_p6_total : ∃ hj32_local_value_h35s_p6_total. Pow(6,4 · 36,hj32_local_value_h35s_p6_total)
    Exact native replay linehave h35s_p6_total : exists hj32_local_value_h35s_p6_total. (exists pa_b_hj32_local_total_h35s_p6_total pa_c_hj32_local_total_h35s_p6_total. ((forall pa_i_hj32_local_total_h35s_p6_total_repeat. (exists pa_lt_hj32_local_total_h35s_p6_total_repeat_bound. pa_lt_hj32_local_total_h35s_p6_total_repeat_bound + S pa_i_hj32_local_total_h35s_p6_total_repeat = 4 * 36) -> (((exists pa_h_hj32_local_total_h35s_p6_total_repeat_decoded. pa_h_hj32_local_total_h35s_p6_total_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h35s_p6_total_repeat)) * pa_c_hj32_local_total_h35s_p6_total)) /\ exists pa_q_hj32_local_total_h35s_p6_total_repeat_decoded. pa_b_hj32_local_total_h35s_p6_total = pa_q_hj32_local_total_h35s_p6_total_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p6_total_repeat)) * pa_c_hj32_local_total_h35s_p6_total) + (6)))) /\ (exists pa_u_hj32_local_total_h35s_p6_total_product pa_v_hj32_local_total_h35s_p6_total_product. ((((exists pa_h_hj32_local_total_h35s_p6_total_product_start. pa_h_hj32_local_total_h35s_p6_total_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p6_total_product)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_start. pa_u_hj32_local_total_h35s_p6_total_product = pa_q_hj32_local_total_h35s_p6_total_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p6_total_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_total_product_terminal. pa_h_hj32_local_total_h35s_p6_total_product_terminal + S (hj32_local_value_h35s_p6_total) = S ((S (4 * 36)) * pa_v_hj32_local_total_h35s_p6_total_product)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_terminal. pa_u_hj32_local_total_h35s_p6_total_product = pa_q_hj32_local_total_h35s_p6_total_product_terminal * S ((S (4 * 36)) * pa_v_hj32_local_total_h35s_p6_total_product) + (hj32_local_value_h35s_p6_total))) /\ forall pa_i_hj32_local_total_h35s_p6_total_product. (exists pa_lt_hj32_local_total_h35s_p6_total_product_bound. pa_lt_hj32_local_total_h35s_p6_total_product_bound + S pa_i_hj32_local_total_h35s_p6_total_product = 4 * 36) -> exists pa_p_hj32_local_total_h35s_p6_total_product pa_r_hj32_local_total_h35s_p6_total_product pa_s_hj32_local_total_h35s_p6_total_product. ((((exists pa_h_hj32_local_total_h35s_p6_total_product_factor. pa_h_hj32_local_total_h35s_p6_total_product_factor + S (pa_p_hj32_local_total_h35s_p6_total_product) = S ((S (pa_i_hj32_local_total_h35s_p6_total_product)) * pa_c_hj32_local_total_h35s_p6_total)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_factor. pa_b_hj32_local_total_h35s_p6_total = pa_q_hj32_local_total_h35s_p6_total_product_factor * S ((S (pa_i_hj32_local_total_h35s_p6_total_product)) * pa_c_hj32_local_total_h35s_p6_total) + (pa_p_hj32_local_total_h35s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_total_product_partial. pa_h_hj32_local_total_h35s_p6_total_product_partial + S (pa_r_hj32_local_total_h35s_p6_total_product) = S ((S (pa_i_hj32_local_total_h35s_p6_total_product)) * pa_v_hj32_local_total_h35s_p6_total_product)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_partial. pa_u_hj32_local_total_h35s_p6_total_product = pa_q_hj32_local_total_h35s_p6_total_product_partial * S ((S (pa_i_hj32_local_total_h35s_p6_total_product)) * pa_v_hj32_local_total_h35s_p6_total_product) + (pa_r_hj32_local_total_h35s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_total_product_successor. pa_h_hj32_local_total_h35s_p6_total_product_successor + S (pa_s_hj32_local_total_h35s_p6_total_product) = S ((S (S pa_i_hj32_local_total_h35s_p6_total_product)) * pa_v_hj32_local_total_h35s_p6_total_product)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_successor. pa_u_hj32_local_total_h35s_p6_total_product = pa_q_hj32_local_total_h35s_p6_total_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p6_total_product)) * pa_v_hj32_local_total_h35s_p6_total_product) + (pa_s_hj32_local_total_h35s_p6_total_product))) /\ pa_s_hj32_local_total_h35s_p6_total_product = pa_r_hj32_local_total_h35s_p6_total_product * pa_p_hj32_local_total_h35s_p6_total_product))))))))
  39. 0039specialize htotal 6
  40. 0040specialize htotal 4 * 36
  41. 0041exact htotal
  42. 0042cases h35s_p6_total
  43. 0043have h35s_conversion : x = x1
  44. 0044specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total 36
  45. 0045specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x
  46. 0046specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x1
  47. 0047apply pow_thirty_six_double_block_eq_pow_six_four_block_from_total
  48. 0048exact htotal
  49. 0049exact h35s_p36_witness
  50. 0050exact h35s_p6_total_witness
  51. 0051rewrite h35s_conversion at h35s_to_36
  52. 0052have h35s_p6_main : ∃ hj32_local_value_h35s_p6_main. Pow(6,10 · 14,hj32_local_value_h35s_p6_main)
    Exact native replay linehave h35s_p6_main : exists hj32_local_value_h35s_p6_main. (exists pa_b_hj32_local_total_h35s_p6_main pa_c_hj32_local_total_h35s_p6_main. ((forall pa_i_hj32_local_total_h35s_p6_main_repeat. (exists pa_lt_hj32_local_total_h35s_p6_main_repeat_bound. pa_lt_hj32_local_total_h35s_p6_main_repeat_bound + S pa_i_hj32_local_total_h35s_p6_main_repeat = 10 * 14) -> (((exists pa_h_hj32_local_total_h35s_p6_main_repeat_decoded. pa_h_hj32_local_total_h35s_p6_main_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h35s_p6_main_repeat)) * pa_c_hj32_local_total_h35s_p6_main)) /\ exists pa_q_hj32_local_total_h35s_p6_main_repeat_decoded. pa_b_hj32_local_total_h35s_p6_main = pa_q_hj32_local_total_h35s_p6_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p6_main_repeat)) * pa_c_hj32_local_total_h35s_p6_main) + (6)))) /\ (exists pa_u_hj32_local_total_h35s_p6_main_product pa_v_hj32_local_total_h35s_p6_main_product. ((((exists pa_h_hj32_local_total_h35s_p6_main_product_start. pa_h_hj32_local_total_h35s_p6_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p6_main_product)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_start. pa_u_hj32_local_total_h35s_p6_main_product = pa_q_hj32_local_total_h35s_p6_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p6_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_main_product_terminal. pa_h_hj32_local_total_h35s_p6_main_product_terminal + S (hj32_local_value_h35s_p6_main) = S ((S (10 * 14)) * pa_v_hj32_local_total_h35s_p6_main_product)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_terminal. pa_u_hj32_local_total_h35s_p6_main_product = pa_q_hj32_local_total_h35s_p6_main_product_terminal * S ((S (10 * 14)) * pa_v_hj32_local_total_h35s_p6_main_product) + (hj32_local_value_h35s_p6_main))) /\ forall pa_i_hj32_local_total_h35s_p6_main_product. (exists pa_lt_hj32_local_total_h35s_p6_main_product_bound. pa_lt_hj32_local_total_h35s_p6_main_product_bound + S pa_i_hj32_local_total_h35s_p6_main_product = 10 * 14) -> exists pa_p_hj32_local_total_h35s_p6_main_product pa_r_hj32_local_total_h35s_p6_main_product pa_s_hj32_local_total_h35s_p6_main_product. ((((exists pa_h_hj32_local_total_h35s_p6_main_product_factor. pa_h_hj32_local_total_h35s_p6_main_product_factor + S (pa_p_hj32_local_total_h35s_p6_main_product) = S ((S (pa_i_hj32_local_total_h35s_p6_main_product)) * pa_c_hj32_local_total_h35s_p6_main)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_factor. pa_b_hj32_local_total_h35s_p6_main = pa_q_hj32_local_total_h35s_p6_main_product_factor * S ((S (pa_i_hj32_local_total_h35s_p6_main_product)) * pa_c_hj32_local_total_h35s_p6_main) + (pa_p_hj32_local_total_h35s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_main_product_partial. pa_h_hj32_local_total_h35s_p6_main_product_partial + S (pa_r_hj32_local_total_h35s_p6_main_product) = S ((S (pa_i_hj32_local_total_h35s_p6_main_product)) * pa_v_hj32_local_total_h35s_p6_main_product)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_partial. pa_u_hj32_local_total_h35s_p6_main_product = pa_q_hj32_local_total_h35s_p6_main_product_partial * S ((S (pa_i_hj32_local_total_h35s_p6_main_product)) * pa_v_hj32_local_total_h35s_p6_main_product) + (pa_r_hj32_local_total_h35s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_main_product_successor. pa_h_hj32_local_total_h35s_p6_main_product_successor + S (pa_s_hj32_local_total_h35s_p6_main_product) = S ((S (S pa_i_hj32_local_total_h35s_p6_main_product)) * pa_v_hj32_local_total_h35s_p6_main_product)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_successor. pa_u_hj32_local_total_h35s_p6_main_product = pa_q_hj32_local_total_h35s_p6_main_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p6_main_product)) * pa_v_hj32_local_total_h35s_p6_main_product) + (pa_s_hj32_local_total_h35s_p6_main_product))) /\ pa_s_hj32_local_total_h35s_p6_main_product = pa_r_hj32_local_total_h35s_p6_main_product * pa_p_hj32_local_total_h35s_p6_main_product))))))))
  53. 0053specialize htotal 6
  54. 0054specialize htotal 10 * 14
  55. 0055exact htotal
  56. 0056cases h35s_p6_main
  57. 0057have h35s_p4_main : ∃ hj32_local_value_h35s_p4_main. Pow(4,13 · 14,hj32_local_value_h35s_p4_main)
    Exact native replay linehave h35s_p4_main : exists hj32_local_value_h35s_p4_main. (exists pa_b_hj32_local_total_h35s_p4_main pa_c_hj32_local_total_h35s_p4_main. ((forall pa_i_hj32_local_total_h35s_p4_main_repeat. (exists pa_lt_hj32_local_total_h35s_p4_main_repeat_bound. pa_lt_hj32_local_total_h35s_p4_main_repeat_bound + S pa_i_hj32_local_total_h35s_p4_main_repeat = 13 * 14) -> (((exists pa_h_hj32_local_total_h35s_p4_main_repeat_decoded. pa_h_hj32_local_total_h35s_p4_main_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h35s_p4_main_repeat)) * pa_c_hj32_local_total_h35s_p4_main)) /\ exists pa_q_hj32_local_total_h35s_p4_main_repeat_decoded. pa_b_hj32_local_total_h35s_p4_main = pa_q_hj32_local_total_h35s_p4_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p4_main_repeat)) * pa_c_hj32_local_total_h35s_p4_main) + (4)))) /\ (exists pa_u_hj32_local_total_h35s_p4_main_product pa_v_hj32_local_total_h35s_p4_main_product. ((((exists pa_h_hj32_local_total_h35s_p4_main_product_start. pa_h_hj32_local_total_h35s_p4_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p4_main_product)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_start. pa_u_hj32_local_total_h35s_p4_main_product = pa_q_hj32_local_total_h35s_p4_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p4_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_main_product_terminal. pa_h_hj32_local_total_h35s_p4_main_product_terminal + S (hj32_local_value_h35s_p4_main) = S ((S (13 * 14)) * pa_v_hj32_local_total_h35s_p4_main_product)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_terminal. pa_u_hj32_local_total_h35s_p4_main_product = pa_q_hj32_local_total_h35s_p4_main_product_terminal * S ((S (13 * 14)) * pa_v_hj32_local_total_h35s_p4_main_product) + (hj32_local_value_h35s_p4_main))) /\ forall pa_i_hj32_local_total_h35s_p4_main_product. (exists pa_lt_hj32_local_total_h35s_p4_main_product_bound. pa_lt_hj32_local_total_h35s_p4_main_product_bound + S pa_i_hj32_local_total_h35s_p4_main_product = 13 * 14) -> exists pa_p_hj32_local_total_h35s_p4_main_product pa_r_hj32_local_total_h35s_p4_main_product pa_s_hj32_local_total_h35s_p4_main_product. ((((exists pa_h_hj32_local_total_h35s_p4_main_product_factor. pa_h_hj32_local_total_h35s_p4_main_product_factor + S (pa_p_hj32_local_total_h35s_p4_main_product) = S ((S (pa_i_hj32_local_total_h35s_p4_main_product)) * pa_c_hj32_local_total_h35s_p4_main)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_factor. pa_b_hj32_local_total_h35s_p4_main = pa_q_hj32_local_total_h35s_p4_main_product_factor * S ((S (pa_i_hj32_local_total_h35s_p4_main_product)) * pa_c_hj32_local_total_h35s_p4_main) + (pa_p_hj32_local_total_h35s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_main_product_partial. pa_h_hj32_local_total_h35s_p4_main_product_partial + S (pa_r_hj32_local_total_h35s_p4_main_product) = S ((S (pa_i_hj32_local_total_h35s_p4_main_product)) * pa_v_hj32_local_total_h35s_p4_main_product)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_partial. pa_u_hj32_local_total_h35s_p4_main_product = pa_q_hj32_local_total_h35s_p4_main_product_partial * S ((S (pa_i_hj32_local_total_h35s_p4_main_product)) * pa_v_hj32_local_total_h35s_p4_main_product) + (pa_r_hj32_local_total_h35s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_main_product_successor. pa_h_hj32_local_total_h35s_p4_main_product_successor + S (pa_s_hj32_local_total_h35s_p4_main_product) = S ((S (S pa_i_hj32_local_total_h35s_p4_main_product)) * pa_v_hj32_local_total_h35s_p4_main_product)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_successor. pa_u_hj32_local_total_h35s_p4_main_product = pa_q_hj32_local_total_h35s_p4_main_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p4_main_product)) * pa_v_hj32_local_total_h35s_p4_main_product) + (pa_s_hj32_local_total_h35s_p4_main_product))) /\ pa_s_hj32_local_total_h35s_p4_main_product = pa_r_hj32_local_total_h35s_p4_main_product * pa_p_hj32_local_total_h35s_p4_main_product))))))))
  58. 0058specialize htotal 4
  59. 0059specialize htotal 13 * 14
  60. 0060exact htotal
  61. 0061cases h35s_p4_main
  62. 0062have h35s_main_bound : Le(x2,x3)
    Exact native replay linehave h35s_main_bound : exists bqb_le_gap_hj32_h35s_main_bound. bqb_le_gap_hj32_h35s_main_bound + (x2) = (x3)
  63. 0063specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 14
  64. 0064specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x2
  65. 0065specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x3
  66. 0066apply pow_six_ten_block_le_pow_four_thirteen_block_from_total
  67. 0067exact htotal
  68. 0068exact h35s_p6_main_witness
  69. 0069exact h35s_p4_main_witness
  70. 0070have h35s_p6_residual : ∃ hj32_local_value_h35s_p6_residual. Pow(6,4,hj32_local_value_h35s_p6_residual)
    Exact native replay linehave h35s_p6_residual : exists hj32_local_value_h35s_p6_residual. (exists pa_b_hj32_local_total_h35s_p6_residual pa_c_hj32_local_total_h35s_p6_residual. ((forall pa_i_hj32_local_total_h35s_p6_residual_repeat. (exists pa_lt_hj32_local_total_h35s_p6_residual_repeat_bound. pa_lt_hj32_local_total_h35s_p6_residual_repeat_bound + S pa_i_hj32_local_total_h35s_p6_residual_repeat = 4) -> (((exists pa_h_hj32_local_total_h35s_p6_residual_repeat_decoded. pa_h_hj32_local_total_h35s_p6_residual_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h35s_p6_residual_repeat)) * pa_c_hj32_local_total_h35s_p6_residual)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_repeat_decoded. pa_b_hj32_local_total_h35s_p6_residual = pa_q_hj32_local_total_h35s_p6_residual_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p6_residual_repeat)) * pa_c_hj32_local_total_h35s_p6_residual) + (6)))) /\ (exists pa_u_hj32_local_total_h35s_p6_residual_product pa_v_hj32_local_total_h35s_p6_residual_product. ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_start. pa_h_hj32_local_total_h35s_p6_residual_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_start. pa_u_hj32_local_total_h35s_p6_residual_product = pa_q_hj32_local_total_h35s_p6_residual_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p6_residual_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_terminal. pa_h_hj32_local_total_h35s_p6_residual_product_terminal + S (hj32_local_value_h35s_p6_residual) = S ((S (4)) * pa_v_hj32_local_total_h35s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_terminal. pa_u_hj32_local_total_h35s_p6_residual_product = pa_q_hj32_local_total_h35s_p6_residual_product_terminal * S ((S (4)) * pa_v_hj32_local_total_h35s_p6_residual_product) + (hj32_local_value_h35s_p6_residual))) /\ forall pa_i_hj32_local_total_h35s_p6_residual_product. (exists pa_lt_hj32_local_total_h35s_p6_residual_product_bound. pa_lt_hj32_local_total_h35s_p6_residual_product_bound + S pa_i_hj32_local_total_h35s_p6_residual_product = 4) -> exists pa_p_hj32_local_total_h35s_p6_residual_product pa_r_hj32_local_total_h35s_p6_residual_product pa_s_hj32_local_total_h35s_p6_residual_product. ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_factor. pa_h_hj32_local_total_h35s_p6_residual_product_factor + S (pa_p_hj32_local_total_h35s_p6_residual_product) = S ((S (pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_c_hj32_local_total_h35s_p6_residual)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_factor. pa_b_hj32_local_total_h35s_p6_residual = pa_q_hj32_local_total_h35s_p6_residual_product_factor * S ((S (pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_c_hj32_local_total_h35s_p6_residual) + (pa_p_hj32_local_total_h35s_p6_residual_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_partial. pa_h_hj32_local_total_h35s_p6_residual_product_partial + S (pa_r_hj32_local_total_h35s_p6_residual_product) = S ((S (pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_v_hj32_local_total_h35s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_partial. pa_u_hj32_local_total_h35s_p6_residual_product = pa_q_hj32_local_total_h35s_p6_residual_product_partial * S ((S (pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_v_hj32_local_total_h35s_p6_residual_product) + (pa_r_hj32_local_total_h35s_p6_residual_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_successor. pa_h_hj32_local_total_h35s_p6_residual_product_successor + S (pa_s_hj32_local_total_h35s_p6_residual_product) = S ((S (S pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_v_hj32_local_total_h35s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_successor. pa_u_hj32_local_total_h35s_p6_residual_product = pa_q_hj32_local_total_h35s_p6_residual_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_v_hj32_local_total_h35s_p6_residual_product) + (pa_s_hj32_local_total_h35s_p6_residual_product))) /\ pa_s_hj32_local_total_h35s_p6_residual_product = pa_r_hj32_local_total_h35s_p6_residual_product * pa_p_hj32_local_total_h35s_p6_residual_product))))))))
  71. 0071specialize htotal 6
  72. 0072specialize htotal 4
  73. 0073exact htotal
  74. 0074cases h35s_p6_residual
  75. 0075have h35s_p4_residual : ∃ hj32_local_value_h35s_p4_residual. Pow(4,6,hj32_local_value_h35s_p4_residual)
    Exact native replay linehave h35s_p4_residual : exists hj32_local_value_h35s_p4_residual. (exists pa_b_hj32_local_total_h35s_p4_residual pa_c_hj32_local_total_h35s_p4_residual. ((forall pa_i_hj32_local_total_h35s_p4_residual_repeat. (exists pa_lt_hj32_local_total_h35s_p4_residual_repeat_bound. pa_lt_hj32_local_total_h35s_p4_residual_repeat_bound + S pa_i_hj32_local_total_h35s_p4_residual_repeat = 6) -> (((exists pa_h_hj32_local_total_h35s_p4_residual_repeat_decoded. pa_h_hj32_local_total_h35s_p4_residual_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h35s_p4_residual_repeat)) * pa_c_hj32_local_total_h35s_p4_residual)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_repeat_decoded. pa_b_hj32_local_total_h35s_p4_residual = pa_q_hj32_local_total_h35s_p4_residual_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p4_residual_repeat)) * pa_c_hj32_local_total_h35s_p4_residual) + (4)))) /\ (exists pa_u_hj32_local_total_h35s_p4_residual_product pa_v_hj32_local_total_h35s_p4_residual_product. ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_start. pa_h_hj32_local_total_h35s_p4_residual_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_start. pa_u_hj32_local_total_h35s_p4_residual_product = pa_q_hj32_local_total_h35s_p4_residual_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p4_residual_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_terminal. pa_h_hj32_local_total_h35s_p4_residual_product_terminal + S (hj32_local_value_h35s_p4_residual) = S ((S (6)) * pa_v_hj32_local_total_h35s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_terminal. pa_u_hj32_local_total_h35s_p4_residual_product = pa_q_hj32_local_total_h35s_p4_residual_product_terminal * S ((S (6)) * pa_v_hj32_local_total_h35s_p4_residual_product) + (hj32_local_value_h35s_p4_residual))) /\ forall pa_i_hj32_local_total_h35s_p4_residual_product. (exists pa_lt_hj32_local_total_h35s_p4_residual_product_bound. pa_lt_hj32_local_total_h35s_p4_residual_product_bound + S pa_i_hj32_local_total_h35s_p4_residual_product = 6) -> exists pa_p_hj32_local_total_h35s_p4_residual_product pa_r_hj32_local_total_h35s_p4_residual_product pa_s_hj32_local_total_h35s_p4_residual_product. ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_factor. pa_h_hj32_local_total_h35s_p4_residual_product_factor + S (pa_p_hj32_local_total_h35s_p4_residual_product) = S ((S (pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_c_hj32_local_total_h35s_p4_residual)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_factor. pa_b_hj32_local_total_h35s_p4_residual = pa_q_hj32_local_total_h35s_p4_residual_product_factor * S ((S (pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_c_hj32_local_total_h35s_p4_residual) + (pa_p_hj32_local_total_h35s_p4_residual_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_partial. pa_h_hj32_local_total_h35s_p4_residual_product_partial + S (pa_r_hj32_local_total_h35s_p4_residual_product) = S ((S (pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_v_hj32_local_total_h35s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_partial. pa_u_hj32_local_total_h35s_p4_residual_product = pa_q_hj32_local_total_h35s_p4_residual_product_partial * S ((S (pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_v_hj32_local_total_h35s_p4_residual_product) + (pa_r_hj32_local_total_h35s_p4_residual_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_successor. pa_h_hj32_local_total_h35s_p4_residual_product_successor + S (pa_s_hj32_local_total_h35s_p4_residual_product) = S ((S (S pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_v_hj32_local_total_h35s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_successor. pa_u_hj32_local_total_h35s_p4_residual_product = pa_q_hj32_local_total_h35s_p4_residual_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_v_hj32_local_total_h35s_p4_residual_product) + (pa_s_hj32_local_total_h35s_p4_residual_product))) /\ pa_s_hj32_local_total_h35s_p4_residual_product = pa_r_hj32_local_total_h35s_p4_residual_product * pa_p_hj32_local_total_h35s_p4_residual_product))))))))
  76. 0076specialize htotal 4
  77. 0077specialize htotal 6
  78. 0078exact htotal
  79. 0079cases h35s_p4_residual
  80. 0080have h35s_residual_bound : Le(x4,x5)
    Exact native replay linehave h35s_residual_bound : exists bqb_le_gap_hj32_h35s_residual_bound. bqb_le_gap_hj32_h35s_residual_bound + (x4) = (x5)
  81. 0081specialize pow_six_four_le_pow_four_six_from_total x4
  82. 0082specialize pow_six_four_le_pow_four_six_from_total x5
  83. 0083apply pow_six_four_le_pow_four_six_from_total
  84. 0084exact htotal
  85. 0085exact h35s_p6_residual_witness
  86. 0086exact h35s_p4_residual_witness
  87. 0087have h35s_exponent : 4 * 36 = 10 * 14 + 4
  88. 0088have h35s_thirty_six : 36 = 5 * 7 + 1
  89. 0089norm_num
  90. 0090rewrite h35s_thirty_six
  91. 0091have h35s_distrib : 4 * (5 * 7 + 1) = 4 * (5 * 7) + 4 * 1
  92. 0092specialize mul_add 4
  93. 0093specialize mul_add (5 * 7)
  94. 0094specialize mul_add 1
  95. 0095apply mul_add
  96. 0096rewrite h35s_distrib
  97. 0097have h35s_left_assoc : 4 * (5 * 7) = (4 * 5) * 7
  98. 0098symm
  99. 0099specialize mul_assoc 4
  100. 0100specialize mul_assoc 5
  101. 0101specialize mul_assoc 7
  102. 0102apply mul_assoc
  103. 0103rewrite h35s_left_assoc
  104. 0104have h35s_fourteen : 14 = 2 * 7
  105. 0105norm_num
  106. 0106rewrite h35s_fourteen
  107. 0107have h35s_right_assoc : 10 * (2 * 7) = (10 * 2) * 7
  108. 0108symm
  109. 0109specialize mul_assoc 10
  110. 0110specialize mul_assoc 2
  111. 0111specialize mul_assoc 7
  112. 0112apply mul_assoc
  113. 0113rewrite h35s_right_assoc
  114. 0114have h35s_right_twenty : 10 * 2 = 20
  115. 0115norm_num
  116. 0116rewrite h35s_right_twenty
  117. 0117have h35s_twenty : 4 * 5 = 20
  118. 0118norm_num
  119. 0119rewrite h35s_twenty
  120. 0120have h35s_four : 4 * 1 = 4
  121. 0121norm_num
  122. 0122rewrite h35s_four
  123. 0123refl
  124. 0124have h35s_left_product : x1 = x2 * x4
  125. 0125specialize pow_add 6
  126. 0126specialize pow_add 10 * 14
  127. 0127specialize pow_add 4
  128. 0128specialize pow_add 4 * 36
  129. 0129specialize pow_add x2
  130. 0130specialize pow_add x4
  131. 0131specialize pow_add x1
  132. 0132apply pow_add
  133. 0133exact h35s_exponent
  134. 0134exact h35s_p6_main_witness
  135. 0135exact h35s_p6_residual_witness
  136. 0136exact h35s_p6_total_witness
  137. 0137have h35s_p4_budget : ∃ hj32_local_value_h35s_p4_budget. Pow(4,13 · 14 + 6,hj32_local_value_h35s_p4_budget)
    Exact native replay linehave h35s_p4_budget : exists hj32_local_value_h35s_p4_budget. (exists pa_b_hj32_local_total_h35s_p4_budget pa_c_hj32_local_total_h35s_p4_budget. ((forall pa_i_hj32_local_total_h35s_p4_budget_repeat. (exists pa_lt_hj32_local_total_h35s_p4_budget_repeat_bound. pa_lt_hj32_local_total_h35s_p4_budget_repeat_bound + S pa_i_hj32_local_total_h35s_p4_budget_repeat = 13 * 14 + 6) -> (((exists pa_h_hj32_local_total_h35s_p4_budget_repeat_decoded. pa_h_hj32_local_total_h35s_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h35s_p4_budget_repeat)) * pa_c_hj32_local_total_h35s_p4_budget)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_repeat_decoded. pa_b_hj32_local_total_h35s_p4_budget = pa_q_hj32_local_total_h35s_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p4_budget_repeat)) * pa_c_hj32_local_total_h35s_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h35s_p4_budget_product pa_v_hj32_local_total_h35s_p4_budget_product. ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_start. pa_h_hj32_local_total_h35s_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_start. pa_u_hj32_local_total_h35s_p4_budget_product = pa_q_hj32_local_total_h35s_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_terminal. pa_h_hj32_local_total_h35s_p4_budget_product_terminal + S (hj32_local_value_h35s_p4_budget) = S ((S (13 * 14 + 6)) * pa_v_hj32_local_total_h35s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_terminal. pa_u_hj32_local_total_h35s_p4_budget_product = pa_q_hj32_local_total_h35s_p4_budget_product_terminal * S ((S (13 * 14 + 6)) * pa_v_hj32_local_total_h35s_p4_budget_product) + (hj32_local_value_h35s_p4_budget))) /\ forall pa_i_hj32_local_total_h35s_p4_budget_product. (exists pa_lt_hj32_local_total_h35s_p4_budget_product_bound. pa_lt_hj32_local_total_h35s_p4_budget_product_bound + S pa_i_hj32_local_total_h35s_p4_budget_product = 13 * 14 + 6) -> exists pa_p_hj32_local_total_h35s_p4_budget_product pa_r_hj32_local_total_h35s_p4_budget_product pa_s_hj32_local_total_h35s_p4_budget_product. ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_factor. pa_h_hj32_local_total_h35s_p4_budget_product_factor + S (pa_p_hj32_local_total_h35s_p4_budget_product) = S ((S (pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_c_hj32_local_total_h35s_p4_budget)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_factor. pa_b_hj32_local_total_h35s_p4_budget = pa_q_hj32_local_total_h35s_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_c_hj32_local_total_h35s_p4_budget) + (pa_p_hj32_local_total_h35s_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_partial. pa_h_hj32_local_total_h35s_p4_budget_product_partial + S (pa_r_hj32_local_total_h35s_p4_budget_product) = S ((S (pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_v_hj32_local_total_h35s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_partial. pa_u_hj32_local_total_h35s_p4_budget_product = pa_q_hj32_local_total_h35s_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_v_hj32_local_total_h35s_p4_budget_product) + (pa_r_hj32_local_total_h35s_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_successor. pa_h_hj32_local_total_h35s_p4_budget_product_successor + S (pa_s_hj32_local_total_h35s_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_v_hj32_local_total_h35s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_successor. pa_u_hj32_local_total_h35s_p4_budget_product = pa_q_hj32_local_total_h35s_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_v_hj32_local_total_h35s_p4_budget_product) + (pa_s_hj32_local_total_h35s_p4_budget_product))) /\ pa_s_hj32_local_total_h35s_p4_budget_product = pa_r_hj32_local_total_h35s_p4_budget_product * pa_p_hj32_local_total_h35s_p4_budget_product))))))))
  138. 0138specialize htotal 4
  139. 0139specialize htotal 13 * 14 + 6
  140. 0140exact htotal
  141. 0141cases h35s_p4_budget
  142. 0142have h35s_right_product : x6 = x3 * x5
  143. 0143specialize pow_add 4
  144. 0144specialize pow_add 13 * 14
  145. 0145specialize pow_add 6
  146. 0146specialize pow_add 13 * 14 + 6
  147. 0147specialize pow_add x3
  148. 0148specialize pow_add x5
  149. 0149specialize pow_add x6
  150. 0150apply pow_add
  151. 0151refl
  152. 0152exact h35s_p4_main_witness
  153. 0153exact h35s_p4_residual_witness
  154. 0154exact h35s_p4_budget_witness
  155. 0155have h35s_six_bound : Le(x2 · x4,x3 · x5)
    Exact native replay linehave h35s_six_bound : exists bqb_le_gap_hj32_local_product_bound_h35s_six_bound. bqb_le_gap_hj32_local_product_bound_h35s_six_bound + (x2 * x4) = (x3 * x5)
  156. 0156specialize mul_le_mul x2
  157. 0157specialize mul_le_mul x3
  158. 0158specialize mul_le_mul x4
  159. 0159specialize mul_le_mul x5
  160. 0160apply mul_le_mul
  161. 0161exact h35s_main_bound
  162. 0162exact h35s_residual_bound
  163. 0163rewrite <- h35s_left_product at h35s_six_bound
  164. 0164rewrite <- h35s_right_product at h35s_six_bound
  165. 0165have h35s_to_budget : Le(h,x6)
    Exact native replay linehave h35s_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h35s_to_budget. bqb_le_gap_hj32_local_trans_bound_h35s_to_budget + (h) = (x6)
  166. 0166specialize le_trans h
  167. 0167specialize le_trans x1
  168. 0168specialize le_trans x6
  169. 0169apply le_trans
  170. 0170exact h35s_to_36
  171. 0171exact h35s_six_bound
  172. 0172have hscaled : Le(6 · (13 · 14 + 6),35 · 35)
    Exact native replay linehave hscaled : exists bqb_le_gap_hj32_scaled_budget_root_35. bqb_le_gap_hj32_scaled_budget_root_35 + (6 * (13 * 14 + 6)) = (35 * 35)
  173. 0173apply bertrand_scaled_budget_root_35
  174. 0174have hbudget_exponent : Le(13 · 14 + 6,e)
    Exact native replay linehave hbudget_exponent : exists bqb_le_gap_hj32_h_35_budget_exponent. bqb_le_gap_hj32_h_35_budget_exponent + (13 * 14 + 6) = (e)
  175. 0175specialize ceil_div_six_budget_of_scaled_le (35 * 35)
  176. 0176specialize ceil_div_six_budget_of_scaled_le (13 * 14 + 6)
  177. 0177specialize ceil_div_six_budget_of_scaled_le e
  178. 0178apply ceil_div_six_budget_of_scaled_le
  179. 0179exact hceiling
  180. 0180exact hscaled
  181. 0181have h35_budget_growth : Le(x6,u)
    Exact native replay linehave h35_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h35_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h35_budget_growth + (x6) = (u)
  182. 0182specialize pow_exponent_monotone_from_total 4
  183. 0183specialize pow_exponent_monotone_from_total 13 * 14 + 6
  184. 0184specialize pow_exponent_monotone_from_total e
  185. 0185specialize pow_exponent_monotone_from_total x6
  186. 0186specialize pow_exponent_monotone_from_total u
  187. 0187apply pow_exponent_monotone_from_total
  188. 0188exact htotal
  189. 0189exists 3
  190. 0190norm_num
  191. 0191exact hbudget_exponent
  192. 0192exact h35s_p4_budget_witness
  193. 0193exact hu
  194. 0194have h35_result : Le(h,u)
    Exact native replay linehave h35_result : exists bqb_le_gap_hj32_local_trans_bound_h35_result. bqb_le_gap_hj32_local_trans_bound_h35_result + (h) = (u)
  195. 0195specialize le_trans h
  196. 0196specialize le_trans x6
  197. 0197specialize le_trans u
  198. 0198apply le_trans
  199. 0199exact h35s_to_budget
  200. 0200exact h35_budget_growth
  201. 0201exact h35_result