BT00WQ · Bertrand theorem

bertrand_h_root_33_from_total

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

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

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(33 · 33,e) → Pow(33 + 1,2 · 33 + 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_33 bpt_e_hj32_h_root_33. exists bpt_x_hj32_h_root_33. (exists ff_b_bpt_value_hj32_h_root_33 ff_c_bpt_value_hj32_h_root_33. ((forall ff_i_bpt_value_hj32_h_root_33_repeat. (exists ff_lt_bpt_value_hj32_h_root_33_repeat_bound. ff_lt_bpt_value_hj32_h_root_33_repeat_bound + S ff_i_bpt_value_hj32_h_root_33_repeat = bpt_e_hj32_h_root_33) -> (((exists ff_h_bpt_value_hj32_h_root_33_repeat_decoded. ff_h_bpt_value_hj32_h_root_33_repeat_decoded + S (bpt_a_hj32_h_root_33) = S ((S (ff_i_bpt_value_hj32_h_root_33_repeat)) * ff_c_bpt_value_hj32_h_root_33)) /\ exists ff_q_bpt_value_hj32_h_root_33_repeat_decoded. ff_b_bpt_value_hj32_h_root_33 = ff_q_bpt_value_hj32_h_root_33_repeat_decoded * S ((S (ff_i_bpt_value_hj32_h_root_33_repeat)) * ff_c_bpt_value_hj32_h_root_33) + (bpt_a_hj32_h_root_33)))) /\ (exists ff_u_bpt_value_hj32_h_root_33_product ff_v_bpt_value_hj32_h_root_33_product. ((((exists ff_h_bpt_value_hj32_h_root_33_product_start. ff_h_bpt_value_hj32_h_root_33_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_h_root_33_product)) /\ exists ff_q_bpt_value_hj32_h_root_33_product_start. ff_u_bpt_value_hj32_h_root_33_product = ff_q_bpt_value_hj32_h_root_33_product_start * S ((S (0)) * ff_v_bpt_value_hj32_h_root_33_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_h_root_33_product_terminal. ff_h_bpt_value_hj32_h_root_33_product_terminal + S (bpt_x_hj32_h_root_33) = S ((S (bpt_e_hj32_h_root_33)) * ff_v_bpt_value_hj32_h_root_33_product)) /\ exists ff_q_bpt_value_hj32_h_root_33_product_terminal. ff_u_bpt_value_hj32_h_root_33_product = ff_q_bpt_value_hj32_h_root_33_product_terminal * S ((S (bpt_e_hj32_h_root_33)) * ff_v_bpt_value_hj32_h_root_33_product) + (bpt_x_hj32_h_root_33))) /\ forall ff_i_bpt_value_hj32_h_root_33_product. (exists ff_lt_bpt_value_hj32_h_root_33_product_bound. ff_lt_bpt_value_hj32_h_root_33_product_bound + S ff_i_bpt_value_hj32_h_root_33_product = bpt_e_hj32_h_root_33) -> exists ff_p_bpt_value_hj32_h_root_33_product ff_r_bpt_value_hj32_h_root_33_product ff_s_bpt_value_hj32_h_root_33_product. ((((exists ff_h_bpt_value_hj32_h_root_33_product_factor. ff_h_bpt_value_hj32_h_root_33_product_factor + S (ff_p_bpt_value_hj32_h_root_33_product) = S ((S (ff_i_bpt_value_hj32_h_root_33_product)) * ff_c_bpt_value_hj32_h_root_33)) /\ exists ff_q_bpt_value_hj32_h_root_33_product_factor. ff_b_bpt_value_hj32_h_root_33 = ff_q_bpt_value_hj32_h_root_33_product_factor * S ((S (ff_i_bpt_value_hj32_h_root_33_product)) * ff_c_bpt_value_hj32_h_root_33) + (ff_p_bpt_value_hj32_h_root_33_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_33_product_partial. ff_h_bpt_value_hj32_h_root_33_product_partial + S (ff_r_bpt_value_hj32_h_root_33_product) = S ((S (ff_i_bpt_value_hj32_h_root_33_product)) * ff_v_bpt_value_hj32_h_root_33_product)) /\ exists ff_q_bpt_value_hj32_h_root_33_product_partial. ff_u_bpt_value_hj32_h_root_33_product = ff_q_bpt_value_hj32_h_root_33_product_partial * S ((S (ff_i_bpt_value_hj32_h_root_33_product)) * ff_v_bpt_value_hj32_h_root_33_product) + (ff_r_bpt_value_hj32_h_root_33_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_33_product_successor. ff_h_bpt_value_hj32_h_root_33_product_successor + S (ff_s_bpt_value_hj32_h_root_33_product) = S ((S (S ff_i_bpt_value_hj32_h_root_33_product)) * ff_v_bpt_value_hj32_h_root_33_product)) /\ exists ff_q_bpt_value_hj32_h_root_33_product_successor. ff_u_bpt_value_hj32_h_root_33_product = ff_q_bpt_value_hj32_h_root_33_product_successor * S ((S (S ff_i_bpt_value_hj32_h_root_33_product)) * ff_v_bpt_value_hj32_h_root_33_product) + (ff_s_bpt_value_hj32_h_root_33_product))) /\ ff_s_bpt_value_hj32_h_root_33_product = ff_r_bpt_value_hj32_h_root_33_product * ff_p_bpt_value_hj32_h_root_33_product))))))))) -> (((exists bcs_lower_gap_hj32_h_root_33_ceiling. bcs_lower_gap_hj32_h_root_33_ceiling + (33 * 33) = 6 * (e)) /\ exists bcs_upper_gap_hj32_h_root_33_ceiling. bcs_upper_gap_hj32_h_root_33_ceiling + S (6 * (e)) = (33 * 33) + 6)) -> (exists pa_b_hj32_h_root_33_h pa_c_hj32_h_root_33_h. ((forall pa_i_hj32_h_root_33_h_repeat. (exists pa_lt_hj32_h_root_33_h_repeat_bound. pa_lt_hj32_h_root_33_h_repeat_bound + S pa_i_hj32_h_root_33_h_repeat = 2 * 33 + 2) -> (((exists pa_h_hj32_h_root_33_h_repeat_decoded. pa_h_hj32_h_root_33_h_repeat_decoded + S (33 + 1) = S ((S (pa_i_hj32_h_root_33_h_repeat)) * pa_c_hj32_h_root_33_h)) /\ exists pa_q_hj32_h_root_33_h_repeat_decoded. pa_b_hj32_h_root_33_h = pa_q_hj32_h_root_33_h_repeat_decoded * S ((S (pa_i_hj32_h_root_33_h_repeat)) * pa_c_hj32_h_root_33_h) + (33 + 1)))) /\ (exists pa_u_hj32_h_root_33_h_product pa_v_hj32_h_root_33_h_product. ((((exists pa_h_hj32_h_root_33_h_product_start. pa_h_hj32_h_root_33_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_33_h_product)) /\ exists pa_q_hj32_h_root_33_h_product_start. pa_u_hj32_h_root_33_h_product = pa_q_hj32_h_root_33_h_product_start * S ((S (0)) * pa_v_hj32_h_root_33_h_product) + (1))) /\ ((((exists pa_h_hj32_h_root_33_h_product_terminal. pa_h_hj32_h_root_33_h_product_terminal + S (h) = S ((S (2 * 33 + 2)) * pa_v_hj32_h_root_33_h_product)) /\ exists pa_q_hj32_h_root_33_h_product_terminal. pa_u_hj32_h_root_33_h_product = pa_q_hj32_h_root_33_h_product_terminal * S ((S (2 * 33 + 2)) * pa_v_hj32_h_root_33_h_product) + (h))) /\ forall pa_i_hj32_h_root_33_h_product. (exists pa_lt_hj32_h_root_33_h_product_bound. pa_lt_hj32_h_root_33_h_product_bound + S pa_i_hj32_h_root_33_h_product = 2 * 33 + 2) -> exists pa_p_hj32_h_root_33_h_product pa_r_hj32_h_root_33_h_product pa_s_hj32_h_root_33_h_product. ((((exists pa_h_hj32_h_root_33_h_product_factor. pa_h_hj32_h_root_33_h_product_factor + S (pa_p_hj32_h_root_33_h_product) = S ((S (pa_i_hj32_h_root_33_h_product)) * pa_c_hj32_h_root_33_h)) /\ exists pa_q_hj32_h_root_33_h_product_factor. pa_b_hj32_h_root_33_h = pa_q_hj32_h_root_33_h_product_factor * S ((S (pa_i_hj32_h_root_33_h_product)) * pa_c_hj32_h_root_33_h) + (pa_p_hj32_h_root_33_h_product))) /\ ((((exists pa_h_hj32_h_root_33_h_product_partial. pa_h_hj32_h_root_33_h_product_partial + S (pa_r_hj32_h_root_33_h_product) = S ((S (pa_i_hj32_h_root_33_h_product)) * pa_v_hj32_h_root_33_h_product)) /\ exists pa_q_hj32_h_root_33_h_product_partial. pa_u_hj32_h_root_33_h_product = pa_q_hj32_h_root_33_h_product_partial * S ((S (pa_i_hj32_h_root_33_h_product)) * pa_v_hj32_h_root_33_h_product) + (pa_r_hj32_h_root_33_h_product))) /\ ((((exists pa_h_hj32_h_root_33_h_product_successor. pa_h_hj32_h_root_33_h_product_successor + S (pa_s_hj32_h_root_33_h_product) = S ((S (S pa_i_hj32_h_root_33_h_product)) * pa_v_hj32_h_root_33_h_product)) /\ exists pa_q_hj32_h_root_33_h_product_successor. pa_u_hj32_h_root_33_h_product = pa_q_hj32_h_root_33_h_product_successor * S ((S (S pa_i_hj32_h_root_33_h_product)) * pa_v_hj32_h_root_33_h_product) + (pa_s_hj32_h_root_33_h_product))) /\ pa_s_hj32_h_root_33_h_product = pa_r_hj32_h_root_33_h_product * pa_p_hj32_h_root_33_h_product)))))))) -> (exists pa_b_hj32_h_root_33_u pa_c_hj32_h_root_33_u. ((forall pa_i_hj32_h_root_33_u_repeat. (exists pa_lt_hj32_h_root_33_u_repeat_bound. pa_lt_hj32_h_root_33_u_repeat_bound + S pa_i_hj32_h_root_33_u_repeat = e) -> (((exists pa_h_hj32_h_root_33_u_repeat_decoded. pa_h_hj32_h_root_33_u_repeat_decoded + S (4) = S ((S (pa_i_hj32_h_root_33_u_repeat)) * pa_c_hj32_h_root_33_u)) /\ exists pa_q_hj32_h_root_33_u_repeat_decoded. pa_b_hj32_h_root_33_u = pa_q_hj32_h_root_33_u_repeat_decoded * S ((S (pa_i_hj32_h_root_33_u_repeat)) * pa_c_hj32_h_root_33_u) + (4)))) /\ (exists pa_u_hj32_h_root_33_u_product pa_v_hj32_h_root_33_u_product. ((((exists pa_h_hj32_h_root_33_u_product_start. pa_h_hj32_h_root_33_u_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_33_u_product)) /\ exists pa_q_hj32_h_root_33_u_product_start. pa_u_hj32_h_root_33_u_product = pa_q_hj32_h_root_33_u_product_start * S ((S (0)) * pa_v_hj32_h_root_33_u_product) + (1))) /\ ((((exists pa_h_hj32_h_root_33_u_product_terminal. pa_h_hj32_h_root_33_u_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_h_root_33_u_product)) /\ exists pa_q_hj32_h_root_33_u_product_terminal. pa_u_hj32_h_root_33_u_product = pa_q_hj32_h_root_33_u_product_terminal * S ((S (e)) * pa_v_hj32_h_root_33_u_product) + (u))) /\ forall pa_i_hj32_h_root_33_u_product. (exists pa_lt_hj32_h_root_33_u_product_bound. pa_lt_hj32_h_root_33_u_product_bound + S pa_i_hj32_h_root_33_u_product = e) -> exists pa_p_hj32_h_root_33_u_product pa_r_hj32_h_root_33_u_product pa_s_hj32_h_root_33_u_product. ((((exists pa_h_hj32_h_root_33_u_product_factor. pa_h_hj32_h_root_33_u_product_factor + S (pa_p_hj32_h_root_33_u_product) = S ((S (pa_i_hj32_h_root_33_u_product)) * pa_c_hj32_h_root_33_u)) /\ exists pa_q_hj32_h_root_33_u_product_factor. pa_b_hj32_h_root_33_u = pa_q_hj32_h_root_33_u_product_factor * S ((S (pa_i_hj32_h_root_33_u_product)) * pa_c_hj32_h_root_33_u) + (pa_p_hj32_h_root_33_u_product))) /\ ((((exists pa_h_hj32_h_root_33_u_product_partial. pa_h_hj32_h_root_33_u_product_partial + S (pa_r_hj32_h_root_33_u_product) = S ((S (pa_i_hj32_h_root_33_u_product)) * pa_v_hj32_h_root_33_u_product)) /\ exists pa_q_hj32_h_root_33_u_product_partial. pa_u_hj32_h_root_33_u_product = pa_q_hj32_h_root_33_u_product_partial * S ((S (pa_i_hj32_h_root_33_u_product)) * pa_v_hj32_h_root_33_u_product) + (pa_r_hj32_h_root_33_u_product))) /\ ((((exists pa_h_hj32_h_root_33_u_product_successor. pa_h_hj32_h_root_33_u_product_successor + S (pa_s_hj32_h_root_33_u_product) = S ((S (S pa_i_hj32_h_root_33_u_product)) * pa_v_hj32_h_root_33_u_product)) /\ exists pa_q_hj32_h_root_33_u_product_successor. pa_u_hj32_h_root_33_u_product = pa_q_hj32_h_root_33_u_product_successor * S ((S (S pa_i_hj32_h_root_33_u_product)) * pa_v_hj32_h_root_33_u_product) + (pa_s_hj32_h_root_33_u_product))) /\ pa_s_hj32_h_root_33_u_product = pa_r_hj32_h_root_33_u_product * pa_p_hj32_h_root_33_u_product)))))))) -> (exists bqb_le_gap_hj32_h_root_33_result. bqb_le_gap_hj32_h_root_33_result + (h) = (u))

