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(34 · 34,e) → Pow(34 + 1,2 · 34 + 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
15 occurrences
Exact expanded native-PA statement
forall e h u. (forall bpt_a_hj32_h_root_34 bpt_e_hj32_h_root_34. exists bpt_x_hj32_h_root_34. (exists ff_b_bpt_value_hj32_h_root_34 ff_c_bpt_value_hj32_h_root_34. ((forall ff_i_bpt_value_hj32_h_root_34_repeat. (exists ff_lt_bpt_value_hj32_h_root_34_repeat_bound. ff_lt_bpt_value_hj32_h_root_34_repeat_bound + S ff_i_bpt_value_hj32_h_root_34_repeat = bpt_e_hj32_h_root_34) -> (((exists ff_h_bpt_value_hj32_h_root_34_repeat_decoded. ff_h_bpt_value_hj32_h_root_34_repeat_decoded + S (bpt_a_hj32_h_root_34) = S ((S (ff_i_bpt_value_hj32_h_root_34_repeat)) * ff_c_bpt_value_hj32_h_root_34)) /\ exists ff_q_bpt_value_hj32_h_root_34_repeat_decoded. ff_b_bpt_value_hj32_h_root_34 = ff_q_bpt_value_hj32_h_root_34_repeat_decoded * S ((S (ff_i_bpt_value_hj32_h_root_34_repeat)) * ff_c_bpt_value_hj32_h_root_34) + (bpt_a_hj32_h_root_34)))) /\ (exists ff_u_bpt_value_hj32_h_root_34_product ff_v_bpt_value_hj32_h_root_34_product. ((((exists ff_h_bpt_value_hj32_h_root_34_product_start. ff_h_bpt_value_hj32_h_root_34_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_h_root_34_product)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_start. ff_u_bpt_value_hj32_h_root_34_product = ff_q_bpt_value_hj32_h_root_34_product_start * S ((S (0)) * ff_v_bpt_value_hj32_h_root_34_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_h_root_34_product_terminal. ff_h_bpt_value_hj32_h_root_34_product_terminal + S (bpt_x_hj32_h_root_34) = S ((S (bpt_e_hj32_h_root_34)) * ff_v_bpt_value_hj32_h_root_34_product)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_terminal. ff_u_bpt_value_hj32_h_root_34_product = ff_q_bpt_value_hj32_h_root_34_product_terminal * S ((S (bpt_e_hj32_h_root_34)) * ff_v_bpt_value_hj32_h_root_34_product) + (bpt_x_hj32_h_root_34))) /\ forall ff_i_bpt_value_hj32_h_root_34_product. (exists ff_lt_bpt_value_hj32_h_root_34_product_bound. ff_lt_bpt_value_hj32_h_root_34_product_bound + S ff_i_bpt_value_hj32_h_root_34_product = bpt_e_hj32_h_root_34) -> exists ff_p_bpt_value_hj32_h_root_34_product ff_r_bpt_value_hj32_h_root_34_product ff_s_bpt_value_hj32_h_root_34_product. ((((exists ff_h_bpt_value_hj32_h_root_34_product_factor. ff_h_bpt_value_hj32_h_root_34_product_factor + S (ff_p_bpt_value_hj32_h_root_34_product) = S ((S (ff_i_bpt_value_hj32_h_root_34_product)) * ff_c_bpt_value_hj32_h_root_34)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_factor. ff_b_bpt_value_hj32_h_root_34 = ff_q_bpt_value_hj32_h_root_34_product_factor * S ((S (ff_i_bpt_value_hj32_h_root_34_product)) * ff_c_bpt_value_hj32_h_root_34) + (ff_p_bpt_value_hj32_h_root_34_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_34_product_partial. ff_h_bpt_value_hj32_h_root_34_product_partial + S (ff_r_bpt_value_hj32_h_root_34_product) = S ((S (ff_i_bpt_value_hj32_h_root_34_product)) * ff_v_bpt_value_hj32_h_root_34_product)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_partial. ff_u_bpt_value_hj32_h_root_34_product = ff_q_bpt_value_hj32_h_root_34_product_partial * S ((S (ff_i_bpt_value_hj32_h_root_34_product)) * ff_v_bpt_value_hj32_h_root_34_product) + (ff_r_bpt_value_hj32_h_root_34_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_34_product_successor. ff_h_bpt_value_hj32_h_root_34_product_successor + S (ff_s_bpt_value_hj32_h_root_34_product) = S ((S (S ff_i_bpt_value_hj32_h_root_34_product)) * ff_v_bpt_value_hj32_h_root_34_product)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_successor. ff_u_bpt_value_hj32_h_root_34_product = ff_q_bpt_value_hj32_h_root_34_product_successor * S ((S (S ff_i_bpt_value_hj32_h_root_34_product)) * ff_v_bpt_value_hj32_h_root_34_product) + (ff_s_bpt_value_hj32_h_root_34_product))) /\ ff_s_bpt_value_hj32_h_root_34_product = ff_r_bpt_value_hj32_h_root_34_product * ff_p_bpt_value_hj32_h_root_34_product))))))))) -> (((exists bcs_lower_gap_hj32_h_root_34_ceiling. bcs_lower_gap_hj32_h_root_34_ceiling + (34 * 34) = 6 * (e)) /\ exists bcs_upper_gap_hj32_h_root_34_ceiling. bcs_upper_gap_hj32_h_root_34_ceiling + S (6 * (e)) = (34 * 34) + 6)) -> (exists pa_b_hj32_h_root_34_h pa_c_hj32_h_root_34_h. ((forall pa_i_hj32_h_root_34_h_repeat. (exists pa_lt_hj32_h_root_34_h_repeat_bound. pa_lt_hj32_h_root_34_h_repeat_bound + S pa_i_hj32_h_root_34_h_repeat = 2 * 34 + 2) -> (((exists pa_h_hj32_h_root_34_h_repeat_decoded. pa_h_hj32_h_root_34_h_repeat_decoded + S (34 + 1) = S ((S (pa_i_hj32_h_root_34_h_repeat)) * pa_c_hj32_h_root_34_h)) /\ exists pa_q_hj32_h_root_34_h_repeat_decoded. pa_b_hj32_h_root_34_h = pa_q_hj32_h_root_34_h_repeat_decoded * S ((S (pa_i_hj32_h_root_34_h_repeat)) * pa_c_hj32_h_root_34_h) + (34 + 1)))) /\ (exists pa_u_hj32_h_root_34_h_product pa_v_hj32_h_root_34_h_product. ((((exists pa_h_hj32_h_root_34_h_product_start. pa_h_hj32_h_root_34_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_34_h_product)) /\ exists pa_q_hj32_h_root_34_h_product_start. pa_u_hj32_h_root_34_h_product = pa_q_hj32_h_root_34_h_product_start * S ((S (0)) * pa_v_hj32_h_root_34_h_product) + (1))) /\ ((((exists pa_h_hj32_h_root_34_h_product_terminal. pa_h_hj32_h_root_34_h_product_terminal + S (h) = S ((S (2 * 34 + 2)) * pa_v_hj32_h_root_34_h_product)) /\ exists pa_q_hj32_h_root_34_h_product_terminal. pa_u_hj32_h_root_34_h_product = pa_q_hj32_h_root_34_h_product_terminal * S ((S (2 * 34 + 2)) * pa_v_hj32_h_root_34_h_product) + (h))) /\ forall pa_i_hj32_h_root_34_h_product. (exists pa_lt_hj32_h_root_34_h_product_bound. pa_lt_hj32_h_root_34_h_product_bound + S pa_i_hj32_h_root_34_h_product = 2 * 34 + 2) -> exists pa_p_hj32_h_root_34_h_product pa_r_hj32_h_root_34_h_product pa_s_hj32_h_root_34_h_product. ((((exists pa_h_hj32_h_root_34_h_product_factor. pa_h_hj32_h_root_34_h_product_factor + S (pa_p_hj32_h_root_34_h_product) = S ((S (pa_i_hj32_h_root_34_h_product)) * pa_c_hj32_h_root_34_h)) /\ exists pa_q_hj32_h_root_34_h_product_factor. pa_b_hj32_h_root_34_h = pa_q_hj32_h_root_34_h_product_factor * S ((S (pa_i_hj32_h_root_34_h_product)) * pa_c_hj32_h_root_34_h) + (pa_p_hj32_h_root_34_h_product))) /\ ((((exists pa_h_hj32_h_root_34_h_product_partial. pa_h_hj32_h_root_34_h_product_partial + S (pa_r_hj32_h_root_34_h_product) = S ((S (pa_i_hj32_h_root_34_h_product)) * pa_v_hj32_h_root_34_h_product)) /\ exists pa_q_hj32_h_root_34_h_product_partial. pa_u_hj32_h_root_34_h_product = pa_q_hj32_h_root_34_h_product_partial * S ((S (pa_i_hj32_h_root_34_h_product)) * pa_v_hj32_h_root_34_h_product) + (pa_r_hj32_h_root_34_h_product))) /\ ((((exists pa_h_hj32_h_root_34_h_product_successor. pa_h_hj32_h_root_34_h_product_successor + S (pa_s_hj32_h_root_34_h_product) = S ((S (S pa_i_hj32_h_root_34_h_product)) * pa_v_hj32_h_root_34_h_product)) /\ exists pa_q_hj32_h_root_34_h_product_successor. pa_u_hj32_h_root_34_h_product = pa_q_hj32_h_root_34_h_product_successor * S ((S (S pa_i_hj32_h_root_34_h_product)) * pa_v_hj32_h_root_34_h_product) + (pa_s_hj32_h_root_34_h_product))) /\ pa_s_hj32_h_root_34_h_product = pa_r_hj32_h_root_34_h_product * pa_p_hj32_h_root_34_h_product)))))))) -> (exists pa_b_hj32_h_root_34_u pa_c_hj32_h_root_34_u. ((forall pa_i_hj32_h_root_34_u_repeat. (exists pa_lt_hj32_h_root_34_u_repeat_bound. pa_lt_hj32_h_root_34_u_repeat_bound + S pa_i_hj32_h_root_34_u_repeat = e) -> (((exists pa_h_hj32_h_root_34_u_repeat_decoded. pa_h_hj32_h_root_34_u_repeat_decoded + S (4) = S ((S (pa_i_hj32_h_root_34_u_repeat)) * pa_c_hj32_h_root_34_u)) /\ exists pa_q_hj32_h_root_34_u_repeat_decoded. pa_b_hj32_h_root_34_u = pa_q_hj32_h_root_34_u_repeat_decoded * S ((S (pa_i_hj32_h_root_34_u_repeat)) * pa_c_hj32_h_root_34_u) + (4)))) /\ (exists pa_u_hj32_h_root_34_u_product pa_v_hj32_h_root_34_u_product. ((((exists pa_h_hj32_h_root_34_u_product_start. pa_h_hj32_h_root_34_u_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_34_u_product)) /\ exists pa_q_hj32_h_root_34_u_product_start. pa_u_hj32_h_root_34_u_product = pa_q_hj32_h_root_34_u_product_start * S ((S (0)) * pa_v_hj32_h_root_34_u_product) + (1))) /\ ((((exists pa_h_hj32_h_root_34_u_product_terminal. pa_h_hj32_h_root_34_u_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_h_root_34_u_product)) /\ exists pa_q_hj32_h_root_34_u_product_terminal. pa_u_hj32_h_root_34_u_product = pa_q_hj32_h_root_34_u_product_terminal * S ((S (e)) * pa_v_hj32_h_root_34_u_product) + (u))) /\ forall pa_i_hj32_h_root_34_u_product. (exists pa_lt_hj32_h_root_34_u_product_bound. pa_lt_hj32_h_root_34_u_product_bound + S pa_i_hj32_h_root_34_u_product = e) -> exists pa_p_hj32_h_root_34_u_product pa_r_hj32_h_root_34_u_product pa_s_hj32_h_root_34_u_product. ((((exists pa_h_hj32_h_root_34_u_product_factor. pa_h_hj32_h_root_34_u_product_factor + S (pa_p_hj32_h_root_34_u_product) = S ((S (pa_i_hj32_h_root_34_u_product)) * pa_c_hj32_h_root_34_u)) /\ exists pa_q_hj32_h_root_34_u_product_factor. pa_b_hj32_h_root_34_u = pa_q_hj32_h_root_34_u_product_factor * S ((S (pa_i_hj32_h_root_34_u_product)) * pa_c_hj32_h_root_34_u) + (pa_p_hj32_h_root_34_u_product))) /\ ((((exists pa_h_hj32_h_root_34_u_product_partial. pa_h_hj32_h_root_34_u_product_partial + S (pa_r_hj32_h_root_34_u_product) = S ((S (pa_i_hj32_h_root_34_u_product)) * pa_v_hj32_h_root_34_u_product)) /\ exists pa_q_hj32_h_root_34_u_product_partial. pa_u_hj32_h_root_34_u_product = pa_q_hj32_h_root_34_u_product_partial * S ((S (pa_i_hj32_h_root_34_u_product)) * pa_v_hj32_h_root_34_u_product) + (pa_r_hj32_h_root_34_u_product))) /\ ((((exists pa_h_hj32_h_root_34_u_product_successor. pa_h_hj32_h_root_34_u_product_successor + S (pa_s_hj32_h_root_34_u_product) = S ((S (S pa_i_hj32_h_root_34_u_product)) * pa_v_hj32_h_root_34_u_product)) /\ exists pa_q_hj32_h_root_34_u_product_successor. pa_u_hj32_h_root_34_u_product = pa_q_hj32_h_root_34_u_product_successor * S ((S (S pa_i_hj32_h_root_34_u_product)) * pa_v_hj32_h_root_34_u_product) + (pa_s_hj32_h_root_34_u_product))) /\ pa_s_hj32_h_root_34_u_product = pa_r_hj32_h_root_34_u_product * pa_p_hj32_h_root_34_u_product)))))))) -> (exists bqb_le_gap_hj32_h_root_34_result. bqb_le_gap_hj32_h_root_34_result + (h) = (u))Proof neighborhood
Direct theorem prerequisites
BT00WA bertrand_scaled_budget_root_34 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 BT00PY pow_base_monotone BT00SN pow_exponent_monotone_from_total BT000F le_trans BT0008 mul_assocDirect 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 (8)
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(35,2 · 35,h)Definitions: Pow(35,2 · 35,h)Original native command in the exact edition
03Establish hh_baseL9–10
04Establish hh_exponentL11–19
05Establish h34s_p36L20–23
Establish this local claim before using it. It is not an additional assumption.
- L20
have h34s_p36 : ∃ hj32_local_value_h34s_p36. Pow(36,2 · 35,hj32_local_value_h34s_p36)Definitions: Pow(36,2 · 35,hj32_local_value_h34s_p36)Original native command in the exact edition - L21
specialize htotal 36 - L22
specialize htotal 2 * 35 - L23
exact htotal
06Separate the logical casesL24–24
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L24
cases h34s_p36
07Establish h34s_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 1
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 h34s_to_36L28–37
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow base monotone.
11Establish h34s_p6_totalL38–41
Establish this local claim before using it. It is not an additional assumption.
- L38
have h34s_p6_total : ∃ hj32_local_value_h34s_p6_total. Pow(6,4 · 35,hj32_local_value_h34s_p6_total)Definitions: Pow(6,4 · 35,hj32_local_value_h34s_p6_total)Original native command in the exact edition - L39
specialize htotal 6 - L40
specialize htotal 4 * 35 - L41
exact htotal
12Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
cases h34s_p6_total
13Establish h34s_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.
- L43
have h34s_conversion : x = x1 - L44
specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total 35 - L45
specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x - L46
specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x1 - L47
apply pow_thirty_six_double_block_eq_pow_six_four_block_from_total - L48
exact htotal - L49
exact h34s_p36_witness - L50
exact h34s_p6_total_witness - L51
rewrite h34s_conversion at h34s_to_36
14Establish h34s_p6_mainL52–55
Establish this local claim before using it. It is not an additional assumption.
- L52
have h34s_p6_main : ∃ hj32_local_value_h34s_p6_main. Pow(6,10 · 14,hj32_local_value_h34s_p6_main)Definitions: Pow(6,10 · 14,hj32_local_value_h34s_p6_main)Original native command in the exact edition - L53
specialize htotal 6 - L54
specialize htotal 10 * 14 - L55
exact htotal
15Separate the logical casesL56–56
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L56
cases h34s_p6_main
16Establish h34s_p4_mainL57–60
Establish this local claim before using it. It is not an additional assumption.
- L57
have h34s_p4_main : ∃ hj32_local_value_h34s_p4_main. Pow(4,13 · 14,hj32_local_value_h34s_p4_main)Definitions: Pow(4,13 · 14,hj32_local_value_h34s_p4_main)Original native command in the exact edition - L58
specialize htotal 4 - L59
specialize htotal 13 * 14 - L60
exact htotal
17Separate the logical casesL61–61
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L61
cases h34s_p4_main
18Establish h34s_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.
- L62
- L63
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 14 - L64
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x2 - L65
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x3 - L66
apply pow_six_ten_block_le_pow_four_thirteen_block_from_total - L67
exact htotal - L68
exact h34s_p6_main_witness - L69
exact h34s_p4_main_witness
19Establish h34s_exponentL70–70
Establish this local claim before using it. It is not an additional assumption.
- L70
have h34s_exponent : 4 * 35 = 10 * 14
20Establish h34s_thirty_fiveL71–73
21Establish h34s_left_assocL74–80
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.
22Establish h34s_fourteenL81–83
23Establish h34s_right_assocL84–90
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.
24Establish h34s_right_twentyL91–93
25Establish h34s_left_twentyL94–97
26Establish h34s_main_powerL98–103
Establish this local claim before using it. It is not an additional assumption.
- L98
have h34s_main_power : Pow(6,10 · 14,x1)Definitions: Pow(6,10 · 14,x1)Original native command in the exact edition - L99
rewrite <- h34s_exponent - L100
rewrite <- h34s_exponent - L101
rewrite <- h34s_exponent - L102
rewrite <- h34s_exponent - L103
exact h34s_p6_total_witness
27Establish h34s_direct_boundL104–111
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.
- L104
have h34s_direct_bound : Le(x1,x3)Definitions: Le(x1,x3)Original native command in the exact edition - L105
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 14 - L106
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x1 - L107
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x3 - L108
apply pow_six_ten_block_le_pow_four_thirteen_block_from_total - L109
exact htotal - L110
exact h34s_main_power - L111
exact h34s_p4_main_witness
28Establish h34s_to_budgetL112–118
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
29Establish hscaledL119–120
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand scaled budget root 34.
- L119
have hscaled : Le(6 · (13 · 14),34 · 34)Definitions: Le(6 · (13 · 14),34 · 34)Original native command in the exact edition - L120
apply bertrand_scaled_budget_root_34
30Establish hbudget_exponentL121–127
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.
- L121
have hbudget_exponent : Le(13 · 14,e)Definitions: Le(13 · 14,e)Original native command in the exact edition - L122
specialize ceil_div_six_budget_of_scaled_le (34 * 34) - L123
specialize ceil_div_six_budget_of_scaled_le (13 * 14) - L124
specialize ceil_div_six_budget_of_scaled_le e - L125
apply ceil_div_six_budget_of_scaled_le - L126
exact hceiling - L127
exact hscaled
31Establish h34_budget_growthL128–135
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow exponent monotone from total.
- L128
- L129
specialize pow_exponent_monotone_from_total 4 - L130
specialize pow_exponent_monotone_from_total 13 * 14 - L131
specialize pow_exponent_monotone_from_total e - L132
specialize pow_exponent_monotone_from_total x3 - L133
specialize pow_exponent_monotone_from_total u - L134
apply pow_exponent_monotone_from_total - L135
exact htotal
32Construct an explicit witnessL136–136
Supply the displayed value, then prove that it has the required property.
- L136
exists 3
33Calculate and transport equalitiesL137–137
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L137
norm_num
34Use earlier factsL138–140
35Establish h34_resultL141–148
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
Original defined command ledger · 148 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(35,2 · 35,h)Exact native replay line
have hh_route : exists pa_b_hj32_h_34_route pa_c_hj32_h_34_route. ((forall pa_i_hj32_h_34_route_repeat. (exists pa_lt_hj32_h_34_route_repeat_bound. pa_lt_hj32_h_34_route_repeat_bound + S pa_i_hj32_h_34_route_repeat = 2 * 35) -> (((exists pa_h_hj32_h_34_route_repeat_decoded. pa_h_hj32_h_34_route_repeat_decoded + S (35) = S ((S (pa_i_hj32_h_34_route_repeat)) * pa_c_hj32_h_34_route)) /\ exists pa_q_hj32_h_34_route_repeat_decoded. pa_b_hj32_h_34_route = pa_q_hj32_h_34_route_repeat_decoded * S ((S (pa_i_hj32_h_34_route_repeat)) * pa_c_hj32_h_34_route) + (35)))) /\ (exists pa_u_hj32_h_34_route_product pa_v_hj32_h_34_route_product. ((((exists pa_h_hj32_h_34_route_product_start. pa_h_hj32_h_34_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_34_route_product)) /\ exists pa_q_hj32_h_34_route_product_start. pa_u_hj32_h_34_route_product = pa_q_hj32_h_34_route_product_start * S ((S (0)) * pa_v_hj32_h_34_route_product) + (1))) /\ ((((exists pa_h_hj32_h_34_route_product_terminal. pa_h_hj32_h_34_route_product_terminal + S (h) = S ((S (2 * 35)) * pa_v_hj32_h_34_route_product)) /\ exists pa_q_hj32_h_34_route_product_terminal. pa_u_hj32_h_34_route_product = pa_q_hj32_h_34_route_product_terminal * S ((S (2 * 35)) * pa_v_hj32_h_34_route_product) + (h))) /\ forall pa_i_hj32_h_34_route_product. (exists pa_lt_hj32_h_34_route_product_bound. pa_lt_hj32_h_34_route_product_bound + S pa_i_hj32_h_34_route_product = 2 * 35) -> exists pa_p_hj32_h_34_route_product pa_r_hj32_h_34_route_product pa_s_hj32_h_34_route_product. ((((exists pa_h_hj32_h_34_route_product_factor. pa_h_hj32_h_34_route_product_factor + S (pa_p_hj32_h_34_route_product) = S ((S (pa_i_hj32_h_34_route_product)) * pa_c_hj32_h_34_route)) /\ exists pa_q_hj32_h_34_route_product_factor. pa_b_hj32_h_34_route = pa_q_hj32_h_34_route_product_factor * S ((S (pa_i_hj32_h_34_route_product)) * pa_c_hj32_h_34_route) + (pa_p_hj32_h_34_route_product))) /\ ((((exists pa_h_hj32_h_34_route_product_partial. pa_h_hj32_h_34_route_product_partial + S (pa_r_hj32_h_34_route_product) = S ((S (pa_i_hj32_h_34_route_product)) * pa_v_hj32_h_34_route_product)) /\ exists pa_q_hj32_h_34_route_product_partial. pa_u_hj32_h_34_route_product = pa_q_hj32_h_34_route_product_partial * S ((S (pa_i_hj32_h_34_route_product)) * pa_v_hj32_h_34_route_product) + (pa_r_hj32_h_34_route_product))) /\ ((((exists pa_h_hj32_h_34_route_product_successor. pa_h_hj32_h_34_route_product_successor + S (pa_s_hj32_h_34_route_product) = S ((S (S pa_i_hj32_h_34_route_product)) * pa_v_hj32_h_34_route_product)) /\ exists pa_q_hj32_h_34_route_product_successor. pa_u_hj32_h_34_route_product = pa_q_hj32_h_34_route_product_successor * S ((S (S pa_i_hj32_h_34_route_product)) * pa_v_hj32_h_34_route_product) + (pa_s_hj32_h_34_route_product))) /\ pa_s_hj32_h_34_route_product = pa_r_hj32_h_34_route_product * pa_p_hj32_h_34_route_product))))))) - 0009
have hh_base : 34 + 1 = 35 - 0010
norm_num - 0011
have hh_exponent : 2 * 34 + 2 = 2 * 35 - 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 h34s_p36 : ∃ hj32_local_value_h34s_p36. Pow(36,2 · 35,hj32_local_value_h34s_p36)Exact native replay line
have h34s_p36 : exists hj32_local_value_h34s_p36. (exists pa_b_hj32_local_total_h34s_p36 pa_c_hj32_local_total_h34s_p36. ((forall pa_i_hj32_local_total_h34s_p36_repeat. (exists pa_lt_hj32_local_total_h34s_p36_repeat_bound. pa_lt_hj32_local_total_h34s_p36_repeat_bound + S pa_i_hj32_local_total_h34s_p36_repeat = 2 * 35) -> (((exists pa_h_hj32_local_total_h34s_p36_repeat_decoded. pa_h_hj32_local_total_h34s_p36_repeat_decoded + S (36) = S ((S (pa_i_hj32_local_total_h34s_p36_repeat)) * pa_c_hj32_local_total_h34s_p36)) /\ exists pa_q_hj32_local_total_h34s_p36_repeat_decoded. pa_b_hj32_local_total_h34s_p36 = pa_q_hj32_local_total_h34s_p36_repeat_decoded * S ((S (pa_i_hj32_local_total_h34s_p36_repeat)) * pa_c_hj32_local_total_h34s_p36) + (36)))) /\ (exists pa_u_hj32_local_total_h34s_p36_product pa_v_hj32_local_total_h34s_p36_product. ((((exists pa_h_hj32_local_total_h34s_p36_product_start. pa_h_hj32_local_total_h34s_p36_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h34s_p36_product)) /\ exists pa_q_hj32_local_total_h34s_p36_product_start. pa_u_hj32_local_total_h34s_p36_product = pa_q_hj32_local_total_h34s_p36_product_start * S ((S (0)) * pa_v_hj32_local_total_h34s_p36_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h34s_p36_product_terminal. pa_h_hj32_local_total_h34s_p36_product_terminal + S (hj32_local_value_h34s_p36) = S ((S (2 * 35)) * pa_v_hj32_local_total_h34s_p36_product)) /\ exists pa_q_hj32_local_total_h34s_p36_product_terminal. pa_u_hj32_local_total_h34s_p36_product = pa_q_hj32_local_total_h34s_p36_product_terminal * S ((S (2 * 35)) * pa_v_hj32_local_total_h34s_p36_product) + (hj32_local_value_h34s_p36))) /\ forall pa_i_hj32_local_total_h34s_p36_product. (exists pa_lt_hj32_local_total_h34s_p36_product_bound. pa_lt_hj32_local_total_h34s_p36_product_bound + S pa_i_hj32_local_total_h34s_p36_product = 2 * 35) -> exists pa_p_hj32_local_total_h34s_p36_product pa_r_hj32_local_total_h34s_p36_product pa_s_hj32_local_total_h34s_p36_product. ((((exists pa_h_hj32_local_total_h34s_p36_product_factor. pa_h_hj32_local_total_h34s_p36_product_factor + S (pa_p_hj32_local_total_h34s_p36_product) = S ((S (pa_i_hj32_local_total_h34s_p36_product)) * pa_c_hj32_local_total_h34s_p36)) /\ exists pa_q_hj32_local_total_h34s_p36_product_factor. pa_b_hj32_local_total_h34s_p36 = pa_q_hj32_local_total_h34s_p36_product_factor * S ((S (pa_i_hj32_local_total_h34s_p36_product)) * pa_c_hj32_local_total_h34s_p36) + (pa_p_hj32_local_total_h34s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p36_product_partial. pa_h_hj32_local_total_h34s_p36_product_partial + S (pa_r_hj32_local_total_h34s_p36_product) = S ((S (pa_i_hj32_local_total_h34s_p36_product)) * pa_v_hj32_local_total_h34s_p36_product)) /\ exists pa_q_hj32_local_total_h34s_p36_product_partial. pa_u_hj32_local_total_h34s_p36_product = pa_q_hj32_local_total_h34s_p36_product_partial * S ((S (pa_i_hj32_local_total_h34s_p36_product)) * pa_v_hj32_local_total_h34s_p36_product) + (pa_r_hj32_local_total_h34s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p36_product_successor. pa_h_hj32_local_total_h34s_p36_product_successor + S (pa_s_hj32_local_total_h34s_p36_product) = S ((S (S pa_i_hj32_local_total_h34s_p36_product)) * pa_v_hj32_local_total_h34s_p36_product)) /\ exists pa_q_hj32_local_total_h34s_p36_product_successor. pa_u_hj32_local_total_h34s_p36_product = pa_q_hj32_local_total_h34s_p36_product_successor * S ((S (S pa_i_hj32_local_total_h34s_p36_product)) * pa_v_hj32_local_total_h34s_p36_product) + (pa_s_hj32_local_total_h34s_p36_product))) /\ pa_s_hj32_local_total_h34s_p36_product = pa_r_hj32_local_total_h34s_p36_product * pa_p_hj32_local_total_h34s_p36_product)))))))) - 0021
specialize htotal 36 - 0022
specialize htotal 2 * 35 - 0023
exact htotal - 0024
cases h34s_p36 - 0025
have h34s_base : Lt(34,36)Exact native replay line
have h34s_base : exists bqb_le_gap_hj32_h34s_base. bqb_le_gap_hj32_h34s_base + (35) = (36) - 0026
exists 1 - 0027
norm_num - 0028
have h34s_to_36 : Le(h,x)Exact native replay line
have h34s_to_36 : exists bqb_le_gap_hj32_local_base_bound_h34s_to_36. bqb_le_gap_hj32_local_base_bound_h34s_to_36 + (h) = (x) - 0029
specialize pow_base_monotone 35 - 0030
specialize pow_base_monotone 36 - 0031
specialize pow_base_monotone 2 * 35 - 0032
specialize pow_base_monotone h - 0033
specialize pow_base_monotone x - 0034
apply pow_base_monotone - 0035
exact h34s_base - 0036
exact hh_route - 0037
exact h34s_p36_witness - 0038
have h34s_p6_total : ∃ hj32_local_value_h34s_p6_total. Pow(6,4 · 35,hj32_local_value_h34s_p6_total)Exact native replay line
have h34s_p6_total : exists hj32_local_value_h34s_p6_total. (exists pa_b_hj32_local_total_h34s_p6_total pa_c_hj32_local_total_h34s_p6_total. ((forall pa_i_hj32_local_total_h34s_p6_total_repeat. (exists pa_lt_hj32_local_total_h34s_p6_total_repeat_bound. pa_lt_hj32_local_total_h34s_p6_total_repeat_bound + S pa_i_hj32_local_total_h34s_p6_total_repeat = 4 * 35) -> (((exists pa_h_hj32_local_total_h34s_p6_total_repeat_decoded. pa_h_hj32_local_total_h34s_p6_total_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h34s_p6_total_repeat)) * pa_c_hj32_local_total_h34s_p6_total)) /\ exists pa_q_hj32_local_total_h34s_p6_total_repeat_decoded. pa_b_hj32_local_total_h34s_p6_total = pa_q_hj32_local_total_h34s_p6_total_repeat_decoded * S ((S (pa_i_hj32_local_total_h34s_p6_total_repeat)) * pa_c_hj32_local_total_h34s_p6_total) + (6)))) /\ (exists pa_u_hj32_local_total_h34s_p6_total_product pa_v_hj32_local_total_h34s_p6_total_product. ((((exists pa_h_hj32_local_total_h34s_p6_total_product_start. pa_h_hj32_local_total_h34s_p6_total_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h34s_p6_total_product)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_start. pa_u_hj32_local_total_h34s_p6_total_product = pa_q_hj32_local_total_h34s_p6_total_product_start * S ((S (0)) * pa_v_hj32_local_total_h34s_p6_total_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_total_product_terminal. pa_h_hj32_local_total_h34s_p6_total_product_terminal + S (hj32_local_value_h34s_p6_total) = S ((S (4 * 35)) * pa_v_hj32_local_total_h34s_p6_total_product)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_terminal. pa_u_hj32_local_total_h34s_p6_total_product = pa_q_hj32_local_total_h34s_p6_total_product_terminal * S ((S (4 * 35)) * pa_v_hj32_local_total_h34s_p6_total_product) + (hj32_local_value_h34s_p6_total))) /\ forall pa_i_hj32_local_total_h34s_p6_total_product. (exists pa_lt_hj32_local_total_h34s_p6_total_product_bound. pa_lt_hj32_local_total_h34s_p6_total_product_bound + S pa_i_hj32_local_total_h34s_p6_total_product = 4 * 35) -> exists pa_p_hj32_local_total_h34s_p6_total_product pa_r_hj32_local_total_h34s_p6_total_product pa_s_hj32_local_total_h34s_p6_total_product. ((((exists pa_h_hj32_local_total_h34s_p6_total_product_factor. pa_h_hj32_local_total_h34s_p6_total_product_factor + S (pa_p_hj32_local_total_h34s_p6_total_product) = S ((S (pa_i_hj32_local_total_h34s_p6_total_product)) * pa_c_hj32_local_total_h34s_p6_total)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_factor. pa_b_hj32_local_total_h34s_p6_total = pa_q_hj32_local_total_h34s_p6_total_product_factor * S ((S (pa_i_hj32_local_total_h34s_p6_total_product)) * pa_c_hj32_local_total_h34s_p6_total) + (pa_p_hj32_local_total_h34s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_total_product_partial. pa_h_hj32_local_total_h34s_p6_total_product_partial + S (pa_r_hj32_local_total_h34s_p6_total_product) = S ((S (pa_i_hj32_local_total_h34s_p6_total_product)) * pa_v_hj32_local_total_h34s_p6_total_product)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_partial. pa_u_hj32_local_total_h34s_p6_total_product = pa_q_hj32_local_total_h34s_p6_total_product_partial * S ((S (pa_i_hj32_local_total_h34s_p6_total_product)) * pa_v_hj32_local_total_h34s_p6_total_product) + (pa_r_hj32_local_total_h34s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_total_product_successor. pa_h_hj32_local_total_h34s_p6_total_product_successor + S (pa_s_hj32_local_total_h34s_p6_total_product) = S ((S (S pa_i_hj32_local_total_h34s_p6_total_product)) * pa_v_hj32_local_total_h34s_p6_total_product)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_successor. pa_u_hj32_local_total_h34s_p6_total_product = pa_q_hj32_local_total_h34s_p6_total_product_successor * S ((S (S pa_i_hj32_local_total_h34s_p6_total_product)) * pa_v_hj32_local_total_h34s_p6_total_product) + (pa_s_hj32_local_total_h34s_p6_total_product))) /\ pa_s_hj32_local_total_h34s_p6_total_product = pa_r_hj32_local_total_h34s_p6_total_product * pa_p_hj32_local_total_h34s_p6_total_product)))))))) - 0039
specialize htotal 6 - 0040
specialize htotal 4 * 35 - 0041
exact htotal - 0042
cases h34s_p6_total - 0043
have h34s_conversion : x = x1 - 0044
specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total 35 - 0045
specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x - 0046
specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x1 - 0047
apply pow_thirty_six_double_block_eq_pow_six_four_block_from_total - 0048
exact htotal - 0049
exact h34s_p36_witness - 0050
exact h34s_p6_total_witness - 0051
rewrite h34s_conversion at h34s_to_36 - 0052
have h34s_p6_main : ∃ hj32_local_value_h34s_p6_main. Pow(6,10 · 14,hj32_local_value_h34s_p6_main)Exact native replay line
have h34s_p6_main : exists hj32_local_value_h34s_p6_main. (exists pa_b_hj32_local_total_h34s_p6_main pa_c_hj32_local_total_h34s_p6_main. ((forall pa_i_hj32_local_total_h34s_p6_main_repeat. (exists pa_lt_hj32_local_total_h34s_p6_main_repeat_bound. pa_lt_hj32_local_total_h34s_p6_main_repeat_bound + S pa_i_hj32_local_total_h34s_p6_main_repeat = 10 * 14) -> (((exists pa_h_hj32_local_total_h34s_p6_main_repeat_decoded. pa_h_hj32_local_total_h34s_p6_main_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h34s_p6_main_repeat)) * pa_c_hj32_local_total_h34s_p6_main)) /\ exists pa_q_hj32_local_total_h34s_p6_main_repeat_decoded. pa_b_hj32_local_total_h34s_p6_main = pa_q_hj32_local_total_h34s_p6_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h34s_p6_main_repeat)) * pa_c_hj32_local_total_h34s_p6_main) + (6)))) /\ (exists pa_u_hj32_local_total_h34s_p6_main_product pa_v_hj32_local_total_h34s_p6_main_product. ((((exists pa_h_hj32_local_total_h34s_p6_main_product_start. pa_h_hj32_local_total_h34s_p6_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h34s_p6_main_product)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_start. pa_u_hj32_local_total_h34s_p6_main_product = pa_q_hj32_local_total_h34s_p6_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h34s_p6_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_main_product_terminal. pa_h_hj32_local_total_h34s_p6_main_product_terminal + S (hj32_local_value_h34s_p6_main) = S ((S (10 * 14)) * pa_v_hj32_local_total_h34s_p6_main_product)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_terminal. pa_u_hj32_local_total_h34s_p6_main_product = pa_q_hj32_local_total_h34s_p6_main_product_terminal * S ((S (10 * 14)) * pa_v_hj32_local_total_h34s_p6_main_product) + (hj32_local_value_h34s_p6_main))) /\ forall pa_i_hj32_local_total_h34s_p6_main_product. (exists pa_lt_hj32_local_total_h34s_p6_main_product_bound. pa_lt_hj32_local_total_h34s_p6_main_product_bound + S pa_i_hj32_local_total_h34s_p6_main_product = 10 * 14) -> exists pa_p_hj32_local_total_h34s_p6_main_product pa_r_hj32_local_total_h34s_p6_main_product pa_s_hj32_local_total_h34s_p6_main_product. ((((exists pa_h_hj32_local_total_h34s_p6_main_product_factor. pa_h_hj32_local_total_h34s_p6_main_product_factor + S (pa_p_hj32_local_total_h34s_p6_main_product) = S ((S (pa_i_hj32_local_total_h34s_p6_main_product)) * pa_c_hj32_local_total_h34s_p6_main)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_factor. pa_b_hj32_local_total_h34s_p6_main = pa_q_hj32_local_total_h34s_p6_main_product_factor * S ((S (pa_i_hj32_local_total_h34s_p6_main_product)) * pa_c_hj32_local_total_h34s_p6_main) + (pa_p_hj32_local_total_h34s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_main_product_partial. pa_h_hj32_local_total_h34s_p6_main_product_partial + S (pa_r_hj32_local_total_h34s_p6_main_product) = S ((S (pa_i_hj32_local_total_h34s_p6_main_product)) * pa_v_hj32_local_total_h34s_p6_main_product)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_partial. pa_u_hj32_local_total_h34s_p6_main_product = pa_q_hj32_local_total_h34s_p6_main_product_partial * S ((S (pa_i_hj32_local_total_h34s_p6_main_product)) * pa_v_hj32_local_total_h34s_p6_main_product) + (pa_r_hj32_local_total_h34s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_main_product_successor. pa_h_hj32_local_total_h34s_p6_main_product_successor + S (pa_s_hj32_local_total_h34s_p6_main_product) = S ((S (S pa_i_hj32_local_total_h34s_p6_main_product)) * pa_v_hj32_local_total_h34s_p6_main_product)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_successor. pa_u_hj32_local_total_h34s_p6_main_product = pa_q_hj32_local_total_h34s_p6_main_product_successor * S ((S (S pa_i_hj32_local_total_h34s_p6_main_product)) * pa_v_hj32_local_total_h34s_p6_main_product) + (pa_s_hj32_local_total_h34s_p6_main_product))) /\ pa_s_hj32_local_total_h34s_p6_main_product = pa_r_hj32_local_total_h34s_p6_main_product * pa_p_hj32_local_total_h34s_p6_main_product)))))))) - 0053
specialize htotal 6 - 0054
specialize htotal 10 * 14 - 0055
exact htotal - 0056
cases h34s_p6_main - 0057
have h34s_p4_main : ∃ hj32_local_value_h34s_p4_main. Pow(4,13 · 14,hj32_local_value_h34s_p4_main)Exact native replay line
have h34s_p4_main : exists hj32_local_value_h34s_p4_main. (exists pa_b_hj32_local_total_h34s_p4_main pa_c_hj32_local_total_h34s_p4_main. ((forall pa_i_hj32_local_total_h34s_p4_main_repeat. (exists pa_lt_hj32_local_total_h34s_p4_main_repeat_bound. pa_lt_hj32_local_total_h34s_p4_main_repeat_bound + S pa_i_hj32_local_total_h34s_p4_main_repeat = 13 * 14) -> (((exists pa_h_hj32_local_total_h34s_p4_main_repeat_decoded. pa_h_hj32_local_total_h34s_p4_main_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h34s_p4_main_repeat)) * pa_c_hj32_local_total_h34s_p4_main)) /\ exists pa_q_hj32_local_total_h34s_p4_main_repeat_decoded. pa_b_hj32_local_total_h34s_p4_main = pa_q_hj32_local_total_h34s_p4_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h34s_p4_main_repeat)) * pa_c_hj32_local_total_h34s_p4_main) + (4)))) /\ (exists pa_u_hj32_local_total_h34s_p4_main_product pa_v_hj32_local_total_h34s_p4_main_product. ((((exists pa_h_hj32_local_total_h34s_p4_main_product_start. pa_h_hj32_local_total_h34s_p4_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h34s_p4_main_product)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_start. pa_u_hj32_local_total_h34s_p4_main_product = pa_q_hj32_local_total_h34s_p4_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h34s_p4_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h34s_p4_main_product_terminal. pa_h_hj32_local_total_h34s_p4_main_product_terminal + S (hj32_local_value_h34s_p4_main) = S ((S (13 * 14)) * pa_v_hj32_local_total_h34s_p4_main_product)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_terminal. pa_u_hj32_local_total_h34s_p4_main_product = pa_q_hj32_local_total_h34s_p4_main_product_terminal * S ((S (13 * 14)) * pa_v_hj32_local_total_h34s_p4_main_product) + (hj32_local_value_h34s_p4_main))) /\ forall pa_i_hj32_local_total_h34s_p4_main_product. (exists pa_lt_hj32_local_total_h34s_p4_main_product_bound. pa_lt_hj32_local_total_h34s_p4_main_product_bound + S pa_i_hj32_local_total_h34s_p4_main_product = 13 * 14) -> exists pa_p_hj32_local_total_h34s_p4_main_product pa_r_hj32_local_total_h34s_p4_main_product pa_s_hj32_local_total_h34s_p4_main_product. ((((exists pa_h_hj32_local_total_h34s_p4_main_product_factor. pa_h_hj32_local_total_h34s_p4_main_product_factor + S (pa_p_hj32_local_total_h34s_p4_main_product) = S ((S (pa_i_hj32_local_total_h34s_p4_main_product)) * pa_c_hj32_local_total_h34s_p4_main)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_factor. pa_b_hj32_local_total_h34s_p4_main = pa_q_hj32_local_total_h34s_p4_main_product_factor * S ((S (pa_i_hj32_local_total_h34s_p4_main_product)) * pa_c_hj32_local_total_h34s_p4_main) + (pa_p_hj32_local_total_h34s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p4_main_product_partial. pa_h_hj32_local_total_h34s_p4_main_product_partial + S (pa_r_hj32_local_total_h34s_p4_main_product) = S ((S (pa_i_hj32_local_total_h34s_p4_main_product)) * pa_v_hj32_local_total_h34s_p4_main_product)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_partial. pa_u_hj32_local_total_h34s_p4_main_product = pa_q_hj32_local_total_h34s_p4_main_product_partial * S ((S (pa_i_hj32_local_total_h34s_p4_main_product)) * pa_v_hj32_local_total_h34s_p4_main_product) + (pa_r_hj32_local_total_h34s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p4_main_product_successor. pa_h_hj32_local_total_h34s_p4_main_product_successor + S (pa_s_hj32_local_total_h34s_p4_main_product) = S ((S (S pa_i_hj32_local_total_h34s_p4_main_product)) * pa_v_hj32_local_total_h34s_p4_main_product)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_successor. pa_u_hj32_local_total_h34s_p4_main_product = pa_q_hj32_local_total_h34s_p4_main_product_successor * S ((S (S pa_i_hj32_local_total_h34s_p4_main_product)) * pa_v_hj32_local_total_h34s_p4_main_product) + (pa_s_hj32_local_total_h34s_p4_main_product))) /\ pa_s_hj32_local_total_h34s_p4_main_product = pa_r_hj32_local_total_h34s_p4_main_product * pa_p_hj32_local_total_h34s_p4_main_product)))))))) - 0058
specialize htotal 4 - 0059
specialize htotal 13 * 14 - 0060
exact htotal - 0061
cases h34s_p4_main - 0062
have h34s_main_bound : Le(x2,x3)Exact native replay line
have h34s_main_bound : exists bqb_le_gap_hj32_h34s_main_bound. bqb_le_gap_hj32_h34s_main_bound + (x2) = (x3) - 0063
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 14 - 0064
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x2 - 0065
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x3 - 0066
apply pow_six_ten_block_le_pow_four_thirteen_block_from_total - 0067
exact htotal - 0068
exact h34s_p6_main_witness - 0069
exact h34s_p4_main_witness - 0070
have h34s_exponent : 4 * 35 = 10 * 14 - 0071
have h34s_thirty_five : 35 = 5 * 7 - 0072
norm_num - 0073
rewrite h34s_thirty_five - 0074
have h34s_left_assoc : 4 * (5 * 7) = (4 * 5) * 7 - 0075
symm - 0076
specialize mul_assoc 4 - 0077
specialize mul_assoc 5 - 0078
specialize mul_assoc 7 - 0079
apply mul_assoc - 0080
rewrite h34s_left_assoc - 0081
have h34s_fourteen : 14 = 2 * 7 - 0082
norm_num - 0083
rewrite h34s_fourteen - 0084
have h34s_right_assoc : 10 * (2 * 7) = (10 * 2) * 7 - 0085
symm - 0086
specialize mul_assoc 10 - 0087
specialize mul_assoc 2 - 0088
specialize mul_assoc 7 - 0089
apply mul_assoc - 0090
rewrite h34s_right_assoc - 0091
have h34s_right_twenty : 10 * 2 = 20 - 0092
norm_num - 0093
rewrite h34s_right_twenty - 0094
have h34s_left_twenty : 4 * 5 = 20 - 0095
norm_num - 0096
rewrite h34s_left_twenty - 0097
refl - 0098
have h34s_main_power : Pow(6,10 · 14,x1)Exact native replay line
have h34s_main_power : exists pa_b_hj32_h34s_main_power pa_c_hj32_h34s_main_power. ((forall pa_i_hj32_h34s_main_power_repeat. (exists pa_lt_hj32_h34s_main_power_repeat_bound. pa_lt_hj32_h34s_main_power_repeat_bound + S pa_i_hj32_h34s_main_power_repeat = 10 * 14) -> (((exists pa_h_hj32_h34s_main_power_repeat_decoded. pa_h_hj32_h34s_main_power_repeat_decoded + S (6) = S ((S (pa_i_hj32_h34s_main_power_repeat)) * pa_c_hj32_h34s_main_power)) /\ exists pa_q_hj32_h34s_main_power_repeat_decoded. pa_b_hj32_h34s_main_power = pa_q_hj32_h34s_main_power_repeat_decoded * S ((S (pa_i_hj32_h34s_main_power_repeat)) * pa_c_hj32_h34s_main_power) + (6)))) /\ (exists pa_u_hj32_h34s_main_power_product pa_v_hj32_h34s_main_power_product. ((((exists pa_h_hj32_h34s_main_power_product_start. pa_h_hj32_h34s_main_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_h34s_main_power_product)) /\ exists pa_q_hj32_h34s_main_power_product_start. pa_u_hj32_h34s_main_power_product = pa_q_hj32_h34s_main_power_product_start * S ((S (0)) * pa_v_hj32_h34s_main_power_product) + (1))) /\ ((((exists pa_h_hj32_h34s_main_power_product_terminal. pa_h_hj32_h34s_main_power_product_terminal + S (x1) = S ((S (10 * 14)) * pa_v_hj32_h34s_main_power_product)) /\ exists pa_q_hj32_h34s_main_power_product_terminal. pa_u_hj32_h34s_main_power_product = pa_q_hj32_h34s_main_power_product_terminal * S ((S (10 * 14)) * pa_v_hj32_h34s_main_power_product) + (x1))) /\ forall pa_i_hj32_h34s_main_power_product. (exists pa_lt_hj32_h34s_main_power_product_bound. pa_lt_hj32_h34s_main_power_product_bound + S pa_i_hj32_h34s_main_power_product = 10 * 14) -> exists pa_p_hj32_h34s_main_power_product pa_r_hj32_h34s_main_power_product pa_s_hj32_h34s_main_power_product. ((((exists pa_h_hj32_h34s_main_power_product_factor. pa_h_hj32_h34s_main_power_product_factor + S (pa_p_hj32_h34s_main_power_product) = S ((S (pa_i_hj32_h34s_main_power_product)) * pa_c_hj32_h34s_main_power)) /\ exists pa_q_hj32_h34s_main_power_product_factor. pa_b_hj32_h34s_main_power = pa_q_hj32_h34s_main_power_product_factor * S ((S (pa_i_hj32_h34s_main_power_product)) * pa_c_hj32_h34s_main_power) + (pa_p_hj32_h34s_main_power_product))) /\ ((((exists pa_h_hj32_h34s_main_power_product_partial. pa_h_hj32_h34s_main_power_product_partial + S (pa_r_hj32_h34s_main_power_product) = S ((S (pa_i_hj32_h34s_main_power_product)) * pa_v_hj32_h34s_main_power_product)) /\ exists pa_q_hj32_h34s_main_power_product_partial. pa_u_hj32_h34s_main_power_product = pa_q_hj32_h34s_main_power_product_partial * S ((S (pa_i_hj32_h34s_main_power_product)) * pa_v_hj32_h34s_main_power_product) + (pa_r_hj32_h34s_main_power_product))) /\ ((((exists pa_h_hj32_h34s_main_power_product_successor. pa_h_hj32_h34s_main_power_product_successor + S (pa_s_hj32_h34s_main_power_product) = S ((S (S pa_i_hj32_h34s_main_power_product)) * pa_v_hj32_h34s_main_power_product)) /\ exists pa_q_hj32_h34s_main_power_product_successor. pa_u_hj32_h34s_main_power_product = pa_q_hj32_h34s_main_power_product_successor * S ((S (S pa_i_hj32_h34s_main_power_product)) * pa_v_hj32_h34s_main_power_product) + (pa_s_hj32_h34s_main_power_product))) /\ pa_s_hj32_h34s_main_power_product = pa_r_hj32_h34s_main_power_product * pa_p_hj32_h34s_main_power_product))))))) - 0099
rewrite <- h34s_exponent - 0100
rewrite <- h34s_exponent - 0101
rewrite <- h34s_exponent - 0102
rewrite <- h34s_exponent - 0103
exact h34s_p6_total_witness - 0104
have h34s_direct_bound : Le(x1,x3)Exact native replay line
have h34s_direct_bound : exists bqb_le_gap_hj32_h34s_direct_bound. bqb_le_gap_hj32_h34s_direct_bound + (x1) = (x3) - 0105
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 14 - 0106
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x1 - 0107
specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x3 - 0108
apply pow_six_ten_block_le_pow_four_thirteen_block_from_total - 0109
exact htotal - 0110
exact h34s_main_power - 0111
exact h34s_p4_main_witness - 0112
have h34s_to_budget : Le(h,x3)Exact native replay line
have h34s_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h34s_to_budget. bqb_le_gap_hj32_local_trans_bound_h34s_to_budget + (h) = (x3) - 0113
specialize le_trans h - 0114
specialize le_trans x1 - 0115
specialize le_trans x3 - 0116
apply le_trans - 0117
exact h34s_to_36 - 0118
exact h34s_direct_bound - 0119
have hscaled : Le(6 · (13 · 14),34 · 34)Exact native replay line
have hscaled : exists bqb_le_gap_hj32_scaled_budget_root_34. bqb_le_gap_hj32_scaled_budget_root_34 + (6 * (13 * 14)) = (34 * 34) - 0120
apply bertrand_scaled_budget_root_34 - 0121
have hbudget_exponent : Le(13 · 14,e)Exact native replay line
have hbudget_exponent : exists bqb_le_gap_hj32_h_34_budget_exponent. bqb_le_gap_hj32_h_34_budget_exponent + (13 * 14) = (e) - 0122
specialize ceil_div_six_budget_of_scaled_le (34 * 34) - 0123
specialize ceil_div_six_budget_of_scaled_le (13 * 14) - 0124
specialize ceil_div_six_budget_of_scaled_le e - 0125
apply ceil_div_six_budget_of_scaled_le - 0126
exact hceiling - 0127
exact hscaled - 0128
have h34_budget_growth : Le(x3,u)Exact native replay line
have h34_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h34_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h34_budget_growth + (x3) = (u) - 0129
specialize pow_exponent_monotone_from_total 4 - 0130
specialize pow_exponent_monotone_from_total 13 * 14 - 0131
specialize pow_exponent_monotone_from_total e - 0132
specialize pow_exponent_monotone_from_total x3 - 0133
specialize pow_exponent_monotone_from_total u - 0134
apply pow_exponent_monotone_from_total - 0135
exact htotal - 0136
exists 3 - 0137
norm_num - 0138
exact hbudget_exponent - 0139
exact h34s_p4_main_witness - 0140
exact hu - 0141
have h34_result : Le(h,u)Exact native replay line
have h34_result : exists bqb_le_gap_hj32_local_trans_bound_h34_result. bqb_le_gap_hj32_local_trans_bound_h34_result + (h) = (u) - 0142
specialize le_trans h - 0143
specialize le_trans x3 - 0144
specialize le_trans u - 0145
apply le_trans - 0146
exact h34s_to_budget - 0147
exact h34_budget_growth - 0148
exact h34_result