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(37 · 37,e) → Pow(37 + 1,2 · 37 + 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
5 occurrences
In local proof propositions
17 occurrences
Exact expanded native-PA statement
forall e h u. (forall bpt_a_hj32_h_root_37 bpt_e_hj32_h_root_37. exists bpt_x_hj32_h_root_37. (exists ff_b_bpt_value_hj32_h_root_37 ff_c_bpt_value_hj32_h_root_37. ((forall ff_i_bpt_value_hj32_h_root_37_repeat. (exists ff_lt_bpt_value_hj32_h_root_37_repeat_bound. ff_lt_bpt_value_hj32_h_root_37_repeat_bound + S ff_i_bpt_value_hj32_h_root_37_repeat = bpt_e_hj32_h_root_37) -> (((exists ff_h_bpt_value_hj32_h_root_37_repeat_decoded. ff_h_bpt_value_hj32_h_root_37_repeat_decoded + S (bpt_a_hj32_h_root_37) = S ((S (ff_i_bpt_value_hj32_h_root_37_repeat)) * ff_c_bpt_value_hj32_h_root_37)) /\ exists ff_q_bpt_value_hj32_h_root_37_repeat_decoded. ff_b_bpt_value_hj32_h_root_37 = ff_q_bpt_value_hj32_h_root_37_repeat_decoded * S ((S (ff_i_bpt_value_hj32_h_root_37_repeat)) * ff_c_bpt_value_hj32_h_root_37) + (bpt_a_hj32_h_root_37)))) /\ (exists ff_u_bpt_value_hj32_h_root_37_product ff_v_bpt_value_hj32_h_root_37_product. ((((exists ff_h_bpt_value_hj32_h_root_37_product_start. ff_h_bpt_value_hj32_h_root_37_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_h_root_37_product)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_start. ff_u_bpt_value_hj32_h_root_37_product = ff_q_bpt_value_hj32_h_root_37_product_start * S ((S (0)) * ff_v_bpt_value_hj32_h_root_37_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_h_root_37_product_terminal. ff_h_bpt_value_hj32_h_root_37_product_terminal + S (bpt_x_hj32_h_root_37) = S ((S (bpt_e_hj32_h_root_37)) * ff_v_bpt_value_hj32_h_root_37_product)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_terminal. ff_u_bpt_value_hj32_h_root_37_product = ff_q_bpt_value_hj32_h_root_37_product_terminal * S ((S (bpt_e_hj32_h_root_37)) * ff_v_bpt_value_hj32_h_root_37_product) + (bpt_x_hj32_h_root_37))) /\ forall ff_i_bpt_value_hj32_h_root_37_product. (exists ff_lt_bpt_value_hj32_h_root_37_product_bound. ff_lt_bpt_value_hj32_h_root_37_product_bound + S ff_i_bpt_value_hj32_h_root_37_product = bpt_e_hj32_h_root_37) -> exists ff_p_bpt_value_hj32_h_root_37_product ff_r_bpt_value_hj32_h_root_37_product ff_s_bpt_value_hj32_h_root_37_product. ((((exists ff_h_bpt_value_hj32_h_root_37_product_factor. ff_h_bpt_value_hj32_h_root_37_product_factor + S (ff_p_bpt_value_hj32_h_root_37_product) = S ((S (ff_i_bpt_value_hj32_h_root_37_product)) * ff_c_bpt_value_hj32_h_root_37)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_factor. ff_b_bpt_value_hj32_h_root_37 = ff_q_bpt_value_hj32_h_root_37_product_factor * S ((S (ff_i_bpt_value_hj32_h_root_37_product)) * ff_c_bpt_value_hj32_h_root_37) + (ff_p_bpt_value_hj32_h_root_37_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_37_product_partial. ff_h_bpt_value_hj32_h_root_37_product_partial + S (ff_r_bpt_value_hj32_h_root_37_product) = S ((S (ff_i_bpt_value_hj32_h_root_37_product)) * ff_v_bpt_value_hj32_h_root_37_product)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_partial. ff_u_bpt_value_hj32_h_root_37_product = ff_q_bpt_value_hj32_h_root_37_product_partial * S ((S (ff_i_bpt_value_hj32_h_root_37_product)) * ff_v_bpt_value_hj32_h_root_37_product) + (ff_r_bpt_value_hj32_h_root_37_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_37_product_successor. ff_h_bpt_value_hj32_h_root_37_product_successor + S (ff_s_bpt_value_hj32_h_root_37_product) = S ((S (S ff_i_bpt_value_hj32_h_root_37_product)) * ff_v_bpt_value_hj32_h_root_37_product)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_successor. ff_u_bpt_value_hj32_h_root_37_product = ff_q_bpt_value_hj32_h_root_37_product_successor * S ((S (S ff_i_bpt_value_hj32_h_root_37_product)) * ff_v_bpt_value_hj32_h_root_37_product) + (ff_s_bpt_value_hj32_h_root_37_product))) /\ ff_s_bpt_value_hj32_h_root_37_product = ff_r_bpt_value_hj32_h_root_37_product * ff_p_bpt_value_hj32_h_root_37_product))))))))) -> (((exists bcs_lower_gap_hj32_h_root_37_ceiling. bcs_lower_gap_hj32_h_root_37_ceiling + (37 * 37) = 6 * (e)) /\ exists bcs_upper_gap_hj32_h_root_37_ceiling. bcs_upper_gap_hj32_h_root_37_ceiling + S (6 * (e)) = (37 * 37) + 6)) -> (exists pa_b_hj32_h_root_37_h pa_c_hj32_h_root_37_h. ((forall pa_i_hj32_h_root_37_h_repeat. (exists pa_lt_hj32_h_root_37_h_repeat_bound. pa_lt_hj32_h_root_37_h_repeat_bound + S pa_i_hj32_h_root_37_h_repeat = 2 * 37 + 2) -> (((exists pa_h_hj32_h_root_37_h_repeat_decoded. pa_h_hj32_h_root_37_h_repeat_decoded + S (37 + 1) = S ((S (pa_i_hj32_h_root_37_h_repeat)) * pa_c_hj32_h_root_37_h)) /\ exists pa_q_hj32_h_root_37_h_repeat_decoded. pa_b_hj32_h_root_37_h = pa_q_hj32_h_root_37_h_repeat_decoded * S ((S (pa_i_hj32_h_root_37_h_repeat)) * pa_c_hj32_h_root_37_h) + (37 + 1)))) /\ (exists pa_u_hj32_h_root_37_h_product pa_v_hj32_h_root_37_h_product. ((((exists pa_h_hj32_h_root_37_h_product_start. pa_h_hj32_h_root_37_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_37_h_product)) /\ exists pa_q_hj32_h_root_37_h_product_start. pa_u_hj32_h_root_37_h_product = pa_q_hj32_h_root_37_h_product_start * S ((S (0)) * pa_v_hj32_h_root_37_h_product) + (1))) /\ ((((exists pa_h_hj32_h_root_37_h_product_terminal. pa_h_hj32_h_root_37_h_product_terminal + S (h) = S ((S (2 * 37 + 2)) * pa_v_hj32_h_root_37_h_product)) /\ exists pa_q_hj32_h_root_37_h_product_terminal. pa_u_hj32_h_root_37_h_product = pa_q_hj32_h_root_37_h_product_terminal * S ((S (2 * 37 + 2)) * pa_v_hj32_h_root_37_h_product) + (h))) /\ forall pa_i_hj32_h_root_37_h_product. (exists pa_lt_hj32_h_root_37_h_product_bound. pa_lt_hj32_h_root_37_h_product_bound + S pa_i_hj32_h_root_37_h_product = 2 * 37 + 2) -> exists pa_p_hj32_h_root_37_h_product pa_r_hj32_h_root_37_h_product pa_s_hj32_h_root_37_h_product. ((((exists pa_h_hj32_h_root_37_h_product_factor. pa_h_hj32_h_root_37_h_product_factor + S (pa_p_hj32_h_root_37_h_product) = S ((S (pa_i_hj32_h_root_37_h_product)) * pa_c_hj32_h_root_37_h)) /\ exists pa_q_hj32_h_root_37_h_product_factor. pa_b_hj32_h_root_37_h = pa_q_hj32_h_root_37_h_product_factor * S ((S (pa_i_hj32_h_root_37_h_product)) * pa_c_hj32_h_root_37_h) + (pa_p_hj32_h_root_37_h_product))) /\ ((((exists pa_h_hj32_h_root_37_h_product_partial. pa_h_hj32_h_root_37_h_product_partial + S (pa_r_hj32_h_root_37_h_product) = S ((S (pa_i_hj32_h_root_37_h_product)) * pa_v_hj32_h_root_37_h_product)) /\ exists pa_q_hj32_h_root_37_h_product_partial. pa_u_hj32_h_root_37_h_product = pa_q_hj32_h_root_37_h_product_partial * S ((S (pa_i_hj32_h_root_37_h_product)) * pa_v_hj32_h_root_37_h_product) + (pa_r_hj32_h_root_37_h_product))) /\ ((((exists pa_h_hj32_h_root_37_h_product_successor. pa_h_hj32_h_root_37_h_product_successor + S (pa_s_hj32_h_root_37_h_product) = S ((S (S pa_i_hj32_h_root_37_h_product)) * pa_v_hj32_h_root_37_h_product)) /\ exists pa_q_hj32_h_root_37_h_product_successor. pa_u_hj32_h_root_37_h_product = pa_q_hj32_h_root_37_h_product_successor * S ((S (S pa_i_hj32_h_root_37_h_product)) * pa_v_hj32_h_root_37_h_product) + (pa_s_hj32_h_root_37_h_product))) /\ pa_s_hj32_h_root_37_h_product = pa_r_hj32_h_root_37_h_product * pa_p_hj32_h_root_37_h_product)))))))) -> (exists pa_b_hj32_h_root_37_u pa_c_hj32_h_root_37_u. ((forall pa_i_hj32_h_root_37_u_repeat. (exists pa_lt_hj32_h_root_37_u_repeat_bound. pa_lt_hj32_h_root_37_u_repeat_bound + S pa_i_hj32_h_root_37_u_repeat = e) -> (((exists pa_h_hj32_h_root_37_u_repeat_decoded. pa_h_hj32_h_root_37_u_repeat_decoded + S (4) = S ((S (pa_i_hj32_h_root_37_u_repeat)) * pa_c_hj32_h_root_37_u)) /\ exists pa_q_hj32_h_root_37_u_repeat_decoded. pa_b_hj32_h_root_37_u = pa_q_hj32_h_root_37_u_repeat_decoded * S ((S (pa_i_hj32_h_root_37_u_repeat)) * pa_c_hj32_h_root_37_u) + (4)))) /\ (exists pa_u_hj32_h_root_37_u_product pa_v_hj32_h_root_37_u_product. ((((exists pa_h_hj32_h_root_37_u_product_start. pa_h_hj32_h_root_37_u_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_37_u_product)) /\ exists pa_q_hj32_h_root_37_u_product_start. pa_u_hj32_h_root_37_u_product = pa_q_hj32_h_root_37_u_product_start * S ((S (0)) * pa_v_hj32_h_root_37_u_product) + (1))) /\ ((((exists pa_h_hj32_h_root_37_u_product_terminal. pa_h_hj32_h_root_37_u_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_h_root_37_u_product)) /\ exists pa_q_hj32_h_root_37_u_product_terminal. pa_u_hj32_h_root_37_u_product = pa_q_hj32_h_root_37_u_product_terminal * S ((S (e)) * pa_v_hj32_h_root_37_u_product) + (u))) /\ forall pa_i_hj32_h_root_37_u_product. (exists pa_lt_hj32_h_root_37_u_product_bound. pa_lt_hj32_h_root_37_u_product_bound + S pa_i_hj32_h_root_37_u_product = e) -> exists pa_p_hj32_h_root_37_u_product pa_r_hj32_h_root_37_u_product pa_s_hj32_h_root_37_u_product. ((((exists pa_h_hj32_h_root_37_u_product_factor. pa_h_hj32_h_root_37_u_product_factor + S (pa_p_hj32_h_root_37_u_product) = S ((S (pa_i_hj32_h_root_37_u_product)) * pa_c_hj32_h_root_37_u)) /\ exists pa_q_hj32_h_root_37_u_product_factor. pa_b_hj32_h_root_37_u = pa_q_hj32_h_root_37_u_product_factor * S ((S (pa_i_hj32_h_root_37_u_product)) * pa_c_hj32_h_root_37_u) + (pa_p_hj32_h_root_37_u_product))) /\ ((((exists pa_h_hj32_h_root_37_u_product_partial. pa_h_hj32_h_root_37_u_product_partial + S (pa_r_hj32_h_root_37_u_product) = S ((S (pa_i_hj32_h_root_37_u_product)) * pa_v_hj32_h_root_37_u_product)) /\ exists pa_q_hj32_h_root_37_u_product_partial. pa_u_hj32_h_root_37_u_product = pa_q_hj32_h_root_37_u_product_partial * S ((S (pa_i_hj32_h_root_37_u_product)) * pa_v_hj32_h_root_37_u_product) + (pa_r_hj32_h_root_37_u_product))) /\ ((((exists pa_h_hj32_h_root_37_u_product_successor. pa_h_hj32_h_root_37_u_product_successor + S (pa_s_hj32_h_root_37_u_product) = S ((S (S pa_i_hj32_h_root_37_u_product)) * pa_v_hj32_h_root_37_u_product)) /\ exists pa_q_hj32_h_root_37_u_product_successor. pa_u_hj32_h_root_37_u_product = pa_q_hj32_h_root_37_u_product_successor * S ((S (S pa_i_hj32_h_root_37_u_product)) * pa_v_hj32_h_root_37_u_product) + (pa_s_hj32_h_root_37_u_product))) /\ pa_s_hj32_h_root_37_u_product = pa_r_hj32_h_root_37_u_product * pa_p_hj32_h_root_37_u_product)))))))) -> (exists bqb_le_gap_hj32_h_root_37_result. bqb_le_gap_hj32_h_root_37_result + (h) = (u))Proof neighborhood
Direct theorem prerequisites
BT00WD bertrand_scaled_budget_root_37 BT00WE ceil_div_six_budget_of_scaled_le BT00WL pow_eleven_double_block_le_pow_four_even_from_total BT00QV pow_mul_base BT009X pow_add BT00PY pow_base_monotone BT00SN pow_exponent_monotone_from_total BT00PV mul_le_mul BT000E le_refl BT000F le_trans BT0008 mul_assoc BT0006 mul_commDirect theorem dependents
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
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.
Named ingredients (12)
01Fix variables and assumptionsL1–7
02Establish hh_routeL8–8
Establish this local claim before using it. It is not an additional assumption.
- L8
have hh_route : Pow(38,2 · 38,h)Definitions: Pow(38,2 · 38,h)Original native command in the exact edition
03Establish hh_baseL9–10
04Establish hh_exponentL11–19
05Establish h37t_p44L20–23
Establish this local claim before using it. It is not an additional assumption.
- L20
have h37t_p44 : ∃ hj32_local_value_h37t_p44. Pow(44,2 · 38,hj32_local_value_h37t_p44)Definitions: Pow(44,2 · 38,hj32_local_value_h37t_p44)Original native command in the exact edition - L21
specialize htotal 44 - L22
specialize htotal 2 * 38 - L23
exact htotal
06Separate the logical casesL24–24
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L24
cases h37t_p44
07Establish h37t_baseL25–25
Establish this local claim before using it. It is not an additional assumption.
08Construct an explicit witnessL26–26
Supply the displayed value, then prove that it has the required property.
- L26
exists 6
09Calculate and transport equalitiesL27–27
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L27
norm_num
10Establish h37t_to_44L28–37
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow base monotone.
11Establish h37t_p4_expL38–41
Establish this local claim before using it. It is not an additional assumption.
- L38
have h37t_p4_exp : ∃ hj32_local_value_h37t_p4_exp. Pow(4,2 · 38,hj32_local_value_h37t_p4_exp)Definitions: Pow(4,2 · 38,hj32_local_value_h37t_p4_exp)Original native command in the exact edition - L39
specialize htotal 4 - L40
specialize htotal 2 * 38 - L41
exact htotal
12Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
cases h37t_p4_exp
13Establish h37t_p11_expL43–46
Establish this local claim before using it. It is not an additional assumption.
- L43
have h37t_p11_exp : ∃ hj32_local_value_h37t_p11_exp. Pow(11,2 · 38,hj32_local_value_h37t_p11_exp)Definitions: Pow(11,2 · 38,hj32_local_value_h37t_p11_exp)Original native command in the exact edition - L44
specialize htotal 11 - L45
specialize htotal 2 * 38 - L46
exact htotal
14Separate the logical casesL47–47
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L47
cases h37t_p11_exp
15Establish h37t_p44_product_graphL48–48
Establish this local claim before using it. It is not an additional assumption.
- L48
have h37t_p44_product_graph : Pow(4 · 11,2 · 38,x)Definitions: Pow(4 · 11,2 · 38,x)Original native command in the exact edition
16Establish h37t_p44_product_baseL49–53
17Establish h37t_p44_productL54–63
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul base.
18Use earlier factsL64–64
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L64
exact h37t_p44_product_graph
19Establish h37t_p4_tailL65–68
Establish this local claim before using it. It is not an additional assumption.
- L65
have h37t_p4_tail : ∃ hj32_local_value_h37t_p4_tail. Pow(4,7 · 19,hj32_local_value_h37t_p4_tail)Definitions: Pow(4,7 · 19,hj32_local_value_h37t_p4_tail)Original native command in the exact edition - L66
specialize htotal 4 - L67
specialize htotal 7 * 19 - L68
exact htotal
20Separate the logical casesL69–69
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L69
cases h37t_p4_tail
21Establish h37t_parityL70–70
Establish this local claim before using it. It is not an additional assumption.
- L70
have h37t_parity : 7 * 38 = 2 * (7 * 19)
22Establish h37t_rootL71–80
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.
23Calculate and transport equalitiesL81–81
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L81
congr
24Use earlier factsL82–84
25Calculate and transport equalitiesL85–85
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L85
refl
26Use earlier factsL86–89
27Establish h37t_eleven_boundL90–99
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow eleven double block le pow four even from total.
- L90
have h37t_eleven_bound : Le(x2,x3)Definitions: Le(x2,x3)Original native command in the exact edition - L91
specialize pow_eleven_double_block_le_pow_four_even_from_total 38 - L92
specialize pow_eleven_double_block_le_pow_four_even_from_total (7 * 19) - L93
specialize pow_eleven_double_block_le_pow_four_even_from_total x2 - L94
specialize pow_eleven_double_block_le_pow_four_even_from_total x3 - L95
apply pow_eleven_double_block_le_pow_four_even_from_total - L96
exact htotal - L97
exact h37t_parity - L98
exact h37t_p11_exp_witness - L99
exact h37t_p4_tail_witness
28Establish h37t_four_reflL100–102
Establish this local claim before using it. It is not an additional assumption.
29Establish h37t_product_boundL103–110
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.
- L103
have h37t_product_bound : Le(x1 · x2,x1 · x3)Definitions: Le(x1 · x2,x1 · x3)Original native command in the exact edition - L104
specialize mul_le_mul x1 - L105
specialize mul_le_mul x1 - L106
specialize mul_le_mul x2 - L107
specialize mul_le_mul x3 - L108
apply mul_le_mul - L109
exact h37t_four_refl - L110
exact h37t_eleven_bound
30Establish h37t_p4_budgetL111–114
Establish this local claim before using it. It is not an additional assumption.
- L111
have h37t_p4_budget : ∃ hj32_local_value_h37t_p4_budget. Pow(4,2 · 38 + 7 · 19,hj32_local_value_h37t_p4_budget)Definitions: Pow(4,2 · 38 + 7 · 19,hj32_local_value_h37t_p4_budget)Original native command in the exact edition - L112
specialize htotal 4 - L113
specialize htotal 2 * 38 + 7 * 19 - L114
exact htotal
31Separate the logical casesL115–115
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L115
cases h37t_p4_budget
32Establish h37t_budget_productL116–125
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.
33Use earlier factsL126–128
34Calculate and transport equalitiesL129–130
35Establish h37t_to_budgetL131–137
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
36Establish hscaledL138–139
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand scaled budget root 37.
- L138
have hscaled : Le(6 · (2 · 38 + 7 · 19),37 · 37)Definitions: Le(6 · (2 · 38 + 7 · 19),37 · 37)Original native command in the exact edition - L139
apply bertrand_scaled_budget_root_37
37Establish hbudget_exponentL140–146
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.
- L140
have hbudget_exponent : Le(2 · 38 + 7 · 19,e)Definitions: Le(2 · 38 + 7 · 19,e)Original native command in the exact edition - L141
specialize ceil_div_six_budget_of_scaled_le (37 * 37) - L142
specialize ceil_div_six_budget_of_scaled_le (2 * 38 + 7 * 19) - L143
specialize ceil_div_six_budget_of_scaled_le e - L144
apply ceil_div_six_budget_of_scaled_le - L145
exact hceiling - L146
exact hscaled
38Establish h37_budget_growthL147–154
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow exponent monotone from total.
- L147
- L148
specialize pow_exponent_monotone_from_total 4 - L149
specialize pow_exponent_monotone_from_total 2 * 38 + 7 * 19 - L150
specialize pow_exponent_monotone_from_total e - L151
specialize pow_exponent_monotone_from_total x4 - L152
specialize pow_exponent_monotone_from_total u - L153
apply pow_exponent_monotone_from_total - L154
exact htotal
39Construct an explicit witnessL155–155
Supply the displayed value, then prove that it has the required property.
- L155
exists 3
40Calculate and transport equalitiesL156–156
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L156
norm_num
41Use earlier factsL157–159
42Establish h37_resultL160–167
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
Original defined command ledger · 167 lines
- 0001
intro e - 0002
intro h - 0003
intro u - 0004
intro htotal - 0005
intro hceiling - 0006
intro hh - 0007
intro hu - 0008
have hh_route : Pow(38,2 · 38,h)Exact native replay line
have hh_route : exists pa_b_hj32_h_37_route pa_c_hj32_h_37_route. ((forall pa_i_hj32_h_37_route_repeat. (exists pa_lt_hj32_h_37_route_repeat_bound. pa_lt_hj32_h_37_route_repeat_bound + S pa_i_hj32_h_37_route_repeat = 2 * 38) -> (((exists pa_h_hj32_h_37_route_repeat_decoded. pa_h_hj32_h_37_route_repeat_decoded + S (38) = S ((S (pa_i_hj32_h_37_route_repeat)) * pa_c_hj32_h_37_route)) /\ exists pa_q_hj32_h_37_route_repeat_decoded. pa_b_hj32_h_37_route = pa_q_hj32_h_37_route_repeat_decoded * S ((S (pa_i_hj32_h_37_route_repeat)) * pa_c_hj32_h_37_route) + (38)))) /\ (exists pa_u_hj32_h_37_route_product pa_v_hj32_h_37_route_product. ((((exists pa_h_hj32_h_37_route_product_start. pa_h_hj32_h_37_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_37_route_product)) /\ exists pa_q_hj32_h_37_route_product_start. pa_u_hj32_h_37_route_product = pa_q_hj32_h_37_route_product_start * S ((S (0)) * pa_v_hj32_h_37_route_product) + (1))) /\ ((((exists pa_h_hj32_h_37_route_product_terminal. pa_h_hj32_h_37_route_product_terminal + S (h) = S ((S (2 * 38)) * pa_v_hj32_h_37_route_product)) /\ exists pa_q_hj32_h_37_route_product_terminal. pa_u_hj32_h_37_route_product = pa_q_hj32_h_37_route_product_terminal * S ((S (2 * 38)) * pa_v_hj32_h_37_route_product) + (h))) /\ forall pa_i_hj32_h_37_route_product. (exists pa_lt_hj32_h_37_route_product_bound. pa_lt_hj32_h_37_route_product_bound + S pa_i_hj32_h_37_route_product = 2 * 38) -> exists pa_p_hj32_h_37_route_product pa_r_hj32_h_37_route_product pa_s_hj32_h_37_route_product. ((((exists pa_h_hj32_h_37_route_product_factor. pa_h_hj32_h_37_route_product_factor + S (pa_p_hj32_h_37_route_product) = S ((S (pa_i_hj32_h_37_route_product)) * pa_c_hj32_h_37_route)) /\ exists pa_q_hj32_h_37_route_product_factor. pa_b_hj32_h_37_route = pa_q_hj32_h_37_route_product_factor * S ((S (pa_i_hj32_h_37_route_product)) * pa_c_hj32_h_37_route) + (pa_p_hj32_h_37_route_product))) /\ ((((exists pa_h_hj32_h_37_route_product_partial. pa_h_hj32_h_37_route_product_partial + S (pa_r_hj32_h_37_route_product) = S ((S (pa_i_hj32_h_37_route_product)) * pa_v_hj32_h_37_route_product)) /\ exists pa_q_hj32_h_37_route_product_partial. pa_u_hj32_h_37_route_product = pa_q_hj32_h_37_route_product_partial * S ((S (pa_i_hj32_h_37_route_product)) * pa_v_hj32_h_37_route_product) + (pa_r_hj32_h_37_route_product))) /\ ((((exists pa_h_hj32_h_37_route_product_successor. pa_h_hj32_h_37_route_product_successor + S (pa_s_hj32_h_37_route_product) = S ((S (S pa_i_hj32_h_37_route_product)) * pa_v_hj32_h_37_route_product)) /\ exists pa_q_hj32_h_37_route_product_successor. pa_u_hj32_h_37_route_product = pa_q_hj32_h_37_route_product_successor * S ((S (S pa_i_hj32_h_37_route_product)) * pa_v_hj32_h_37_route_product) + (pa_s_hj32_h_37_route_product))) /\ pa_s_hj32_h_37_route_product = pa_r_hj32_h_37_route_product * pa_p_hj32_h_37_route_product))))))) - 0009
have hh_base : 37 + 1 = 38 - 0010
norm_num - 0011
have hh_exponent : 2 * 37 + 2 = 2 * 38 - 0012
norm_num - 0013
rewrite <- hh_exponent - 0014
rewrite <- hh_exponent - 0015
rewrite <- hh_exponent - 0016
rewrite <- hh_exponent - 0017
rewrite <- hh_base - 0018
rewrite <- hh_base - 0019
exact hh - 0020
have h37t_p44 : ∃ hj32_local_value_h37t_p44. Pow(44,2 · 38,hj32_local_value_h37t_p44)Exact native replay line
have h37t_p44 : exists hj32_local_value_h37t_p44. (exists pa_b_hj32_local_total_h37t_p44 pa_c_hj32_local_total_h37t_p44. ((forall pa_i_hj32_local_total_h37t_p44_repeat. (exists pa_lt_hj32_local_total_h37t_p44_repeat_bound. pa_lt_hj32_local_total_h37t_p44_repeat_bound + S pa_i_hj32_local_total_h37t_p44_repeat = 2 * 38) -> (((exists pa_h_hj32_local_total_h37t_p44_repeat_decoded. pa_h_hj32_local_total_h37t_p44_repeat_decoded + S (44) = S ((S (pa_i_hj32_local_total_h37t_p44_repeat)) * pa_c_hj32_local_total_h37t_p44)) /\ exists pa_q_hj32_local_total_h37t_p44_repeat_decoded. pa_b_hj32_local_total_h37t_p44 = pa_q_hj32_local_total_h37t_p44_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p44_repeat)) * pa_c_hj32_local_total_h37t_p44) + (44)))) /\ (exists pa_u_hj32_local_total_h37t_p44_product pa_v_hj32_local_total_h37t_p44_product. ((((exists pa_h_hj32_local_total_h37t_p44_product_start. pa_h_hj32_local_total_h37t_p44_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p44_product)) /\ exists pa_q_hj32_local_total_h37t_p44_product_start. pa_u_hj32_local_total_h37t_p44_product = pa_q_hj32_local_total_h37t_p44_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p44_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p44_product_terminal. pa_h_hj32_local_total_h37t_p44_product_terminal + S (hj32_local_value_h37t_p44) = S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p44_product)) /\ exists pa_q_hj32_local_total_h37t_p44_product_terminal. pa_u_hj32_local_total_h37t_p44_product = pa_q_hj32_local_total_h37t_p44_product_terminal * S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p44_product) + (hj32_local_value_h37t_p44))) /\ forall pa_i_hj32_local_total_h37t_p44_product. (exists pa_lt_hj32_local_total_h37t_p44_product_bound. pa_lt_hj32_local_total_h37t_p44_product_bound + S pa_i_hj32_local_total_h37t_p44_product = 2 * 38) -> exists pa_p_hj32_local_total_h37t_p44_product pa_r_hj32_local_total_h37t_p44_product pa_s_hj32_local_total_h37t_p44_product. ((((exists pa_h_hj32_local_total_h37t_p44_product_factor. pa_h_hj32_local_total_h37t_p44_product_factor + S (pa_p_hj32_local_total_h37t_p44_product) = S ((S (pa_i_hj32_local_total_h37t_p44_product)) * pa_c_hj32_local_total_h37t_p44)) /\ exists pa_q_hj32_local_total_h37t_p44_product_factor. pa_b_hj32_local_total_h37t_p44 = pa_q_hj32_local_total_h37t_p44_product_factor * S ((S (pa_i_hj32_local_total_h37t_p44_product)) * pa_c_hj32_local_total_h37t_p44) + (pa_p_hj32_local_total_h37t_p44_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p44_product_partial. pa_h_hj32_local_total_h37t_p44_product_partial + S (pa_r_hj32_local_total_h37t_p44_product) = S ((S (pa_i_hj32_local_total_h37t_p44_product)) * pa_v_hj32_local_total_h37t_p44_product)) /\ exists pa_q_hj32_local_total_h37t_p44_product_partial. pa_u_hj32_local_total_h37t_p44_product = pa_q_hj32_local_total_h37t_p44_product_partial * S ((S (pa_i_hj32_local_total_h37t_p44_product)) * pa_v_hj32_local_total_h37t_p44_product) + (pa_r_hj32_local_total_h37t_p44_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p44_product_successor. pa_h_hj32_local_total_h37t_p44_product_successor + S (pa_s_hj32_local_total_h37t_p44_product) = S ((S (S pa_i_hj32_local_total_h37t_p44_product)) * pa_v_hj32_local_total_h37t_p44_product)) /\ exists pa_q_hj32_local_total_h37t_p44_product_successor. pa_u_hj32_local_total_h37t_p44_product = pa_q_hj32_local_total_h37t_p44_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p44_product)) * pa_v_hj32_local_total_h37t_p44_product) + (pa_s_hj32_local_total_h37t_p44_product))) /\ pa_s_hj32_local_total_h37t_p44_product = pa_r_hj32_local_total_h37t_p44_product * pa_p_hj32_local_total_h37t_p44_product)))))))) - 0021
specialize htotal 44 - 0022
specialize htotal 2 * 38 - 0023
exact htotal - 0024
cases h37t_p44 - 0025
have h37t_base : Lt(37,44)Exact native replay line
have h37t_base : exists bqb_le_gap_hj32_h37t_base. bqb_le_gap_hj32_h37t_base + (38) = (44) - 0026
exists 6 - 0027
norm_num - 0028
have h37t_to_44 : Le(h,x)Exact native replay line
have h37t_to_44 : exists bqb_le_gap_hj32_local_base_bound_h37t_to_44. bqb_le_gap_hj32_local_base_bound_h37t_to_44 + (h) = (x) - 0029
specialize pow_base_monotone 38 - 0030
specialize pow_base_monotone 44 - 0031
specialize pow_base_monotone 2 * 38 - 0032
specialize pow_base_monotone h - 0033
specialize pow_base_monotone x - 0034
apply pow_base_monotone - 0035
exact h37t_base - 0036
exact hh_route - 0037
exact h37t_p44_witness - 0038
have h37t_p4_exp : ∃ hj32_local_value_h37t_p4_exp. Pow(4,2 · 38,hj32_local_value_h37t_p4_exp)Exact native replay line
have h37t_p4_exp : exists hj32_local_value_h37t_p4_exp. (exists pa_b_hj32_local_total_h37t_p4_exp pa_c_hj32_local_total_h37t_p4_exp. ((forall pa_i_hj32_local_total_h37t_p4_exp_repeat. (exists pa_lt_hj32_local_total_h37t_p4_exp_repeat_bound. pa_lt_hj32_local_total_h37t_p4_exp_repeat_bound + S pa_i_hj32_local_total_h37t_p4_exp_repeat = 2 * 38) -> (((exists pa_h_hj32_local_total_h37t_p4_exp_repeat_decoded. pa_h_hj32_local_total_h37t_p4_exp_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h37t_p4_exp_repeat)) * pa_c_hj32_local_total_h37t_p4_exp)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_repeat_decoded. pa_b_hj32_local_total_h37t_p4_exp = pa_q_hj32_local_total_h37t_p4_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p4_exp_repeat)) * pa_c_hj32_local_total_h37t_p4_exp) + (4)))) /\ (exists pa_u_hj32_local_total_h37t_p4_exp_product pa_v_hj32_local_total_h37t_p4_exp_product. ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_start. pa_h_hj32_local_total_h37t_p4_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_start. pa_u_hj32_local_total_h37t_p4_exp_product = pa_q_hj32_local_total_h37t_p4_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p4_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_terminal. pa_h_hj32_local_total_h37t_p4_exp_product_terminal + S (hj32_local_value_h37t_p4_exp) = S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_terminal. pa_u_hj32_local_total_h37t_p4_exp_product = pa_q_hj32_local_total_h37t_p4_exp_product_terminal * S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p4_exp_product) + (hj32_local_value_h37t_p4_exp))) /\ forall pa_i_hj32_local_total_h37t_p4_exp_product. (exists pa_lt_hj32_local_total_h37t_p4_exp_product_bound. pa_lt_hj32_local_total_h37t_p4_exp_product_bound + S pa_i_hj32_local_total_h37t_p4_exp_product = 2 * 38) -> exists pa_p_hj32_local_total_h37t_p4_exp_product pa_r_hj32_local_total_h37t_p4_exp_product pa_s_hj32_local_total_h37t_p4_exp_product. ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_factor. pa_h_hj32_local_total_h37t_p4_exp_product_factor + S (pa_p_hj32_local_total_h37t_p4_exp_product) = S ((S (pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_c_hj32_local_total_h37t_p4_exp)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_factor. pa_b_hj32_local_total_h37t_p4_exp = pa_q_hj32_local_total_h37t_p4_exp_product_factor * S ((S (pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_c_hj32_local_total_h37t_p4_exp) + (pa_p_hj32_local_total_h37t_p4_exp_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_partial. pa_h_hj32_local_total_h37t_p4_exp_product_partial + S (pa_r_hj32_local_total_h37t_p4_exp_product) = S ((S (pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_v_hj32_local_total_h37t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_partial. pa_u_hj32_local_total_h37t_p4_exp_product = pa_q_hj32_local_total_h37t_p4_exp_product_partial * S ((S (pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_v_hj32_local_total_h37t_p4_exp_product) + (pa_r_hj32_local_total_h37t_p4_exp_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_successor. pa_h_hj32_local_total_h37t_p4_exp_product_successor + S (pa_s_hj32_local_total_h37t_p4_exp_product) = S ((S (S pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_v_hj32_local_total_h37t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_successor. pa_u_hj32_local_total_h37t_p4_exp_product = pa_q_hj32_local_total_h37t_p4_exp_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_v_hj32_local_total_h37t_p4_exp_product) + (pa_s_hj32_local_total_h37t_p4_exp_product))) /\ pa_s_hj32_local_total_h37t_p4_exp_product = pa_r_hj32_local_total_h37t_p4_exp_product * pa_p_hj32_local_total_h37t_p4_exp_product)))))))) - 0039
specialize htotal 4 - 0040
specialize htotal 2 * 38 - 0041
exact htotal - 0042
cases h37t_p4_exp - 0043
have h37t_p11_exp : ∃ hj32_local_value_h37t_p11_exp. Pow(11,2 · 38,hj32_local_value_h37t_p11_exp)Exact native replay line
have h37t_p11_exp : exists hj32_local_value_h37t_p11_exp. (exists pa_b_hj32_local_total_h37t_p11_exp pa_c_hj32_local_total_h37t_p11_exp. ((forall pa_i_hj32_local_total_h37t_p11_exp_repeat. (exists pa_lt_hj32_local_total_h37t_p11_exp_repeat_bound. pa_lt_hj32_local_total_h37t_p11_exp_repeat_bound + S pa_i_hj32_local_total_h37t_p11_exp_repeat = 2 * 38) -> (((exists pa_h_hj32_local_total_h37t_p11_exp_repeat_decoded. pa_h_hj32_local_total_h37t_p11_exp_repeat_decoded + S (11) = S ((S (pa_i_hj32_local_total_h37t_p11_exp_repeat)) * pa_c_hj32_local_total_h37t_p11_exp)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_repeat_decoded. pa_b_hj32_local_total_h37t_p11_exp = pa_q_hj32_local_total_h37t_p11_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p11_exp_repeat)) * pa_c_hj32_local_total_h37t_p11_exp) + (11)))) /\ (exists pa_u_hj32_local_total_h37t_p11_exp_product pa_v_hj32_local_total_h37t_p11_exp_product. ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_start. pa_h_hj32_local_total_h37t_p11_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_start. pa_u_hj32_local_total_h37t_p11_exp_product = pa_q_hj32_local_total_h37t_p11_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p11_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_terminal. pa_h_hj32_local_total_h37t_p11_exp_product_terminal + S (hj32_local_value_h37t_p11_exp) = S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_terminal. pa_u_hj32_local_total_h37t_p11_exp_product = pa_q_hj32_local_total_h37t_p11_exp_product_terminal * S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p11_exp_product) + (hj32_local_value_h37t_p11_exp))) /\ forall pa_i_hj32_local_total_h37t_p11_exp_product. (exists pa_lt_hj32_local_total_h37t_p11_exp_product_bound. pa_lt_hj32_local_total_h37t_p11_exp_product_bound + S pa_i_hj32_local_total_h37t_p11_exp_product = 2 * 38) -> exists pa_p_hj32_local_total_h37t_p11_exp_product pa_r_hj32_local_total_h37t_p11_exp_product pa_s_hj32_local_total_h37t_p11_exp_product. ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_factor. pa_h_hj32_local_total_h37t_p11_exp_product_factor + S (pa_p_hj32_local_total_h37t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_c_hj32_local_total_h37t_p11_exp)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_factor. pa_b_hj32_local_total_h37t_p11_exp = pa_q_hj32_local_total_h37t_p11_exp_product_factor * S ((S (pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_c_hj32_local_total_h37t_p11_exp) + (pa_p_hj32_local_total_h37t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_partial. pa_h_hj32_local_total_h37t_p11_exp_product_partial + S (pa_r_hj32_local_total_h37t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_v_hj32_local_total_h37t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_partial. pa_u_hj32_local_total_h37t_p11_exp_product = pa_q_hj32_local_total_h37t_p11_exp_product_partial * S ((S (pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_v_hj32_local_total_h37t_p11_exp_product) + (pa_r_hj32_local_total_h37t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_successor. pa_h_hj32_local_total_h37t_p11_exp_product_successor + S (pa_s_hj32_local_total_h37t_p11_exp_product) = S ((S (S pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_v_hj32_local_total_h37t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_successor. pa_u_hj32_local_total_h37t_p11_exp_product = pa_q_hj32_local_total_h37t_p11_exp_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_v_hj32_local_total_h37t_p11_exp_product) + (pa_s_hj32_local_total_h37t_p11_exp_product))) /\ pa_s_hj32_local_total_h37t_p11_exp_product = pa_r_hj32_local_total_h37t_p11_exp_product * pa_p_hj32_local_total_h37t_p11_exp_product)))))))) - 0044
specialize htotal 11 - 0045
specialize htotal 2 * 38 - 0046
exact htotal - 0047
cases h37t_p11_exp - 0048
have h37t_p44_product_graph : Pow(4 · 11,2 · 38,x)Exact native replay line
have h37t_p44_product_graph : exists pa_b_hj32_local_product_h37t_p44_product pa_c_hj32_local_product_h37t_p44_product. ((forall pa_i_hj32_local_product_h37t_p44_product_repeat. (exists pa_lt_hj32_local_product_h37t_p44_product_repeat_bound. pa_lt_hj32_local_product_h37t_p44_product_repeat_bound + S pa_i_hj32_local_product_h37t_p44_product_repeat = 2 * 38) -> (((exists pa_h_hj32_local_product_h37t_p44_product_repeat_decoded. pa_h_hj32_local_product_h37t_p44_product_repeat_decoded + S (4 * 11) = S ((S (pa_i_hj32_local_product_h37t_p44_product_repeat)) * pa_c_hj32_local_product_h37t_p44_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_repeat_decoded. pa_b_hj32_local_product_h37t_p44_product = pa_q_hj32_local_product_h37t_p44_product_repeat_decoded * S ((S (pa_i_hj32_local_product_h37t_p44_product_repeat)) * pa_c_hj32_local_product_h37t_p44_product) + (4 * 11)))) /\ (exists pa_u_hj32_local_product_h37t_p44_product_product pa_v_hj32_local_product_h37t_p44_product_product. ((((exists pa_h_hj32_local_product_h37t_p44_product_product_start. pa_h_hj32_local_product_h37t_p44_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_h37t_p44_product_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_start. pa_u_hj32_local_product_h37t_p44_product_product = pa_q_hj32_local_product_h37t_p44_product_product_start * S ((S (0)) * pa_v_hj32_local_product_h37t_p44_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_h37t_p44_product_product_terminal. pa_h_hj32_local_product_h37t_p44_product_product_terminal + S (x) = S ((S (2 * 38)) * pa_v_hj32_local_product_h37t_p44_product_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_terminal. pa_u_hj32_local_product_h37t_p44_product_product = pa_q_hj32_local_product_h37t_p44_product_product_terminal * S ((S (2 * 38)) * pa_v_hj32_local_product_h37t_p44_product_product) + (x))) /\ forall pa_i_hj32_local_product_h37t_p44_product_product. (exists pa_lt_hj32_local_product_h37t_p44_product_product_bound. pa_lt_hj32_local_product_h37t_p44_product_product_bound + S pa_i_hj32_local_product_h37t_p44_product_product = 2 * 38) -> exists pa_p_hj32_local_product_h37t_p44_product_product pa_r_hj32_local_product_h37t_p44_product_product pa_s_hj32_local_product_h37t_p44_product_product. ((((exists pa_h_hj32_local_product_h37t_p44_product_product_factor. pa_h_hj32_local_product_h37t_p44_product_product_factor + S (pa_p_hj32_local_product_h37t_p44_product_product) = S ((S (pa_i_hj32_local_product_h37t_p44_product_product)) * pa_c_hj32_local_product_h37t_p44_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_factor. pa_b_hj32_local_product_h37t_p44_product = pa_q_hj32_local_product_h37t_p44_product_product_factor * S ((S (pa_i_hj32_local_product_h37t_p44_product_product)) * pa_c_hj32_local_product_h37t_p44_product) + (pa_p_hj32_local_product_h37t_p44_product_product))) /\ ((((exists pa_h_hj32_local_product_h37t_p44_product_product_partial. pa_h_hj32_local_product_h37t_p44_product_product_partial + S (pa_r_hj32_local_product_h37t_p44_product_product) = S ((S (pa_i_hj32_local_product_h37t_p44_product_product)) * pa_v_hj32_local_product_h37t_p44_product_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_partial. pa_u_hj32_local_product_h37t_p44_product_product = pa_q_hj32_local_product_h37t_p44_product_product_partial * S ((S (pa_i_hj32_local_product_h37t_p44_product_product)) * pa_v_hj32_local_product_h37t_p44_product_product) + (pa_r_hj32_local_product_h37t_p44_product_product))) /\ ((((exists pa_h_hj32_local_product_h37t_p44_product_product_successor. pa_h_hj32_local_product_h37t_p44_product_product_successor + S (pa_s_hj32_local_product_h37t_p44_product_product) = S ((S (S pa_i_hj32_local_product_h37t_p44_product_product)) * pa_v_hj32_local_product_h37t_p44_product_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_successor. pa_u_hj32_local_product_h37t_p44_product_product = pa_q_hj32_local_product_h37t_p44_product_product_successor * S ((S (S pa_i_hj32_local_product_h37t_p44_product_product)) * pa_v_hj32_local_product_h37t_p44_product_product) + (pa_s_hj32_local_product_h37t_p44_product_product))) /\ pa_s_hj32_local_product_h37t_p44_product_product = pa_r_hj32_local_product_h37t_p44_product_product * pa_p_hj32_local_product_h37t_p44_product_product))))))) - 0049
have h37t_p44_product_base : 4 * 11 = 44 - 0050
norm_num - 0051
rewrite h37t_p44_product_base - 0052
rewrite h37t_p44_product_base - 0053
exact h37t_p44_witness - 0054
have h37t_p44_product : x = x1 * x2 - 0055
specialize pow_mul_base 4 - 0056
specialize pow_mul_base 11 - 0057
specialize pow_mul_base 2 * 38 - 0058
specialize pow_mul_base x1 - 0059
specialize pow_mul_base x2 - 0060
specialize pow_mul_base x - 0061
apply pow_mul_base - 0062
exact h37t_p4_exp_witness - 0063
exact h37t_p11_exp_witness - 0064
exact h37t_p44_product_graph - 0065
have h37t_p4_tail : ∃ hj32_local_value_h37t_p4_tail. Pow(4,7 · 19,hj32_local_value_h37t_p4_tail)Exact native replay line
have h37t_p4_tail : exists hj32_local_value_h37t_p4_tail. (exists pa_b_hj32_local_total_h37t_p4_tail pa_c_hj32_local_total_h37t_p4_tail. ((forall pa_i_hj32_local_total_h37t_p4_tail_repeat. (exists pa_lt_hj32_local_total_h37t_p4_tail_repeat_bound. pa_lt_hj32_local_total_h37t_p4_tail_repeat_bound + S pa_i_hj32_local_total_h37t_p4_tail_repeat = 7 * 19) -> (((exists pa_h_hj32_local_total_h37t_p4_tail_repeat_decoded. pa_h_hj32_local_total_h37t_p4_tail_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h37t_p4_tail_repeat)) * pa_c_hj32_local_total_h37t_p4_tail)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_repeat_decoded. pa_b_hj32_local_total_h37t_p4_tail = pa_q_hj32_local_total_h37t_p4_tail_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p4_tail_repeat)) * pa_c_hj32_local_total_h37t_p4_tail) + (4)))) /\ (exists pa_u_hj32_local_total_h37t_p4_tail_product pa_v_hj32_local_total_h37t_p4_tail_product. ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_start. pa_h_hj32_local_total_h37t_p4_tail_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_start. pa_u_hj32_local_total_h37t_p4_tail_product = pa_q_hj32_local_total_h37t_p4_tail_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p4_tail_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_terminal. pa_h_hj32_local_total_h37t_p4_tail_product_terminal + S (hj32_local_value_h37t_p4_tail) = S ((S (7 * 19)) * pa_v_hj32_local_total_h37t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_terminal. pa_u_hj32_local_total_h37t_p4_tail_product = pa_q_hj32_local_total_h37t_p4_tail_product_terminal * S ((S (7 * 19)) * pa_v_hj32_local_total_h37t_p4_tail_product) + (hj32_local_value_h37t_p4_tail))) /\ forall pa_i_hj32_local_total_h37t_p4_tail_product. (exists pa_lt_hj32_local_total_h37t_p4_tail_product_bound. pa_lt_hj32_local_total_h37t_p4_tail_product_bound + S pa_i_hj32_local_total_h37t_p4_tail_product = 7 * 19) -> exists pa_p_hj32_local_total_h37t_p4_tail_product pa_r_hj32_local_total_h37t_p4_tail_product pa_s_hj32_local_total_h37t_p4_tail_product. ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_factor. pa_h_hj32_local_total_h37t_p4_tail_product_factor + S (pa_p_hj32_local_total_h37t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_c_hj32_local_total_h37t_p4_tail)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_factor. pa_b_hj32_local_total_h37t_p4_tail = pa_q_hj32_local_total_h37t_p4_tail_product_factor * S ((S (pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_c_hj32_local_total_h37t_p4_tail) + (pa_p_hj32_local_total_h37t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_partial. pa_h_hj32_local_total_h37t_p4_tail_product_partial + S (pa_r_hj32_local_total_h37t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_v_hj32_local_total_h37t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_partial. pa_u_hj32_local_total_h37t_p4_tail_product = pa_q_hj32_local_total_h37t_p4_tail_product_partial * S ((S (pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_v_hj32_local_total_h37t_p4_tail_product) + (pa_r_hj32_local_total_h37t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_successor. pa_h_hj32_local_total_h37t_p4_tail_product_successor + S (pa_s_hj32_local_total_h37t_p4_tail_product) = S ((S (S pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_v_hj32_local_total_h37t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_successor. pa_u_hj32_local_total_h37t_p4_tail_product = pa_q_hj32_local_total_h37t_p4_tail_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_v_hj32_local_total_h37t_p4_tail_product) + (pa_s_hj32_local_total_h37t_p4_tail_product))) /\ pa_s_hj32_local_total_h37t_p4_tail_product = pa_r_hj32_local_total_h37t_p4_tail_product * pa_p_hj32_local_total_h37t_p4_tail_product)))))))) - 0066
specialize htotal 4 - 0067
specialize htotal 7 * 19 - 0068
exact htotal - 0069
cases h37t_p4_tail - 0070
have h37t_parity : 7 * 38 = 2 * (7 * 19) - 0071
have h37t_root : 38 = 2 * 19 - 0072
norm_num - 0073
rewrite h37t_root - 0074
trans (7 * 2) * 19 - 0075
symm - 0076
specialize mul_assoc 7 - 0077
specialize mul_assoc 2 - 0078
specialize mul_assoc 19 - 0079
apply mul_assoc - 0080
trans (2 * 7) * 19 - 0081
congr - 0082
specialize mul_comm 7 - 0083
specialize mul_comm 2 - 0084
apply mul_comm - 0085
refl - 0086
specialize mul_assoc 2 - 0087
specialize mul_assoc 7 - 0088
specialize mul_assoc 19 - 0089
apply mul_assoc - 0090
have h37t_eleven_bound : Le(x2,x3)Exact native replay line
have h37t_eleven_bound : exists bqb_le_gap_hj32_h37t_eleven_bound. bqb_le_gap_hj32_h37t_eleven_bound + (x2) = (x3) - 0091
specialize pow_eleven_double_block_le_pow_four_even_from_total 38 - 0092
specialize pow_eleven_double_block_le_pow_four_even_from_total (7 * 19) - 0093
specialize pow_eleven_double_block_le_pow_four_even_from_total x2 - 0094
specialize pow_eleven_double_block_le_pow_four_even_from_total x3 - 0095
apply pow_eleven_double_block_le_pow_four_even_from_total - 0096
exact htotal - 0097
exact h37t_parity - 0098
exact h37t_p11_exp_witness - 0099
exact h37t_p4_tail_witness - 0100
have h37t_four_refl : Le(x1,x1)Exact native replay line
have h37t_four_refl : exists bqb_le_gap_hj32_h37t_four_refl. bqb_le_gap_hj32_h37t_four_refl + (x1) = (x1) - 0101
specialize le_refl x1 - 0102
exact le_refl - 0103
have h37t_product_bound : Le(x1 · x2,x1 · x3)Exact native replay line
have h37t_product_bound : exists bqb_le_gap_hj32_local_product_bound_h37t_product_bound. bqb_le_gap_hj32_local_product_bound_h37t_product_bound + (x1 * x2) = (x1 * x3) - 0104
specialize mul_le_mul x1 - 0105
specialize mul_le_mul x1 - 0106
specialize mul_le_mul x2 - 0107
specialize mul_le_mul x3 - 0108
apply mul_le_mul - 0109
exact h37t_four_refl - 0110
exact h37t_eleven_bound - 0111
have h37t_p4_budget : ∃ hj32_local_value_h37t_p4_budget. Pow(4,2 · 38 + 7 · 19,hj32_local_value_h37t_p4_budget)Exact native replay line
have h37t_p4_budget : exists hj32_local_value_h37t_p4_budget. (exists pa_b_hj32_local_total_h37t_p4_budget pa_c_hj32_local_total_h37t_p4_budget. ((forall pa_i_hj32_local_total_h37t_p4_budget_repeat. (exists pa_lt_hj32_local_total_h37t_p4_budget_repeat_bound. pa_lt_hj32_local_total_h37t_p4_budget_repeat_bound + S pa_i_hj32_local_total_h37t_p4_budget_repeat = 2 * 38 + 7 * 19) -> (((exists pa_h_hj32_local_total_h37t_p4_budget_repeat_decoded. pa_h_hj32_local_total_h37t_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h37t_p4_budget_repeat)) * pa_c_hj32_local_total_h37t_p4_budget)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_repeat_decoded. pa_b_hj32_local_total_h37t_p4_budget = pa_q_hj32_local_total_h37t_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p4_budget_repeat)) * pa_c_hj32_local_total_h37t_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h37t_p4_budget_product pa_v_hj32_local_total_h37t_p4_budget_product. ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_start. pa_h_hj32_local_total_h37t_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_start. pa_u_hj32_local_total_h37t_p4_budget_product = pa_q_hj32_local_total_h37t_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_terminal. pa_h_hj32_local_total_h37t_p4_budget_product_terminal + S (hj32_local_value_h37t_p4_budget) = S ((S (2 * 38 + 7 * 19)) * pa_v_hj32_local_total_h37t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_terminal. pa_u_hj32_local_total_h37t_p4_budget_product = pa_q_hj32_local_total_h37t_p4_budget_product_terminal * S ((S (2 * 38 + 7 * 19)) * pa_v_hj32_local_total_h37t_p4_budget_product) + (hj32_local_value_h37t_p4_budget))) /\ forall pa_i_hj32_local_total_h37t_p4_budget_product. (exists pa_lt_hj32_local_total_h37t_p4_budget_product_bound. pa_lt_hj32_local_total_h37t_p4_budget_product_bound + S pa_i_hj32_local_total_h37t_p4_budget_product = 2 * 38 + 7 * 19) -> exists pa_p_hj32_local_total_h37t_p4_budget_product pa_r_hj32_local_total_h37t_p4_budget_product pa_s_hj32_local_total_h37t_p4_budget_product. ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_factor. pa_h_hj32_local_total_h37t_p4_budget_product_factor + S (pa_p_hj32_local_total_h37t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_c_hj32_local_total_h37t_p4_budget)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_factor. pa_b_hj32_local_total_h37t_p4_budget = pa_q_hj32_local_total_h37t_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_c_hj32_local_total_h37t_p4_budget) + (pa_p_hj32_local_total_h37t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_partial. pa_h_hj32_local_total_h37t_p4_budget_product_partial + S (pa_r_hj32_local_total_h37t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_v_hj32_local_total_h37t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_partial. pa_u_hj32_local_total_h37t_p4_budget_product = pa_q_hj32_local_total_h37t_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_v_hj32_local_total_h37t_p4_budget_product) + (pa_r_hj32_local_total_h37t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_successor. pa_h_hj32_local_total_h37t_p4_budget_product_successor + S (pa_s_hj32_local_total_h37t_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_v_hj32_local_total_h37t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_successor. pa_u_hj32_local_total_h37t_p4_budget_product = pa_q_hj32_local_total_h37t_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_v_hj32_local_total_h37t_p4_budget_product) + (pa_s_hj32_local_total_h37t_p4_budget_product))) /\ pa_s_hj32_local_total_h37t_p4_budget_product = pa_r_hj32_local_total_h37t_p4_budget_product * pa_p_hj32_local_total_h37t_p4_budget_product)))))))) - 0112
specialize htotal 4 - 0113
specialize htotal 2 * 38 + 7 * 19 - 0114
exact htotal - 0115
cases h37t_p4_budget - 0116
have h37t_budget_product : x4 = x1 * x3 - 0117
specialize pow_add 4 - 0118
specialize pow_add 2 * 38 - 0119
specialize pow_add 7 * 19 - 0120
specialize pow_add 2 * 38 + 7 * 19 - 0121
specialize pow_add x1 - 0122
specialize pow_add x3 - 0123
specialize pow_add x4 - 0124
apply pow_add - 0125
refl - 0126
exact h37t_p4_exp_witness - 0127
exact h37t_p4_tail_witness - 0128
exact h37t_p4_budget_witness - 0129
rewrite <- h37t_p44_product at h37t_product_bound - 0130
rewrite <- h37t_budget_product at h37t_product_bound - 0131
have h37t_to_budget : Le(h,x4)Exact native replay line
have h37t_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h37t_to_budget. bqb_le_gap_hj32_local_trans_bound_h37t_to_budget + (h) = (x4) - 0132
specialize le_trans h - 0133
specialize le_trans x - 0134
specialize le_trans x4 - 0135
apply le_trans - 0136
exact h37t_to_44 - 0137
exact h37t_product_bound - 0138
have hscaled : Le(6 · (2 · 38 + 7 · 19),37 · 37)Exact native replay line
have hscaled : exists bqb_le_gap_hj32_scaled_budget_root_37. bqb_le_gap_hj32_scaled_budget_root_37 + (6 * (2 * 38 + 7 * 19)) = (37 * 37) - 0139
apply bertrand_scaled_budget_root_37 - 0140
have hbudget_exponent : Le(2 · 38 + 7 · 19,e)Exact native replay line
have hbudget_exponent : exists bqb_le_gap_hj32_h_37_budget_exponent. bqb_le_gap_hj32_h_37_budget_exponent + (2 * 38 + 7 * 19) = (e) - 0141
specialize ceil_div_six_budget_of_scaled_le (37 * 37) - 0142
specialize ceil_div_six_budget_of_scaled_le (2 * 38 + 7 * 19) - 0143
specialize ceil_div_six_budget_of_scaled_le e - 0144
apply ceil_div_six_budget_of_scaled_le - 0145
exact hceiling - 0146
exact hscaled - 0147
have h37_budget_growth : Le(x4,u)Exact native replay line
have h37_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h37_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h37_budget_growth + (x4) = (u) - 0148
specialize pow_exponent_monotone_from_total 4 - 0149
specialize pow_exponent_monotone_from_total 2 * 38 + 7 * 19 - 0150
specialize pow_exponent_monotone_from_total e - 0151
specialize pow_exponent_monotone_from_total x4 - 0152
specialize pow_exponent_monotone_from_total u - 0153
apply pow_exponent_monotone_from_total - 0154
exact htotal - 0155
exists 3 - 0156
norm_num - 0157
exact hbudget_exponent - 0158
exact h37t_p4_budget_witness - 0159
exact hu - 0160
have h37_result : Le(h,u)Exact native replay line
have h37_result : exists bqb_le_gap_hj32_local_trans_bound_h37_result. bqb_le_gap_hj32_local_trans_bound_h37_result + (h) = (u) - 0161
specialize le_trans h - 0162
specialize le_trans x4 - 0163
specialize le_trans u - 0164
apply le_trans - 0165
exact h37t_to_budget - 0166
exact h37_budget_growth - 0167
exact h37_result