Proof neighborhood

Direct theorem prerequisites

BT00W9 bertrand_scaled_budget_root_33 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 BT00WF pow_six_six_le_pow_four_eight_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 BT000B add_mul 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

206 script commands · 48 reading checkpoints · 33 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (13)
bertrand scaled budget root 33ceil 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 six le pow four eight from totalpow addpow base monotonepow exponent monotone from totalmul le mulle transmul addadd muladd 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(34,2 · 34,h)Definitions: Pow(34,2 · 34,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 : 33 + 1 = 34
  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 * 33 + 2 = 2 * 34
  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 h33s_p36L20–23

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

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

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

  1. L24
    cases h33s_p36
07Establish h33s_baseL25–25

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

  1. L25
    have h33s_base : Lt(33,36)Definitions: Lt(33,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 2
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 h33s_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 h33s_to_36 : Le(h,x)Definitions: Le(h,x)Original native command in the exact edition
  2. L29
    specialize pow_base_monotone 34
  3. L30
    specialize pow_base_monotone 36
  4. L31
    specialize pow_base_monotone 2 * 34
  5. L32
    specialize pow_base_monotone h
  6. L33
    specialize pow_base_monotone x
  7. L34
    apply pow_base_monotone
  8. L35
    exact h33s_base
  9. L36
    exact hh_route
  10. L37
    exact h33s_p36_witness
11Establish h33s_p6_totalL38–41

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

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

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

  1. L42
    cases h33s_p6_total
13Establish h33s_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 h33s_conversion : x = x1
  2. L44
    specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total 34
  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 h33s_p36_witness
  8. L50
    exact h33s_p6_total_witness
  9. L51
    rewrite h33s_conversion at h33s_to_36
14Establish h33s_p6_mainL52–55

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

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

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

  1. L56
    cases h33s_p6_main
16Establish h33s_p4_mainL57–60

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

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

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

  1. L61
    cases h33s_p4_main
18Establish h33s_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 h33s_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 13
  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 h33s_p6_main_witness
  8. L69
    exact h33s_p4_main_witness
19Establish h33s_p6_residualL70–73

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

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

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

  1. L74
    cases h33s_p6_residual
21Establish h33s_p4_residualL75–78

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

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

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

  1. L79
    cases h33s_p4_residual
23Establish h33s_residual_boundL80–86

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

  1. L80
    have h33s_residual_bound : Le(x4,x5)Definitions: Le(x4,x5)Original native command in the exact edition
  2. L81
    specialize pow_six_six_le_pow_four_eight_from_total x4
  3. L82
    specialize pow_six_six_le_pow_four_eight_from_total x5
  4. L83
    apply pow_six_six_le_pow_four_eight_from_total
  5. L84
    exact htotal
  6. L85
    exact h33s_p6_residual_witness
  7. L86
    exact h33s_p4_residual_witness
24Establish h33s_exponentL87–87

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

  1. L87
    have h33s_exponent : 4 * 34 = 10 * 13 + 6
25Establish h33s_thirty_fourL88–90

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

  1. L88
    have h33s_thirty_four : 34 = 13 + 21
  2. L89
    norm_num
  3. L90
    rewrite h33s_thirty_four
26Establish h33s_distrib_oneL91–96

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

  1. L91
    have h33s_distrib_one : 4 * (13 + 21) = 4 * 13 + 4 * 21
  2. L92
    specialize mul_add 4
  3. L93
    specialize mul_add 13
  4. L94
    specialize mul_add 21
  5. L95
    apply mul_add
  6. L96
    rewrite h33s_distrib_one
27Establish h33s_bridgeL97–99

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

  1. L97
    have h33s_bridge : 4 * 21 = 6 * 14
  2. L98
    norm_num
  3. L99
    rewrite h33s_bridge
28Establish h33s_fourteenL100–102

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

  1. L100
    have h33s_fourteen : 14 = 13 + 1
  2. L101
    norm_num
  3. L102
    rewrite h33s_fourteen
29Establish h33s_distrib_twoL103–108

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

  1. L103
    have h33s_distrib_two : 6 * (13 + 1) = 6 * 13 + 6 * 1
  2. L104
    specialize mul_add 6
  3. L105
    specialize mul_add 13
  4. L106
    specialize mul_add 1
  5. L107
    apply mul_add
  6. L108
    rewrite h33s_distrib_two
30Establish h33s_sixL109–111

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

  1. L109
    have h33s_six : 6 * 1 = 6
  2. L110
    norm_num
  3. L111
    rewrite h33s_six
31Establish h33s_assocL112–118

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

  1. L112
    have h33s_assoc : 4 * 13 + (6 * 13 + 6) = (4 * 13 + 6 * 13) + 6
  2. L113
    symm
  3. L114
    specialize add_assoc (4 * 13)
  4. L115
    specialize add_assoc (6 * 13)
  5. L116
    specialize add_assoc 6
  6. L117
    apply add_assoc
  7. L118
    rewrite h33s_assoc
32Establish h33s_factorL119–124

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

  1. L119
    have h33s_factor : (4 + 6) * 13 = 4 * 13 + 6 * 13
  2. L120
    specialize add_mul 4
  3. L121
    specialize add_mul 6
  4. L122
    specialize add_mul 13
  5. L123
    apply add_mul
  6. L124
    rewrite <- h33s_factor
33Establish h33s_tenL125–128

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

  1. L125
    have h33s_ten : 4 + 6 = 10
  2. L126
    norm_num
  3. L127
    rewrite h33s_ten
  4. L128
    refl
34Establish h33s_left_productL129–138

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

  1. L129
    have h33s_left_product : x1 = x2 * x4
  2. L130
    specialize pow_add 6
  3. L131
    specialize pow_add 10 * 13
  4. L132
    specialize pow_add 6
  5. L133
    specialize pow_add 4 * 34
  6. L134
    specialize pow_add x2
  7. L135
    specialize pow_add x4
  8. L136
    specialize pow_add x1
  9. L137
    apply pow_add
  10. L138
    exact h33s_exponent
35Use earlier factsL139–141

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

  1. L139
    exact h33s_p6_main_witness
  2. L140
    exact h33s_p6_residual_witness
  3. L141
    exact h33s_p6_total_witness
36Establish h33s_p4_budgetL142–145

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

  1. L142
    have h33s_p4_budget : ∃ hj32_local_value_h33s_p4_budget. Pow(4,13 · 13 + 8,hj32_local_value_h33s_p4_budget)Definitions: Pow(4,13 · 13 + 8,hj32_local_value_h33s_p4_budget)Original native command in the exact edition
  2. L143
    specialize htotal 4
  3. L144
    specialize htotal 13 * 13 + 8
  4. L145
    exact htotal
37Separate the logical casesL146–146

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

  1. L146
    cases h33s_p4_budget
38Establish h33s_right_productL147–156

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

  1. L147
    have h33s_right_product : x6 = x3 * x5
  2. L148
    specialize pow_add 4
  3. L149
    specialize pow_add 13 * 13
  4. L150
    specialize pow_add 8
  5. L151
    specialize pow_add 13 * 13 + 8
  6. L152
    specialize pow_add x3
  7. L153
    specialize pow_add x5
  8. L154
    specialize pow_add x6
  9. L155
    apply pow_add
  10. L156
    refl
39Use earlier factsL157–159

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

  1. L157
    exact h33s_p4_main_witness
  2. L158
    exact h33s_p4_residual_witness
  3. L159
    exact h33s_p4_budget_witness
40Establish h33s_six_boundL160–169

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

  1. L160
    have h33s_six_bound : Le(x2 · x4,x3 · x5)Definitions: Le(x2 · x4,x3 · x5)Original native command in the exact edition
  2. L161
    specialize mul_le_mul x2
  3. L162
    specialize mul_le_mul x3
  4. L163
    specialize mul_le_mul x4
  5. L164
    specialize mul_le_mul x5
  6. L165
    apply mul_le_mul
  7. L166
    exact h33s_main_bound
  8. L167
    exact h33s_residual_bound
  9. L168
    rewrite <- h33s_left_product at h33s_six_bound
  10. L169
    rewrite <- h33s_right_product at h33s_six_bound
41Establish h33s_to_budgetL170–176

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

  1. L170
    have h33s_to_budget : Le(h,x6)Definitions: Le(h,x6)Original native command in the exact edition
  2. L171
    specialize le_trans h
  3. L172
    specialize le_trans x1
  4. L173
    specialize le_trans x6
  5. L174
    apply le_trans
  6. L175
    exact h33s_to_36
  7. L176
    exact h33s_six_bound
42Establish hscaledL177–178

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

  1. L177
    have hscaled : Le(6 · (13 · 13 + 8),33 · 33)Definitions: Le(6 · (13 · 13 + 8),33 · 33)Original native command in the exact edition
  2. L178
    apply bertrand_scaled_budget_root_33
43Establish hbudget_exponentL179–185

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. L179
    have hbudget_exponent : Le(13 · 13 + 8,e)Definitions: Le(13 · 13 + 8,e)Original native command in the exact edition
  2. L180
    specialize ceil_div_six_budget_of_scaled_le (33 * 33)
  3. L181
    specialize ceil_div_six_budget_of_scaled_le (13 * 13 + 8)
  4. L182
    specialize ceil_div_six_budget_of_scaled_le e
  5. L183
    apply ceil_div_six_budget_of_scaled_le
  6. L184
    exact hceiling
  7. L185
    exact hscaled
44Establish h33_budget_growthL186–193

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

  1. L186
    have h33_budget_growth : Le(x6,u)Definitions: Le(x6,u)Original native command in the exact edition
  2. L187
    specialize pow_exponent_monotone_from_total 4
  3. L188
    specialize pow_exponent_monotone_from_total 13 * 13 + 8
  4. L189
    specialize pow_exponent_monotone_from_total e
  5. L190
    specialize pow_exponent_monotone_from_total x6
  6. L191
    specialize pow_exponent_monotone_from_total u
  7. L192
    apply pow_exponent_monotone_from_total
  8. L193
    exact htotal
45Construct an explicit witnessL194–194

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

  1. L194
    exists 3
46Calculate and transport equalitiesL195–195

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

  1. L195
    norm_num
47Use earlier factsL196–198

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

  1. L196
    exact hbudget_exponent
  2. L197
    exact h33s_p4_budget_witness
  3. L198
    exact hu
48Establish h33_resultL199–206

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

  1. L199
    have h33_result : Le(h,u)Definitions: Le(h,u)Original native command in the exact edition
  2. L200
    specialize le_trans h
  3. L201
    specialize le_trans x6
  4. L202
    specialize le_trans u
  5. L203
    apply le_trans
  6. L204
    exact h33s_to_budget
  7. L205
    exact h33_budget_growth
  8. L206
    exact h33_result

Library-wide reading audit

Original defined command ledger · 206 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(34,2 · 34,h)
    Exact native replay linehave hh_route : exists pa_b_hj32_h_33_route pa_c_hj32_h_33_route. ((forall pa_i_hj32_h_33_route_repeat. (exists pa_lt_hj32_h_33_route_repeat_bound. pa_lt_hj32_h_33_route_repeat_bound + S pa_i_hj32_h_33_route_repeat = 2 * 34) -> (((exists pa_h_hj32_h_33_route_repeat_decoded. pa_h_hj32_h_33_route_repeat_decoded + S (34) = S ((S (pa_i_hj32_h_33_route_repeat)) * pa_c_hj32_h_33_route)) /\ exists pa_q_hj32_h_33_route_repeat_decoded. pa_b_hj32_h_33_route = pa_q_hj32_h_33_route_repeat_decoded * S ((S (pa_i_hj32_h_33_route_repeat)) * pa_c_hj32_h_33_route) + (34)))) /\ (exists pa_u_hj32_h_33_route_product pa_v_hj32_h_33_route_product. ((((exists pa_h_hj32_h_33_route_product_start. pa_h_hj32_h_33_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_33_route_product)) /\ exists pa_q_hj32_h_33_route_product_start. pa_u_hj32_h_33_route_product = pa_q_hj32_h_33_route_product_start * S ((S (0)) * pa_v_hj32_h_33_route_product) + (1))) /\ ((((exists pa_h_hj32_h_33_route_product_terminal. pa_h_hj32_h_33_route_product_terminal + S (h) = S ((S (2 * 34)) * pa_v_hj32_h_33_route_product)) /\ exists pa_q_hj32_h_33_route_product_terminal. pa_u_hj32_h_33_route_product = pa_q_hj32_h_33_route_product_terminal * S ((S (2 * 34)) * pa_v_hj32_h_33_route_product) + (h))) /\ forall pa_i_hj32_h_33_route_product. (exists pa_lt_hj32_h_33_route_product_bound. pa_lt_hj32_h_33_route_product_bound + S pa_i_hj32_h_33_route_product = 2 * 34) -> exists pa_p_hj32_h_33_route_product pa_r_hj32_h_33_route_product pa_s_hj32_h_33_route_product. ((((exists pa_h_hj32_h_33_route_product_factor. pa_h_hj32_h_33_route_product_factor + S (pa_p_hj32_h_33_route_product) = S ((S (pa_i_hj32_h_33_route_product)) * pa_c_hj32_h_33_route)) /\ exists pa_q_hj32_h_33_route_product_factor. pa_b_hj32_h_33_route = pa_q_hj32_h_33_route_product_factor * S ((S (pa_i_hj32_h_33_route_product)) * pa_c_hj32_h_33_route) + (pa_p_hj32_h_33_route_product))) /\ ((((exists pa_h_hj32_h_33_route_product_partial. pa_h_hj32_h_33_route_product_partial + S (pa_r_hj32_h_33_route_product) = S ((S (pa_i_hj32_h_33_route_product)) * pa_v_hj32_h_33_route_product)) /\ exists pa_q_hj32_h_33_route_product_partial. pa_u_hj32_h_33_route_product = pa_q_hj32_h_33_route_product_partial * S ((S (pa_i_hj32_h_33_route_product)) * pa_v_hj32_h_33_route_product) + (pa_r_hj32_h_33_route_product))) /\ ((((exists pa_h_hj32_h_33_route_product_successor. pa_h_hj32_h_33_route_product_successor + S (pa_s_hj32_h_33_route_product) = S ((S (S pa_i_hj32_h_33_route_product)) * pa_v_hj32_h_33_route_product)) /\ exists pa_q_hj32_h_33_route_product_successor. pa_u_hj32_h_33_route_product = pa_q_hj32_h_33_route_product_successor * S ((S (S pa_i_hj32_h_33_route_product)) * pa_v_hj32_h_33_route_product) + (pa_s_hj32_h_33_route_product))) /\ pa_s_hj32_h_33_route_product = pa_r_hj32_h_33_route_product * pa_p_hj32_h_33_route_product)))))))
  9. 0009have hh_base : 33 + 1 = 34
  10. 0010norm_num
  11. 0011have hh_exponent : 2 * 33 + 2 = 2 * 34
  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 h33s_p36 : ∃ hj32_local_value_h33s_p36. Pow(36,2 · 34,hj32_local_value_h33s_p36)
    Exact native replay linehave h33s_p36 : exists hj32_local_value_h33s_p36. (exists pa_b_hj32_local_total_h33s_p36 pa_c_hj32_local_total_h33s_p36. ((forall pa_i_hj32_local_total_h33s_p36_repeat. (exists pa_lt_hj32_local_total_h33s_p36_repeat_bound. pa_lt_hj32_local_total_h33s_p36_repeat_bound + S pa_i_hj32_local_total_h33s_p36_repeat = 2 * 34) -> (((exists pa_h_hj32_local_total_h33s_p36_repeat_decoded. pa_h_hj32_local_total_h33s_p36_repeat_decoded + S (36) = S ((S (pa_i_hj32_local_total_h33s_p36_repeat)) * pa_c_hj32_local_total_h33s_p36)) /\ exists pa_q_hj32_local_total_h33s_p36_repeat_decoded. pa_b_hj32_local_total_h33s_p36 = pa_q_hj32_local_total_h33s_p36_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p36_repeat)) * pa_c_hj32_local_total_h33s_p36) + (36)))) /\ (exists pa_u_hj32_local_total_h33s_p36_product pa_v_hj32_local_total_h33s_p36_product. ((((exists pa_h_hj32_local_total_h33s_p36_product_start. pa_h_hj32_local_total_h33s_p36_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p36_product)) /\ exists pa_q_hj32_local_total_h33s_p36_product_start. pa_u_hj32_local_total_h33s_p36_product = pa_q_hj32_local_total_h33s_p36_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p36_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p36_product_terminal. pa_h_hj32_local_total_h33s_p36_product_terminal + S (hj32_local_value_h33s_p36) = S ((S (2 * 34)) * pa_v_hj32_local_total_h33s_p36_product)) /\ exists pa_q_hj32_local_total_h33s_p36_product_terminal. pa_u_hj32_local_total_h33s_p36_product = pa_q_hj32_local_total_h33s_p36_product_terminal * S ((S (2 * 34)) * pa_v_hj32_local_total_h33s_p36_product) + (hj32_local_value_h33s_p36))) /\ forall pa_i_hj32_local_total_h33s_p36_product. (exists pa_lt_hj32_local_total_h33s_p36_product_bound. pa_lt_hj32_local_total_h33s_p36_product_bound + S pa_i_hj32_local_total_h33s_p36_product = 2 * 34) -> exists pa_p_hj32_local_total_h33s_p36_product pa_r_hj32_local_total_h33s_p36_product pa_s_hj32_local_total_h33s_p36_product. ((((exists pa_h_hj32_local_total_h33s_p36_product_factor. pa_h_hj32_local_total_h33s_p36_product_factor + S (pa_p_hj32_local_total_h33s_p36_product) = S ((S (pa_i_hj32_local_total_h33s_p36_product)) * pa_c_hj32_local_total_h33s_p36)) /\ exists pa_q_hj32_local_total_h33s_p36_product_factor. pa_b_hj32_local_total_h33s_p36 = pa_q_hj32_local_total_h33s_p36_product_factor * S ((S (pa_i_hj32_local_total_h33s_p36_product)) * pa_c_hj32_local_total_h33s_p36) + (pa_p_hj32_local_total_h33s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p36_product_partial. pa_h_hj32_local_total_h33s_p36_product_partial + S (pa_r_hj32_local_total_h33s_p36_product) = S ((S (pa_i_hj32_local_total_h33s_p36_product)) * pa_v_hj32_local_total_h33s_p36_product)) /\ exists pa_q_hj32_local_total_h33s_p36_product_partial. pa_u_hj32_local_total_h33s_p36_product = pa_q_hj32_local_total_h33s_p36_product_partial * S ((S (pa_i_hj32_local_total_h33s_p36_product)) * pa_v_hj32_local_total_h33s_p36_product) + (pa_r_hj32_local_total_h33s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p36_product_successor. pa_h_hj32_local_total_h33s_p36_product_successor + S (pa_s_hj32_local_total_h33s_p36_product) = S ((S (S pa_i_hj32_local_total_h33s_p36_product)) * pa_v_hj32_local_total_h33s_p36_product)) /\ exists pa_q_hj32_local_total_h33s_p36_product_successor. pa_u_hj32_local_total_h33s_p36_product = pa_q_hj32_local_total_h33s_p36_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p36_product)) * pa_v_hj32_local_total_h33s_p36_product) + (pa_s_hj32_local_total_h33s_p36_product))) /\ pa_s_hj32_local_total_h33s_p36_product = pa_r_hj32_local_total_h33s_p36_product * pa_p_hj32_local_total_h33s_p36_product))))))))
  21. 0021specialize htotal 36
  22. 0022specialize htotal 2 * 34
  23. 0023exact htotal
  24. 0024cases h33s_p36
  25. 0025have h33s_base : Lt(33,36)
    Exact native replay linehave h33s_base : exists bqb_le_gap_hj32_h33s_base. bqb_le_gap_hj32_h33s_base + (34) = (36)
  26. 0026exists 2
  27. 0027norm_num
  28. 0028have h33s_to_36 : Le(h,x)
    Exact native replay linehave h33s_to_36 : exists bqb_le_gap_hj32_local_base_bound_h33s_to_36. bqb_le_gap_hj32_local_base_bound_h33s_to_36 + (h) = (x)
  29. 0029specialize pow_base_monotone 34
  30. 0030specialize pow_base_monotone 36
  31. 0031specialize pow_base_monotone 2 * 34
  32. 0032specialize pow_base_monotone h
  33. 0033specialize pow_base_monotone x
  34. 0034apply pow_base_monotone
  35. 0035exact h33s_base
  36. 0036exact hh_route
  37. 0037exact h33s_p36_witness
  38. 0038have h33s_p6_total : ∃ hj32_local_value_h33s_p6_total. Pow(6,4 · 34,hj32_local_value_h33s_p6_total)
    Exact native replay linehave h33s_p6_total : exists hj32_local_value_h33s_p6_total. (exists pa_b_hj32_local_total_h33s_p6_total pa_c_hj32_local_total_h33s_p6_total. ((forall pa_i_hj32_local_total_h33s_p6_total_repeat. (exists pa_lt_hj32_local_total_h33s_p6_total_repeat_bound. pa_lt_hj32_local_total_h33s_p6_total_repeat_bound + S pa_i_hj32_local_total_h33s_p6_total_repeat = 4 * 34) -> (((exists pa_h_hj32_local_total_h33s_p6_total_repeat_decoded. pa_h_hj32_local_total_h33s_p6_total_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h33s_p6_total_repeat)) * pa_c_hj32_local_total_h33s_p6_total)) /\ exists pa_q_hj32_local_total_h33s_p6_total_repeat_decoded. pa_b_hj32_local_total_h33s_p6_total = pa_q_hj32_local_total_h33s_p6_total_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p6_total_repeat)) * pa_c_hj32_local_total_h33s_p6_total) + (6)))) /\ (exists pa_u_hj32_local_total_h33s_p6_total_product pa_v_hj32_local_total_h33s_p6_total_product. ((((exists pa_h_hj32_local_total_h33s_p6_total_product_start. pa_h_hj32_local_total_h33s_p6_total_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p6_total_product)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_start. pa_u_hj32_local_total_h33s_p6_total_product = pa_q_hj32_local_total_h33s_p6_total_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p6_total_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_total_product_terminal. pa_h_hj32_local_total_h33s_p6_total_product_terminal + S (hj32_local_value_h33s_p6_total) = S ((S (4 * 34)) * pa_v_hj32_local_total_h33s_p6_total_product)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_terminal. pa_u_hj32_local_total_h33s_p6_total_product = pa_q_hj32_local_total_h33s_p6_total_product_terminal * S ((S (4 * 34)) * pa_v_hj32_local_total_h33s_p6_total_product) + (hj32_local_value_h33s_p6_total))) /\ forall pa_i_hj32_local_total_h33s_p6_total_product. (exists pa_lt_hj32_local_total_h33s_p6_total_product_bound. pa_lt_hj32_local_total_h33s_p6_total_product_bound + S pa_i_hj32_local_total_h33s_p6_total_product = 4 * 34) -> exists pa_p_hj32_local_total_h33s_p6_total_product pa_r_hj32_local_total_h33s_p6_total_product pa_s_hj32_local_total_h33s_p6_total_product. ((((exists pa_h_hj32_local_total_h33s_p6_total_product_factor. pa_h_hj32_local_total_h33s_p6_total_product_factor + S (pa_p_hj32_local_total_h33s_p6_total_product) = S ((S (pa_i_hj32_local_total_h33s_p6_total_product)) * pa_c_hj32_local_total_h33s_p6_total)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_factor. pa_b_hj32_local_total_h33s_p6_total = pa_q_hj32_local_total_h33s_p6_total_product_factor * S ((S (pa_i_hj32_local_total_h33s_p6_total_product)) * pa_c_hj32_local_total_h33s_p6_total) + (pa_p_hj32_local_total_h33s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_total_product_partial. pa_h_hj32_local_total_h33s_p6_total_product_partial + S (pa_r_hj32_local_total_h33s_p6_total_product) = S ((S (pa_i_hj32_local_total_h33s_p6_total_product)) * pa_v_hj32_local_total_h33s_p6_total_product)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_partial. pa_u_hj32_local_total_h33s_p6_total_product = pa_q_hj32_local_total_h33s_p6_total_product_partial * S ((S (pa_i_hj32_local_total_h33s_p6_total_product)) * pa_v_hj32_local_total_h33s_p6_total_product) + (pa_r_hj32_local_total_h33s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_total_product_successor. pa_h_hj32_local_total_h33s_p6_total_product_successor + S (pa_s_hj32_local_total_h33s_p6_total_product) = S ((S (S pa_i_hj32_local_total_h33s_p6_total_product)) * pa_v_hj32_local_total_h33s_p6_total_product)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_successor. pa_u_hj32_local_total_h33s_p6_total_product = pa_q_hj32_local_total_h33s_p6_total_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p6_total_product)) * pa_v_hj32_local_total_h33s_p6_total_product) + (pa_s_hj32_local_total_h33s_p6_total_product))) /\ pa_s_hj32_local_total_h33s_p6_total_product = pa_r_hj32_local_total_h33s_p6_total_product * pa_p_hj32_local_total_h33s_p6_total_product))))))))
  39. 0039specialize htotal 6
  40. 0040specialize htotal 4 * 34
  41. 0041exact htotal
  42. 0042cases h33s_p6_total
  43. 0043have h33s_conversion : x = x1
  44. 0044specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total 34
  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 h33s_p36_witness
  50. 0050exact h33s_p6_total_witness
  51. 0051rewrite h33s_conversion at h33s_to_36
  52. 0052have h33s_p6_main : ∃ hj32_local_value_h33s_p6_main. Pow(6,10 · 13,hj32_local_value_h33s_p6_main)
    Exact native replay linehave h33s_p6_main : exists hj32_local_value_h33s_p6_main. (exists pa_b_hj32_local_total_h33s_p6_main pa_c_hj32_local_total_h33s_p6_main. ((forall pa_i_hj32_local_total_h33s_p6_main_repeat. (exists pa_lt_hj32_local_total_h33s_p6_main_repeat_bound. pa_lt_hj32_local_total_h33s_p6_main_repeat_bound + S pa_i_hj32_local_total_h33s_p6_main_repeat = 10 * 13) -> (((exists pa_h_hj32_local_total_h33s_p6_main_repeat_decoded. pa_h_hj32_local_total_h33s_p6_main_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h33s_p6_main_repeat)) * pa_c_hj32_local_total_h33s_p6_main)) /\ exists pa_q_hj32_local_total_h33s_p6_main_repeat_decoded. pa_b_hj32_local_total_h33s_p6_main = pa_q_hj32_local_total_h33s_p6_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p6_main_repeat)) * pa_c_hj32_local_total_h33s_p6_main) + (6)))) /\ (exists pa_u_hj32_local_total_h33s_p6_main_product pa_v_hj32_local_total_h33s_p6_main_product. ((((exists pa_h_hj32_local_total_h33s_p6_main_product_start. pa_h_hj32_local_total_h33s_p6_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p6_main_product)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_start. pa_u_hj32_local_total_h33s_p6_main_product = pa_q_hj32_local_total_h33s_p6_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p6_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_main_product_terminal. pa_h_hj32_local_total_h33s_p6_main_product_terminal + S (hj32_local_value_h33s_p6_main) = S ((S (10 * 13)) * pa_v_hj32_local_total_h33s_p6_main_product)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_terminal. pa_u_hj32_local_total_h33s_p6_main_product = pa_q_hj32_local_total_h33s_p6_main_product_terminal * S ((S (10 * 13)) * pa_v_hj32_local_total_h33s_p6_main_product) + (hj32_local_value_h33s_p6_main))) /\ forall pa_i_hj32_local_total_h33s_p6_main_product. (exists pa_lt_hj32_local_total_h33s_p6_main_product_bound. pa_lt_hj32_local_total_h33s_p6_main_product_bound + S pa_i_hj32_local_total_h33s_p6_main_product = 10 * 13) -> exists pa_p_hj32_local_total_h33s_p6_main_product pa_r_hj32_local_total_h33s_p6_main_product pa_s_hj32_local_total_h33s_p6_main_product. ((((exists pa_h_hj32_local_total_h33s_p6_main_product_factor. pa_h_hj32_local_total_h33s_p6_main_product_factor + S (pa_p_hj32_local_total_h33s_p6_main_product) = S ((S (pa_i_hj32_local_total_h33s_p6_main_product)) * pa_c_hj32_local_total_h33s_p6_main)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_factor. pa_b_hj32_local_total_h33s_p6_main = pa_q_hj32_local_total_h33s_p6_main_product_factor * S ((S (pa_i_hj32_local_total_h33s_p6_main_product)) * pa_c_hj32_local_total_h33s_p6_main) + (pa_p_hj32_local_total_h33s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_main_product_partial. pa_h_hj32_local_total_h33s_p6_main_product_partial + S (pa_r_hj32_local_total_h33s_p6_main_product) = S ((S (pa_i_hj32_local_total_h33s_p6_main_product)) * pa_v_hj32_local_total_h33s_p6_main_product)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_partial. pa_u_hj32_local_total_h33s_p6_main_product = pa_q_hj32_local_total_h33s_p6_main_product_partial * S ((S (pa_i_hj32_local_total_h33s_p6_main_product)) * pa_v_hj32_local_total_h33s_p6_main_product) + (pa_r_hj32_local_total_h33s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_main_product_successor. pa_h_hj32_local_total_h33s_p6_main_product_successor + S (pa_s_hj32_local_total_h33s_p6_main_product) = S ((S (S pa_i_hj32_local_total_h33s_p6_main_product)) * pa_v_hj32_local_total_h33s_p6_main_product)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_successor. pa_u_hj32_local_total_h33s_p6_main_product = pa_q_hj32_local_total_h33s_p6_main_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p6_main_product)) * pa_v_hj32_local_total_h33s_p6_main_product) + (pa_s_hj32_local_total_h33s_p6_main_product))) /\ pa_s_hj32_local_total_h33s_p6_main_product = pa_r_hj32_local_total_h33s_p6_main_product * pa_p_hj32_local_total_h33s_p6_main_product))))))))
  53. 0053specialize htotal 6
  54. 0054specialize htotal 10 * 13
  55. 0055exact htotal
  56. 0056cases h33s_p6_main
  57. 0057have h33s_p4_main : ∃ hj32_local_value_h33s_p4_main. Pow(4,13 · 13,hj32_local_value_h33s_p4_main)
    Exact native replay linehave h33s_p4_main : exists hj32_local_value_h33s_p4_main. (exists pa_b_hj32_local_total_h33s_p4_main pa_c_hj32_local_total_h33s_p4_main. ((forall pa_i_hj32_local_total_h33s_p4_main_repeat. (exists pa_lt_hj32_local_total_h33s_p4_main_repeat_bound. pa_lt_hj32_local_total_h33s_p4_main_repeat_bound + S pa_i_hj32_local_total_h33s_p4_main_repeat = 13 * 13) -> (((exists pa_h_hj32_local_total_h33s_p4_main_repeat_decoded. pa_h_hj32_local_total_h33s_p4_main_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h33s_p4_main_repeat)) * pa_c_hj32_local_total_h33s_p4_main)) /\ exists pa_q_hj32_local_total_h33s_p4_main_repeat_decoded. pa_b_hj32_local_total_h33s_p4_main = pa_q_hj32_local_total_h33s_p4_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p4_main_repeat)) * pa_c_hj32_local_total_h33s_p4_main) + (4)))) /\ (exists pa_u_hj32_local_total_h33s_p4_main_product pa_v_hj32_local_total_h33s_p4_main_product. ((((exists pa_h_hj32_local_total_h33s_p4_main_product_start. pa_h_hj32_local_total_h33s_p4_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p4_main_product)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_start. pa_u_hj32_local_total_h33s_p4_main_product = pa_q_hj32_local_total_h33s_p4_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p4_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_main_product_terminal. pa_h_hj32_local_total_h33s_p4_main_product_terminal + S (hj32_local_value_h33s_p4_main) = S ((S (13 * 13)) * pa_v_hj32_local_total_h33s_p4_main_product)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_terminal. pa_u_hj32_local_total_h33s_p4_main_product = pa_q_hj32_local_total_h33s_p4_main_product_terminal * S ((S (13 * 13)) * pa_v_hj32_local_total_h33s_p4_main_product) + (hj32_local_value_h33s_p4_main))) /\ forall pa_i_hj32_local_total_h33s_p4_main_product. (exists pa_lt_hj32_local_total_h33s_p4_main_product_bound. pa_lt_hj32_local_total_h33s_p4_main_product_bound + S pa_i_hj32_local_total_h33s_p4_main_product = 13 * 13) -> exists pa_p_hj32_local_total_h33s_p4_main_product pa_r_hj32_local_total_h33s_p4_main_product pa_s_hj32_local_total_h33s_p4_main_product. ((((exists pa_h_hj32_local_total_h33s_p4_main_product_factor. pa_h_hj32_local_total_h33s_p4_main_product_factor + S (pa_p_hj32_local_total_h33s_p4_main_product) = S ((S (pa_i_hj32_local_total_h33s_p4_main_product)) * pa_c_hj32_local_total_h33s_p4_main)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_factor. pa_b_hj32_local_total_h33s_p4_main = pa_q_hj32_local_total_h33s_p4_main_product_factor * S ((S (pa_i_hj32_local_total_h33s_p4_main_product)) * pa_c_hj32_local_total_h33s_p4_main) + (pa_p_hj32_local_total_h33s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_main_product_partial. pa_h_hj32_local_total_h33s_p4_main_product_partial + S (pa_r_hj32_local_total_h33s_p4_main_product) = S ((S (pa_i_hj32_local_total_h33s_p4_main_product)) * pa_v_hj32_local_total_h33s_p4_main_product)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_partial. pa_u_hj32_local_total_h33s_p4_main_product = pa_q_hj32_local_total_h33s_p4_main_product_partial * S ((S (pa_i_hj32_local_total_h33s_p4_main_product)) * pa_v_hj32_local_total_h33s_p4_main_product) + (pa_r_hj32_local_total_h33s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_main_product_successor. pa_h_hj32_local_total_h33s_p4_main_product_successor + S (pa_s_hj32_local_total_h33s_p4_main_product) = S ((S (S pa_i_hj32_local_total_h33s_p4_main_product)) * pa_v_hj32_local_total_h33s_p4_main_product)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_successor. pa_u_hj32_local_total_h33s_p4_main_product = pa_q_hj32_local_total_h33s_p4_main_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p4_main_product)) * pa_v_hj32_local_total_h33s_p4_main_product) + (pa_s_hj32_local_total_h33s_p4_main_product))) /\ pa_s_hj32_local_total_h33s_p4_main_product = pa_r_hj32_local_total_h33s_p4_main_product * pa_p_hj32_local_total_h33s_p4_main_product))))))))
  58. 0058specialize htotal 4
  59. 0059specialize htotal 13 * 13
  60. 0060exact htotal
  61. 0061cases h33s_p4_main
  62. 0062have h33s_main_bound : Le(x2,x3)
    Exact native replay linehave h33s_main_bound : exists bqb_le_gap_hj32_h33s_main_bound. bqb_le_gap_hj32_h33s_main_bound + (x2) = (x3)
  63. 0063specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 13
  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 h33s_p6_main_witness
  69. 0069exact h33s_p4_main_witness
  70. 0070have h33s_p6_residual : ∃ hj32_local_value_h33s_p6_residual. Pow(6,6,hj32_local_value_h33s_p6_residual)
    Exact native replay linehave h33s_p6_residual : exists hj32_local_value_h33s_p6_residual. (exists pa_b_hj32_local_total_h33s_p6_residual pa_c_hj32_local_total_h33s_p6_residual. ((forall pa_i_hj32_local_total_h33s_p6_residual_repeat. (exists pa_lt_hj32_local_total_h33s_p6_residual_repeat_bound. pa_lt_hj32_local_total_h33s_p6_residual_repeat_bound + S pa_i_hj32_local_total_h33s_p6_residual_repeat = 6) -> (((exists pa_h_hj32_local_total_h33s_p6_residual_repeat_decoded. pa_h_hj32_local_total_h33s_p6_residual_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h33s_p6_residual_repeat)) * pa_c_hj32_local_total_h33s_p6_residual)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_repeat_decoded. pa_b_hj32_local_total_h33s_p6_residual = pa_q_hj32_local_total_h33s_p6_residual_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p6_residual_repeat)) * pa_c_hj32_local_total_h33s_p6_residual) + (6)))) /\ (exists pa_u_hj32_local_total_h33s_p6_residual_product pa_v_hj32_local_total_h33s_p6_residual_product. ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_start. pa_h_hj32_local_total_h33s_p6_residual_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_start. pa_u_hj32_local_total_h33s_p6_residual_product = pa_q_hj32_local_total_h33s_p6_residual_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p6_residual_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_terminal. pa_h_hj32_local_total_h33s_p6_residual_product_terminal + S (hj32_local_value_h33s_p6_residual) = S ((S (6)) * pa_v_hj32_local_total_h33s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_terminal. pa_u_hj32_local_total_h33s_p6_residual_product = pa_q_hj32_local_total_h33s_p6_residual_product_terminal * S ((S (6)) * pa_v_hj32_local_total_h33s_p6_residual_product) + (hj32_local_value_h33s_p6_residual))) /\ forall pa_i_hj32_local_total_h33s_p6_residual_product. (exists pa_lt_hj32_local_total_h33s_p6_residual_product_bound. pa_lt_hj32_local_total_h33s_p6_residual_product_bound + S pa_i_hj32_local_total_h33s_p6_residual_product = 6) -> exists pa_p_hj32_local_total_h33s_p6_residual_product pa_r_hj32_local_total_h33s_p6_residual_product pa_s_hj32_local_total_h33s_p6_residual_product. ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_factor. pa_h_hj32_local_total_h33s_p6_residual_product_factor + S (pa_p_hj32_local_total_h33s_p6_residual_product) = S ((S (pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_c_hj32_local_total_h33s_p6_residual)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_factor. pa_b_hj32_local_total_h33s_p6_residual = pa_q_hj32_local_total_h33s_p6_residual_product_factor * S ((S (pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_c_hj32_local_total_h33s_p6_residual) + (pa_p_hj32_local_total_h33s_p6_residual_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_partial. pa_h_hj32_local_total_h33s_p6_residual_product_partial + S (pa_r_hj32_local_total_h33s_p6_residual_product) = S ((S (pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_v_hj32_local_total_h33s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_partial. pa_u_hj32_local_total_h33s_p6_residual_product = pa_q_hj32_local_total_h33s_p6_residual_product_partial * S ((S (pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_v_hj32_local_total_h33s_p6_residual_product) + (pa_r_hj32_local_total_h33s_p6_residual_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_successor. pa_h_hj32_local_total_h33s_p6_residual_product_successor + S (pa_s_hj32_local_total_h33s_p6_residual_product) = S ((S (S pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_v_hj32_local_total_h33s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_successor. pa_u_hj32_local_total_h33s_p6_residual_product = pa_q_hj32_local_total_h33s_p6_residual_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_v_hj32_local_total_h33s_p6_residual_product) + (pa_s_hj32_local_total_h33s_p6_residual_product))) /\ pa_s_hj32_local_total_h33s_p6_residual_product = pa_r_hj32_local_total_h33s_p6_residual_product * pa_p_hj32_local_total_h33s_p6_residual_product))))))))
  71. 0071specialize htotal 6
  72. 0072specialize htotal 6
  73. 0073exact htotal
  74. 0074cases h33s_p6_residual
  75. 0075have h33s_p4_residual : ∃ hj32_local_value_h33s_p4_residual. Pow(4,8,hj32_local_value_h33s_p4_residual)
    Exact native replay linehave h33s_p4_residual : exists hj32_local_value_h33s_p4_residual. (exists pa_b_hj32_local_total_h33s_p4_residual pa_c_hj32_local_total_h33s_p4_residual. ((forall pa_i_hj32_local_total_h33s_p4_residual_repeat. (exists pa_lt_hj32_local_total_h33s_p4_residual_repeat_bound. pa_lt_hj32_local_total_h33s_p4_residual_repeat_bound + S pa_i_hj32_local_total_h33s_p4_residual_repeat = 8) -> (((exists pa_h_hj32_local_total_h33s_p4_residual_repeat_decoded. pa_h_hj32_local_total_h33s_p4_residual_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h33s_p4_residual_repeat)) * pa_c_hj32_local_total_h33s_p4_residual)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_repeat_decoded. pa_b_hj32_local_total_h33s_p4_residual = pa_q_hj32_local_total_h33s_p4_residual_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p4_residual_repeat)) * pa_c_hj32_local_total_h33s_p4_residual) + (4)))) /\ (exists pa_u_hj32_local_total_h33s_p4_residual_product pa_v_hj32_local_total_h33s_p4_residual_product. ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_start. pa_h_hj32_local_total_h33s_p4_residual_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_start. pa_u_hj32_local_total_h33s_p4_residual_product = pa_q_hj32_local_total_h33s_p4_residual_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p4_residual_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_terminal. pa_h_hj32_local_total_h33s_p4_residual_product_terminal + S (hj32_local_value_h33s_p4_residual) = S ((S (8)) * pa_v_hj32_local_total_h33s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_terminal. pa_u_hj32_local_total_h33s_p4_residual_product = pa_q_hj32_local_total_h33s_p4_residual_product_terminal * S ((S (8)) * pa_v_hj32_local_total_h33s_p4_residual_product) + (hj32_local_value_h33s_p4_residual))) /\ forall pa_i_hj32_local_total_h33s_p4_residual_product. (exists pa_lt_hj32_local_total_h33s_p4_residual_product_bound. pa_lt_hj32_local_total_h33s_p4_residual_product_bound + S pa_i_hj32_local_total_h33s_p4_residual_product = 8) -> exists pa_p_hj32_local_total_h33s_p4_residual_product pa_r_hj32_local_total_h33s_p4_residual_product pa_s_hj32_local_total_h33s_p4_residual_product. ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_factor. pa_h_hj32_local_total_h33s_p4_residual_product_factor + S (pa_p_hj32_local_total_h33s_p4_residual_product) = S ((S (pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_c_hj32_local_total_h33s_p4_residual)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_factor. pa_b_hj32_local_total_h33s_p4_residual = pa_q_hj32_local_total_h33s_p4_residual_product_factor * S ((S (pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_c_hj32_local_total_h33s_p4_residual) + (pa_p_hj32_local_total_h33s_p4_residual_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_partial. pa_h_hj32_local_total_h33s_p4_residual_product_partial + S (pa_r_hj32_local_total_h33s_p4_residual_product) = S ((S (pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_v_hj32_local_total_h33s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_partial. pa_u_hj32_local_total_h33s_p4_residual_product = pa_q_hj32_local_total_h33s_p4_residual_product_partial * S ((S (pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_v_hj32_local_total_h33s_p4_residual_product) + (pa_r_hj32_local_total_h33s_p4_residual_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_successor. pa_h_hj32_local_total_h33s_p4_residual_product_successor + S (pa_s_hj32_local_total_h33s_p4_residual_product) = S ((S (S pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_v_hj32_local_total_h33s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_successor. pa_u_hj32_local_total_h33s_p4_residual_product = pa_q_hj32_local_total_h33s_p4_residual_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_v_hj32_local_total_h33s_p4_residual_product) + (pa_s_hj32_local_total_h33s_p4_residual_product))) /\ pa_s_hj32_local_total_h33s_p4_residual_product = pa_r_hj32_local_total_h33s_p4_residual_product * pa_p_hj32_local_total_h33s_p4_residual_product))))))))
  76. 0076specialize htotal 4
  77. 0077specialize htotal 8
  78. 0078exact htotal
  79. 0079cases h33s_p4_residual
  80. 0080have h33s_residual_bound : Le(x4,x5)
    Exact native replay linehave h33s_residual_bound : exists bqb_le_gap_hj32_h33s_residual_bound. bqb_le_gap_hj32_h33s_residual_bound + (x4) = (x5)
  81. 0081specialize pow_six_six_le_pow_four_eight_from_total x4
  82. 0082specialize pow_six_six_le_pow_four_eight_from_total x5
  83. 0083apply pow_six_six_le_pow_four_eight_from_total
  84. 0084exact htotal
  85. 0085exact h33s_p6_residual_witness
  86. 0086exact h33s_p4_residual_witness
  87. 0087have h33s_exponent : 4 * 34 = 10 * 13 + 6
  88. 0088have h33s_thirty_four : 34 = 13 + 21
  89. 0089norm_num
  90. 0090rewrite h33s_thirty_four
  91. 0091have h33s_distrib_one : 4 * (13 + 21) = 4 * 13 + 4 * 21
  92. 0092specialize mul_add 4
  93. 0093specialize mul_add 13
  94. 0094specialize mul_add 21
  95. 0095apply mul_add
  96. 0096rewrite h33s_distrib_one
  97. 0097have h33s_bridge : 4 * 21 = 6 * 14
  98. 0098norm_num
  99. 0099rewrite h33s_bridge
  100. 0100have h33s_fourteen : 14 = 13 + 1
  101. 0101norm_num
  102. 0102rewrite h33s_fourteen
  103. 0103have h33s_distrib_two : 6 * (13 + 1) = 6 * 13 + 6 * 1
  104. 0104specialize mul_add 6
  105. 0105specialize mul_add 13
  106. 0106specialize mul_add 1
  107. 0107apply mul_add
  108. 0108rewrite h33s_distrib_two
  109. 0109have h33s_six : 6 * 1 = 6
  110. 0110norm_num
  111. 0111rewrite h33s_six
  112. 0112have h33s_assoc : 4 * 13 + (6 * 13 + 6) = (4 * 13 + 6 * 13) + 6
  113. 0113symm
  114. 0114specialize add_assoc (4 * 13)
  115. 0115specialize add_assoc (6 * 13)
  116. 0116specialize add_assoc 6
  117. 0117apply add_assoc
  118. 0118rewrite h33s_assoc
  119. 0119have h33s_factor : (4 + 6) * 13 = 4 * 13 + 6 * 13
  120. 0120specialize add_mul 4
  121. 0121specialize add_mul 6
  122. 0122specialize add_mul 13
  123. 0123apply add_mul
  124. 0124rewrite <- h33s_factor
  125. 0125have h33s_ten : 4 + 6 = 10
  126. 0126norm_num
  127. 0127rewrite h33s_ten
  128. 0128refl
  129. 0129have h33s_left_product : x1 = x2 * x4
  130. 0130specialize pow_add 6
  131. 0131specialize pow_add 10 * 13
  132. 0132specialize pow_add 6
  133. 0133specialize pow_add 4 * 34
  134. 0134specialize pow_add x2
  135. 0135specialize pow_add x4
  136. 0136specialize pow_add x1
  137. 0137apply pow_add
  138. 0138exact h33s_exponent
  139. 0139exact h33s_p6_main_witness
  140. 0140exact h33s_p6_residual_witness
  141. 0141exact h33s_p6_total_witness
  142. 0142have h33s_p4_budget : ∃ hj32_local_value_h33s_p4_budget. Pow(4,13 · 13 + 8,hj32_local_value_h33s_p4_budget)
    Exact native replay linehave h33s_p4_budget : exists hj32_local_value_h33s_p4_budget. (exists pa_b_hj32_local_total_h33s_p4_budget pa_c_hj32_local_total_h33s_p4_budget. ((forall pa_i_hj32_local_total_h33s_p4_budget_repeat. (exists pa_lt_hj32_local_total_h33s_p4_budget_repeat_bound. pa_lt_hj32_local_total_h33s_p4_budget_repeat_bound + S pa_i_hj32_local_total_h33s_p4_budget_repeat = 13 * 13 + 8) -> (((exists pa_h_hj32_local_total_h33s_p4_budget_repeat_decoded. pa_h_hj32_local_total_h33s_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h33s_p4_budget_repeat)) * pa_c_hj32_local_total_h33s_p4_budget)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_repeat_decoded. pa_b_hj32_local_total_h33s_p4_budget = pa_q_hj32_local_total_h33s_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p4_budget_repeat)) * pa_c_hj32_local_total_h33s_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h33s_p4_budget_product pa_v_hj32_local_total_h33s_p4_budget_product. ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_start. pa_h_hj32_local_total_h33s_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_start. pa_u_hj32_local_total_h33s_p4_budget_product = pa_q_hj32_local_total_h33s_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_terminal. pa_h_hj32_local_total_h33s_p4_budget_product_terminal + S (hj32_local_value_h33s_p4_budget) = S ((S (13 * 13 + 8)) * pa_v_hj32_local_total_h33s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_terminal. pa_u_hj32_local_total_h33s_p4_budget_product = pa_q_hj32_local_total_h33s_p4_budget_product_terminal * S ((S (13 * 13 + 8)) * pa_v_hj32_local_total_h33s_p4_budget_product) + (hj32_local_value_h33s_p4_budget))) /\ forall pa_i_hj32_local_total_h33s_p4_budget_product. (exists pa_lt_hj32_local_total_h33s_p4_budget_product_bound. pa_lt_hj32_local_total_h33s_p4_budget_product_bound + S pa_i_hj32_local_total_h33s_p4_budget_product = 13 * 13 + 8) -> exists pa_p_hj32_local_total_h33s_p4_budget_product pa_r_hj32_local_total_h33s_p4_budget_product pa_s_hj32_local_total_h33s_p4_budget_product. ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_factor. pa_h_hj32_local_total_h33s_p4_budget_product_factor + S (pa_p_hj32_local_total_h33s_p4_budget_product) = S ((S (pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_c_hj32_local_total_h33s_p4_budget)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_factor. pa_b_hj32_local_total_h33s_p4_budget = pa_q_hj32_local_total_h33s_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_c_hj32_local_total_h33s_p4_budget) + (pa_p_hj32_local_total_h33s_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_partial. pa_h_hj32_local_total_h33s_p4_budget_product_partial + S (pa_r_hj32_local_total_h33s_p4_budget_product) = S ((S (pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_v_hj32_local_total_h33s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_partial. pa_u_hj32_local_total_h33s_p4_budget_product = pa_q_hj32_local_total_h33s_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_v_hj32_local_total_h33s_p4_budget_product) + (pa_r_hj32_local_total_h33s_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_successor. pa_h_hj32_local_total_h33s_p4_budget_product_successor + S (pa_s_hj32_local_total_h33s_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_v_hj32_local_total_h33s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_successor. pa_u_hj32_local_total_h33s_p4_budget_product = pa_q_hj32_local_total_h33s_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_v_hj32_local_total_h33s_p4_budget_product) + (pa_s_hj32_local_total_h33s_p4_budget_product))) /\ pa_s_hj32_local_total_h33s_p4_budget_product = pa_r_hj32_local_total_h33s_p4_budget_product * pa_p_hj32_local_total_h33s_p4_budget_product))))))))
  143. 0143specialize htotal 4
  144. 0144specialize htotal 13 * 13 + 8
  145. 0145exact htotal
  146. 0146cases h33s_p4_budget
  147. 0147have h33s_right_product : x6 = x3 * x5
  148. 0148specialize pow_add 4
  149. 0149specialize pow_add 13 * 13
  150. 0150specialize pow_add 8
  151. 0151specialize pow_add 13 * 13 + 8
  152. 0152specialize pow_add x3
  153. 0153specialize pow_add x5
  154. 0154specialize pow_add x6
  155. 0155apply pow_add
  156. 0156refl
  157. 0157exact h33s_p4_main_witness
  158. 0158exact h33s_p4_residual_witness
  159. 0159exact h33s_p4_budget_witness
  160. 0160have h33s_six_bound : Le(x2 · x4,x3 · x5)
    Exact native replay linehave h33s_six_bound : exists bqb_le_gap_hj32_local_product_bound_h33s_six_bound. bqb_le_gap_hj32_local_product_bound_h33s_six_bound + (x2 * x4) = (x3 * x5)
  161. 0161specialize mul_le_mul x2
  162. 0162specialize mul_le_mul x3
  163. 0163specialize mul_le_mul x4
  164. 0164specialize mul_le_mul x5
  165. 0165apply mul_le_mul
  166. 0166exact h33s_main_bound
  167. 0167exact h33s_residual_bound
  168. 0168rewrite <- h33s_left_product at h33s_six_bound
  169. 0169rewrite <- h33s_right_product at h33s_six_bound
  170. 0170have h33s_to_budget : Le(h,x6)
    Exact native replay linehave h33s_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h33s_to_budget. bqb_le_gap_hj32_local_trans_bound_h33s_to_budget + (h) = (x6)
  171. 0171specialize le_trans h
  172. 0172specialize le_trans x1
  173. 0173specialize le_trans x6
  174. 0174apply le_trans
  175. 0175exact h33s_to_36
  176. 0176exact h33s_six_bound
  177. 0177have hscaled : Le(6 · (13 · 13 + 8),33 · 33)
    Exact native replay linehave hscaled : exists bqb_le_gap_hj32_scaled_budget_root_33. bqb_le_gap_hj32_scaled_budget_root_33 + (6 * (13 * 13 + 8)) = (33 * 33)
  178. 0178apply bertrand_scaled_budget_root_33
  179. 0179have hbudget_exponent : Le(13 · 13 + 8,e)
    Exact native replay linehave hbudget_exponent : exists bqb_le_gap_hj32_h_33_budget_exponent. bqb_le_gap_hj32_h_33_budget_exponent + (13 * 13 + 8) = (e)
  180. 0180specialize ceil_div_six_budget_of_scaled_le (33 * 33)
  181. 0181specialize ceil_div_six_budget_of_scaled_le (13 * 13 + 8)
  182. 0182specialize ceil_div_six_budget_of_scaled_le e
  183. 0183apply ceil_div_six_budget_of_scaled_le
  184. 0184exact hceiling
  185. 0185exact hscaled
  186. 0186have h33_budget_growth : Le(x6,u)
    Exact native replay linehave h33_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h33_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h33_budget_growth + (x6) = (u)
  187. 0187specialize pow_exponent_monotone_from_total 4
  188. 0188specialize pow_exponent_monotone_from_total 13 * 13 + 8
  189. 0189specialize pow_exponent_monotone_from_total e
  190. 0190specialize pow_exponent_monotone_from_total x6
  191. 0191specialize pow_exponent_monotone_from_total u
  192. 0192apply pow_exponent_monotone_from_total
  193. 0193exact htotal
  194. 0194exists 3
  195. 0195norm_num
  196. 0196exact hbudget_exponent
  197. 0197exact h33s_p4_budget_witness
  198. 0198exact hu
  199. 0199have h33_result : Le(h,u)
    Exact native replay linehave h33_result : exists bqb_le_gap_hj32_local_trans_bound_h33_result. bqb_le_gap_hj32_local_trans_bound_h33_result + (h) = (u)
  200. 0200specialize le_trans h
  201. 0201specialize le_trans x6
  202. 0202specialize le_trans u
  203. 0203apply le_trans
  204. 0204exact h33s_to_budget
  205. 0205exact h33_budget_growth
  206. 0206exact h33_result