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.
Exact expanded PA statement
forall x y. (forall bpt_a_hj32_six_ten bpt_e_hj32_six_ten. exists bpt_x_hj32_six_ten. (exists ff_b_bpt_value_hj32_six_ten ff_c_bpt_value_hj32_six_ten. ((forall ff_i_bpt_value_hj32_six_ten_repeat. (exists ff_lt_bpt_value_hj32_six_ten_repeat_bound. ff_lt_bpt_value_hj32_six_ten_repeat_bound + S ff_i_bpt_value_hj32_six_ten_repeat = bpt_e_hj32_six_ten) -> (((exists ff_h_bpt_value_hj32_six_ten_repeat_decoded. ff_h_bpt_value_hj32_six_ten_repeat_decoded + S (bpt_a_hj32_six_ten) = S ((S (ff_i_bpt_value_hj32_six_ten_repeat)) * ff_c_bpt_value_hj32_six_ten)) /\ exists ff_q_bpt_value_hj32_six_ten_repeat_decoded. ff_b_bpt_value_hj32_six_ten = ff_q_bpt_value_hj32_six_ten_repeat_decoded * S ((S (ff_i_bpt_value_hj32_six_ten_repeat)) * ff_c_bpt_value_hj32_six_ten) + (bpt_a_hj32_six_ten)))) /\ (exists ff_u_bpt_value_hj32_six_ten_product ff_v_bpt_value_hj32_six_ten_product. ((((exists ff_h_bpt_value_hj32_six_ten_product_start. ff_h_bpt_value_hj32_six_ten_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_six_ten_product)) /\ exists ff_q_bpt_value_hj32_six_ten_product_start. ff_u_bpt_value_hj32_six_ten_product = ff_q_bpt_value_hj32_six_ten_product_start * S ((S (0)) * ff_v_bpt_value_hj32_six_ten_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_six_ten_product_terminal. ff_h_bpt_value_hj32_six_ten_product_terminal + S (bpt_x_hj32_six_ten) = S ((S (bpt_e_hj32_six_ten)) * ff_v_bpt_value_hj32_six_ten_product)) /\ exists ff_q_bpt_value_hj32_six_ten_product_terminal. ff_u_bpt_value_hj32_six_ten_product = ff_q_bpt_value_hj32_six_ten_product_terminal * S ((S (bpt_e_hj32_six_ten)) * ff_v_bpt_value_hj32_six_ten_product) + (bpt_x_hj32_six_ten))) /\ forall ff_i_bpt_value_hj32_six_ten_product. (exists ff_lt_bpt_value_hj32_six_ten_product_bound. ff_lt_bpt_value_hj32_six_ten_product_bound + S ff_i_bpt_value_hj32_six_ten_product = bpt_e_hj32_six_ten) -> exists ff_p_bpt_value_hj32_six_ten_product ff_r_bpt_value_hj32_six_ten_product ff_s_bpt_value_hj32_six_ten_product. ((((exists ff_h_bpt_value_hj32_six_ten_product_factor. ff_h_bpt_value_hj32_six_ten_product_factor + S (ff_p_bpt_value_hj32_six_ten_product) = S ((S (ff_i_bpt_value_hj32_six_ten_product)) * ff_c_bpt_value_hj32_six_ten)) /\ exists ff_q_bpt_value_hj32_six_ten_product_factor. ff_b_bpt_value_hj32_six_ten = ff_q_bpt_value_hj32_six_ten_product_factor * S ((S (ff_i_bpt_value_hj32_six_ten_product)) * ff_c_bpt_value_hj32_six_ten) + (ff_p_bpt_value_hj32_six_ten_product))) /\ ((((exists ff_h_bpt_value_hj32_six_ten_product_partial. ff_h_bpt_value_hj32_six_ten_product_partial + S (ff_r_bpt_value_hj32_six_ten_product) = S ((S (ff_i_bpt_value_hj32_six_ten_product)) * ff_v_bpt_value_hj32_six_ten_product)) /\ exists ff_q_bpt_value_hj32_six_ten_product_partial. ff_u_bpt_value_hj32_six_ten_product = ff_q_bpt_value_hj32_six_ten_product_partial * S ((S (ff_i_bpt_value_hj32_six_ten_product)) * ff_v_bpt_value_hj32_six_ten_product) + (ff_r_bpt_value_hj32_six_ten_product))) /\ ((((exists ff_h_bpt_value_hj32_six_ten_product_successor. ff_h_bpt_value_hj32_six_ten_product_successor + S (ff_s_bpt_value_hj32_six_ten_product) = S ((S (S ff_i_bpt_value_hj32_six_ten_product)) * ff_v_bpt_value_hj32_six_ten_product)) /\ exists ff_q_bpt_value_hj32_six_ten_product_successor. ff_u_bpt_value_hj32_six_ten_product = ff_q_bpt_value_hj32_six_ten_product_successor * S ((S (S ff_i_bpt_value_hj32_six_ten_product)) * ff_v_bpt_value_hj32_six_ten_product) + (ff_s_bpt_value_hj32_six_ten_product))) /\ ff_s_bpt_value_hj32_six_ten_product = ff_r_bpt_value_hj32_six_ten_product * ff_p_bpt_value_hj32_six_ten_product))))))))) -> (exists pa_b_hj32_six_ten_left pa_c_hj32_six_ten_left. ((forall pa_i_hj32_six_ten_left_repeat. (exists pa_lt_hj32_six_ten_left_repeat_bound. pa_lt_hj32_six_ten_left_repeat_bound + S pa_i_hj32_six_ten_left_repeat = 10) -> (((exists pa_h_hj32_six_ten_left_repeat_decoded. pa_h_hj32_six_ten_left_repeat_decoded + S (6) = S ((S (pa_i_hj32_six_ten_left_repeat)) * pa_c_hj32_six_ten_left)) /\ exists pa_q_hj32_six_ten_left_repeat_decoded. pa_b_hj32_six_ten_left = pa_q_hj32_six_ten_left_repeat_decoded * S ((S (pa_i_hj32_six_ten_left_repeat)) * pa_c_hj32_six_ten_left) + (6)))) /\ (exists pa_u_hj32_six_ten_left_product pa_v_hj32_six_ten_left_product. ((((exists pa_h_hj32_six_ten_left_product_start. pa_h_hj32_six_ten_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_six_ten_left_product)) /\ exists pa_q_hj32_six_ten_left_product_start. pa_u_hj32_six_ten_left_product = pa_q_hj32_six_ten_left_product_start * S ((S (0)) * pa_v_hj32_six_ten_left_product) + (1))) /\ ((((exists pa_h_hj32_six_ten_left_product_terminal. pa_h_hj32_six_ten_left_product_terminal + S (x) = S ((S (10)) * pa_v_hj32_six_ten_left_product)) /\ exists pa_q_hj32_six_ten_left_product_terminal. pa_u_hj32_six_ten_left_product = pa_q_hj32_six_ten_left_product_terminal * S ((S (10)) * pa_v_hj32_six_ten_left_product) + (x))) /\ forall pa_i_hj32_six_ten_left_product. (exists pa_lt_hj32_six_ten_left_product_bound. pa_lt_hj32_six_ten_left_product_bound + S pa_i_hj32_six_ten_left_product = 10) -> exists pa_p_hj32_six_ten_left_product pa_r_hj32_six_ten_left_product pa_s_hj32_six_ten_left_product. ((((exists pa_h_hj32_six_ten_left_product_factor. pa_h_hj32_six_ten_left_product_factor + S (pa_p_hj32_six_ten_left_product) = S ((S (pa_i_hj32_six_ten_left_product)) * pa_c_hj32_six_ten_left)) /\ exists pa_q_hj32_six_ten_left_product_factor. pa_b_hj32_six_ten_left = pa_q_hj32_six_ten_left_product_factor * S ((S (pa_i_hj32_six_ten_left_product)) * pa_c_hj32_six_ten_left) + (pa_p_hj32_six_ten_left_product))) /\ ((((exists pa_h_hj32_six_ten_left_product_partial. pa_h_hj32_six_ten_left_product_partial + S (pa_r_hj32_six_ten_left_product) = S ((S (pa_i_hj32_six_ten_left_product)) * pa_v_hj32_six_ten_left_product)) /\ exists pa_q_hj32_six_ten_left_product_partial. pa_u_hj32_six_ten_left_product = pa_q_hj32_six_ten_left_product_partial * S ((S (pa_i_hj32_six_ten_left_product)) * pa_v_hj32_six_ten_left_product) + (pa_r_hj32_six_ten_left_product))) /\ ((((exists pa_h_hj32_six_ten_left_product_successor. pa_h_hj32_six_ten_left_product_successor + S (pa_s_hj32_six_ten_left_product) = S ((S (S pa_i_hj32_six_ten_left_product)) * pa_v_hj32_six_ten_left_product)) /\ exists pa_q_hj32_six_ten_left_product_successor. pa_u_hj32_six_ten_left_product = pa_q_hj32_six_ten_left_product_successor * S ((S (S pa_i_hj32_six_ten_left_product)) * pa_v_hj32_six_ten_left_product) + (pa_s_hj32_six_ten_left_product))) /\ pa_s_hj32_six_ten_left_product = pa_r_hj32_six_ten_left_product * pa_p_hj32_six_ten_left_product)))))))) -> (exists pa_b_hj32_six_ten_right pa_c_hj32_six_ten_right. ((forall pa_i_hj32_six_ten_right_repeat. (exists pa_lt_hj32_six_ten_right_repeat_bound. pa_lt_hj32_six_ten_right_repeat_bound + S pa_i_hj32_six_ten_right_repeat = 13) -> (((exists pa_h_hj32_six_ten_right_repeat_decoded. pa_h_hj32_six_ten_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_six_ten_right_repeat)) * pa_c_hj32_six_ten_right)) /\ exists pa_q_hj32_six_ten_right_repeat_decoded. pa_b_hj32_six_ten_right = pa_q_hj32_six_ten_right_repeat_decoded * S ((S (pa_i_hj32_six_ten_right_repeat)) * pa_c_hj32_six_ten_right) + (4)))) /\ (exists pa_u_hj32_six_ten_right_product pa_v_hj32_six_ten_right_product. ((((exists pa_h_hj32_six_ten_right_product_start. pa_h_hj32_six_ten_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_six_ten_right_product)) /\ exists pa_q_hj32_six_ten_right_product_start. pa_u_hj32_six_ten_right_product = pa_q_hj32_six_ten_right_product_start * S ((S (0)) * pa_v_hj32_six_ten_right_product) + (1))) /\ ((((exists pa_h_hj32_six_ten_right_product_terminal. pa_h_hj32_six_ten_right_product_terminal + S (y) = S ((S (13)) * pa_v_hj32_six_ten_right_product)) /\ exists pa_q_hj32_six_ten_right_product_terminal. pa_u_hj32_six_ten_right_product = pa_q_hj32_six_ten_right_product_terminal * S ((S (13)) * pa_v_hj32_six_ten_right_product) + (y))) /\ forall pa_i_hj32_six_ten_right_product. (exists pa_lt_hj32_six_ten_right_product_bound. pa_lt_hj32_six_ten_right_product_bound + S pa_i_hj32_six_ten_right_product = 13) -> exists pa_p_hj32_six_ten_right_product pa_r_hj32_six_ten_right_product pa_s_hj32_six_ten_right_product. ((((exists pa_h_hj32_six_ten_right_product_factor. pa_h_hj32_six_ten_right_product_factor + S (pa_p_hj32_six_ten_right_product) = S ((S (pa_i_hj32_six_ten_right_product)) * pa_c_hj32_six_ten_right)) /\ exists pa_q_hj32_six_ten_right_product_factor. pa_b_hj32_six_ten_right = pa_q_hj32_six_ten_right_product_factor * S ((S (pa_i_hj32_six_ten_right_product)) * pa_c_hj32_six_ten_right) + (pa_p_hj32_six_ten_right_product))) /\ ((((exists pa_h_hj32_six_ten_right_product_partial. pa_h_hj32_six_ten_right_product_partial + S (pa_r_hj32_six_ten_right_product) = S ((S (pa_i_hj32_six_ten_right_product)) * pa_v_hj32_six_ten_right_product)) /\ exists pa_q_hj32_six_ten_right_product_partial. pa_u_hj32_six_ten_right_product = pa_q_hj32_six_ten_right_product_partial * S ((S (pa_i_hj32_six_ten_right_product)) * pa_v_hj32_six_ten_right_product) + (pa_r_hj32_six_ten_right_product))) /\ ((((exists pa_h_hj32_six_ten_right_product_successor. pa_h_hj32_six_ten_right_product_successor + S (pa_s_hj32_six_ten_right_product) = S ((S (S pa_i_hj32_six_ten_right_product)) * pa_v_hj32_six_ten_right_product)) /\ exists pa_q_hj32_six_ten_right_product_successor. pa_u_hj32_six_ten_right_product = pa_q_hj32_six_ten_right_product_successor * S ((S (S pa_i_hj32_six_ten_right_product)) * pa_v_hj32_six_ten_right_product) + (pa_s_hj32_six_ten_right_product))) /\ pa_s_hj32_six_ten_right_product = pa_r_hj32_six_ten_right_product * pa_p_hj32_six_ten_right_product)))))))) -> (exists bqb_le_gap_hj32_six_ten_result. bqb_le_gap_hj32_six_ten_result + (x) = (y))Structural proof guide
The block seed 6^10 <= 4^13 used by the finite H window.
Direct prerequisites: pow_block_bound_from_total, pow_three_five_le_pow_four_four_from_total, pow_two_seed_bundle_from_total, pow_mul_exp_from_total, pow_mul_base, pow_add, mul_le_mul, le_refl. The authored body proceeds by case analysis (7), intermediate claims (19), equality transport (13), closed numeral normalization (5).
Proof neighborhood
Direct dependencies
BT00W3 pow_block_bound_from_total BT00W4 pow_three_five_le_pow_four_four_from_total BT00SO pow_two_seed_bundle_from_total BT00SM pow_mul_exp_from_total BT00QV pow_mul_base BT009X pow_add BT00PV mul_le_mul BT000E le_reflDirect dependents
Formal native tactic body
Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.
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–5
02Establish hthree_fiveL6–9
03Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
cases hthree_five
04Establish hfour_fourL11–14
05Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
cases hfour_four
06Establish hseedL16–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow three five le pow four four from total.
- L16
have hseed : exists bqb_le_gap_hj32_row4_seed_bound. bqb_le_gap_hj32_row4_seed_bound + (x1) = (x2) - L17
specialize pow_three_five_le_pow_four_four_from_total x1 - L18
specialize pow_three_five_le_pow_four_four_from_total x2 - L19
apply pow_three_five_le_pow_four_four_from_total - L20
exact htotal - L21
exact hthree_five_witness - L22
exact hfour_four_witness
07Establish hthree_tenL23–26
08Separate the logical casesL27–27
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L27
cases hthree_ten
09Establish hfour_eightL28–31
10Separate the logical casesL32–32
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L32
cases hfour_eight
11Establish hthree_ten_blockL33–33
12Establish hthree_ten_exponentL34–40
13Establish hfour_eight_blockL41–41
14Establish hfour_eight_exponentL42–48
15Establish hblockL49–58
Establish this local claim before using it. It is not an additional assumption.
- L49
have hblock : exists bqb_le_gap_hj32_row4_block_bound. bqb_le_gap_hj32_row4_block_bound + (x3) = (x4) - L50
specialize pow_block_bound_from_total 3 - L51
specialize pow_block_bound_from_total 4 - L52
specialize pow_block_bound_from_total 5 - L53
specialize pow_block_bound_from_total 4 - L54
specialize pow_block_bound_from_total 2 - L55
specialize pow_block_bound_from_total x1 - L56
specialize pow_block_bound_from_total x2 - L57
specialize pow_block_bound_from_total x3 - L58
specialize pow_block_bound_from_total x4
16Use earlier factsL59–65
17Establish htwo_tenL66–69
18Separate the logical casesL70–70
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L70
cases htwo_ten
19Establish hfour_fiveL71–74
20Separate the logical casesL75–75
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L75
cases hfour_five
21Establish hseedsL76–78
22Separate the logical casesL79–79
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L79
cases hseeds
23Establish htwo_bridgeL80–89
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul exp from total.
- L80
have htwo_bridge : x6 = x5 - L81
specialize pow_mul_exp_from_total 2 - L82
specialize pow_mul_exp_from_total 2 - L83
specialize pow_mul_exp_from_total 5 - L84
specialize pow_mul_exp_from_total 10 - L85
specialize pow_mul_exp_from_total 4 - L86
specialize pow_mul_exp_from_total x6 - L87
specialize pow_mul_exp_from_total x5 - L88
apply pow_mul_exp_from_total - L89
exact htotal
24Calculate and transport equalitiesL90–90
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L90
norm_num
25Use earlier factsL91–93
26Establish hxfactorL94–94
27Establish hsixL95–99
28Establish hxproductL100–109
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul base.
29Use earlier factsL110–110
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L110
exact hxfactor
30Establish hyproductL111–120
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.
31Use earlier factsL121–123
32Calculate and transport equalitiesL124–124
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L124
rewrite htwo_bridge at hyproduct
33Establish hfactor_boundL125–134
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.
- L125
have hfactor_bound : exists bqb_le_gap_hj32_row4_product_bound. bqb_le_gap_hj32_row4_product_bound + (x5 * x3) = (x5 * x4) - L126
specialize mul_le_mul x5 - L127
specialize mul_le_mul x5 - L128
specialize mul_le_mul x3 - L129
specialize mul_le_mul x4 - L130
apply mul_le_mul - L131
specialize le_refl x5 - L132
exact le_refl - L133
exact hblock - L134
rewrite <- hxproduct at hfactor_bound
34Calculate and transport equalitiesL135–135
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L135
rewrite <- hyproduct at hfactor_bound
35Use earlier factsL136–136
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L136
exact hfactor_bound
Original exact command ledger · 136 lines
- 0001
intro x - 0002
intro y - 0003
intro htotal - 0004
intro hx - 0005
intro hy - 0006
have hthree_five : exists q. (exists pa_b_hj32_row4_three_five pa_c_hj32_row4_three_five. ((forall pa_i_hj32_row4_three_five_repeat. (exists pa_lt_hj32_row4_three_five_repeat_bound. pa_lt_hj32_row4_three_five_repeat_bound + S pa_i_hj32_row4_three_five_repeat = 5) -> (((exists pa_h_hj32_row4_three_five_repeat_decoded. pa_h_hj32_row4_three_five_repeat_decoded + S (3) = S ((S (pa_i_hj32_row4_three_five_repeat)) * pa_c_hj32_row4_three_five)) /\ exists pa_q_hj32_row4_three_five_repeat_decoded. pa_b_hj32_row4_three_five = pa_q_hj32_row4_three_five_repeat_decoded * S ((S (pa_i_hj32_row4_three_five_repeat)) * pa_c_hj32_row4_three_five) + (3)))) /\ (exists pa_u_hj32_row4_three_five_product pa_v_hj32_row4_three_five_product. ((((exists pa_h_hj32_row4_three_five_product_start. pa_h_hj32_row4_three_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_three_five_product)) /\ exists pa_q_hj32_row4_three_five_product_start. pa_u_hj32_row4_three_five_product = pa_q_hj32_row4_three_five_product_start * S ((S (0)) * pa_v_hj32_row4_three_five_product) + (1))) /\ ((((exists pa_h_hj32_row4_three_five_product_terminal. pa_h_hj32_row4_three_five_product_terminal + S (q) = S ((S (5)) * pa_v_hj32_row4_three_five_product)) /\ exists pa_q_hj32_row4_three_five_product_terminal. pa_u_hj32_row4_three_five_product = pa_q_hj32_row4_three_five_product_terminal * S ((S (5)) * pa_v_hj32_row4_three_five_product) + (q))) /\ forall pa_i_hj32_row4_three_five_product. (exists pa_lt_hj32_row4_three_five_product_bound. pa_lt_hj32_row4_three_five_product_bound + S pa_i_hj32_row4_three_five_product = 5) -> exists pa_p_hj32_row4_three_five_product pa_r_hj32_row4_three_five_product pa_s_hj32_row4_three_five_product. ((((exists pa_h_hj32_row4_three_five_product_factor. pa_h_hj32_row4_three_five_product_factor + S (pa_p_hj32_row4_three_five_product) = S ((S (pa_i_hj32_row4_three_five_product)) * pa_c_hj32_row4_three_five)) /\ exists pa_q_hj32_row4_three_five_product_factor. pa_b_hj32_row4_three_five = pa_q_hj32_row4_three_five_product_factor * S ((S (pa_i_hj32_row4_three_five_product)) * pa_c_hj32_row4_three_five) + (pa_p_hj32_row4_three_five_product))) /\ ((((exists pa_h_hj32_row4_three_five_product_partial. pa_h_hj32_row4_three_five_product_partial + S (pa_r_hj32_row4_three_five_product) = S ((S (pa_i_hj32_row4_three_five_product)) * pa_v_hj32_row4_three_five_product)) /\ exists pa_q_hj32_row4_three_five_product_partial. pa_u_hj32_row4_three_five_product = pa_q_hj32_row4_three_five_product_partial * S ((S (pa_i_hj32_row4_three_five_product)) * pa_v_hj32_row4_three_five_product) + (pa_r_hj32_row4_three_five_product))) /\ ((((exists pa_h_hj32_row4_three_five_product_successor. pa_h_hj32_row4_three_five_product_successor + S (pa_s_hj32_row4_three_five_product) = S ((S (S pa_i_hj32_row4_three_five_product)) * pa_v_hj32_row4_three_five_product)) /\ exists pa_q_hj32_row4_three_five_product_successor. pa_u_hj32_row4_three_five_product = pa_q_hj32_row4_three_five_product_successor * S ((S (S pa_i_hj32_row4_three_five_product)) * pa_v_hj32_row4_three_five_product) + (pa_s_hj32_row4_three_five_product))) /\ pa_s_hj32_row4_three_five_product = pa_r_hj32_row4_three_five_product * pa_p_hj32_row4_three_five_product)))))))) - 0007
specialize htotal 3 - 0008
specialize htotal 5 - 0009
exact htotal - 0010
cases hthree_five - 0011
have hfour_four : exists q. (exists pa_b_hj32_row4_four_four pa_c_hj32_row4_four_four. ((forall pa_i_hj32_row4_four_four_repeat. (exists pa_lt_hj32_row4_four_four_repeat_bound. pa_lt_hj32_row4_four_four_repeat_bound + S pa_i_hj32_row4_four_four_repeat = 4) -> (((exists pa_h_hj32_row4_four_four_repeat_decoded. pa_h_hj32_row4_four_four_repeat_decoded + S (4) = S ((S (pa_i_hj32_row4_four_four_repeat)) * pa_c_hj32_row4_four_four)) /\ exists pa_q_hj32_row4_four_four_repeat_decoded. pa_b_hj32_row4_four_four = pa_q_hj32_row4_four_four_repeat_decoded * S ((S (pa_i_hj32_row4_four_four_repeat)) * pa_c_hj32_row4_four_four) + (4)))) /\ (exists pa_u_hj32_row4_four_four_product pa_v_hj32_row4_four_four_product. ((((exists pa_h_hj32_row4_four_four_product_start. pa_h_hj32_row4_four_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_four_four_product)) /\ exists pa_q_hj32_row4_four_four_product_start. pa_u_hj32_row4_four_four_product = pa_q_hj32_row4_four_four_product_start * S ((S (0)) * pa_v_hj32_row4_four_four_product) + (1))) /\ ((((exists pa_h_hj32_row4_four_four_product_terminal. pa_h_hj32_row4_four_four_product_terminal + S (q) = S ((S (4)) * pa_v_hj32_row4_four_four_product)) /\ exists pa_q_hj32_row4_four_four_product_terminal. pa_u_hj32_row4_four_four_product = pa_q_hj32_row4_four_four_product_terminal * S ((S (4)) * pa_v_hj32_row4_four_four_product) + (q))) /\ forall pa_i_hj32_row4_four_four_product. (exists pa_lt_hj32_row4_four_four_product_bound. pa_lt_hj32_row4_four_four_product_bound + S pa_i_hj32_row4_four_four_product = 4) -> exists pa_p_hj32_row4_four_four_product pa_r_hj32_row4_four_four_product pa_s_hj32_row4_four_four_product. ((((exists pa_h_hj32_row4_four_four_product_factor. pa_h_hj32_row4_four_four_product_factor + S (pa_p_hj32_row4_four_four_product) = S ((S (pa_i_hj32_row4_four_four_product)) * pa_c_hj32_row4_four_four)) /\ exists pa_q_hj32_row4_four_four_product_factor. pa_b_hj32_row4_four_four = pa_q_hj32_row4_four_four_product_factor * S ((S (pa_i_hj32_row4_four_four_product)) * pa_c_hj32_row4_four_four) + (pa_p_hj32_row4_four_four_product))) /\ ((((exists pa_h_hj32_row4_four_four_product_partial. pa_h_hj32_row4_four_four_product_partial + S (pa_r_hj32_row4_four_four_product) = S ((S (pa_i_hj32_row4_four_four_product)) * pa_v_hj32_row4_four_four_product)) /\ exists pa_q_hj32_row4_four_four_product_partial. pa_u_hj32_row4_four_four_product = pa_q_hj32_row4_four_four_product_partial * S ((S (pa_i_hj32_row4_four_four_product)) * pa_v_hj32_row4_four_four_product) + (pa_r_hj32_row4_four_four_product))) /\ ((((exists pa_h_hj32_row4_four_four_product_successor. pa_h_hj32_row4_four_four_product_successor + S (pa_s_hj32_row4_four_four_product) = S ((S (S pa_i_hj32_row4_four_four_product)) * pa_v_hj32_row4_four_four_product)) /\ exists pa_q_hj32_row4_four_four_product_successor. pa_u_hj32_row4_four_four_product = pa_q_hj32_row4_four_four_product_successor * S ((S (S pa_i_hj32_row4_four_four_product)) * pa_v_hj32_row4_four_four_product) + (pa_s_hj32_row4_four_four_product))) /\ pa_s_hj32_row4_four_four_product = pa_r_hj32_row4_four_four_product * pa_p_hj32_row4_four_four_product)))))))) - 0012
specialize htotal 4 - 0013
specialize htotal 4 - 0014
exact htotal - 0015
cases hfour_four - 0016
have hseed : exists bqb_le_gap_hj32_row4_seed_bound. bqb_le_gap_hj32_row4_seed_bound + (x1) = (x2) - 0017
specialize pow_three_five_le_pow_four_four_from_total x1 - 0018
specialize pow_three_five_le_pow_four_four_from_total x2 - 0019
apply pow_three_five_le_pow_four_four_from_total - 0020
exact htotal - 0021
exact hthree_five_witness - 0022
exact hfour_four_witness - 0023
have hthree_ten : exists q. (exists pa_b_hj32_row4_three_ten pa_c_hj32_row4_three_ten. ((forall pa_i_hj32_row4_three_ten_repeat. (exists pa_lt_hj32_row4_three_ten_repeat_bound. pa_lt_hj32_row4_three_ten_repeat_bound + S pa_i_hj32_row4_three_ten_repeat = 10) -> (((exists pa_h_hj32_row4_three_ten_repeat_decoded. pa_h_hj32_row4_three_ten_repeat_decoded + S (3) = S ((S (pa_i_hj32_row4_three_ten_repeat)) * pa_c_hj32_row4_three_ten)) /\ exists pa_q_hj32_row4_three_ten_repeat_decoded. pa_b_hj32_row4_three_ten = pa_q_hj32_row4_three_ten_repeat_decoded * S ((S (pa_i_hj32_row4_three_ten_repeat)) * pa_c_hj32_row4_three_ten) + (3)))) /\ (exists pa_u_hj32_row4_three_ten_product pa_v_hj32_row4_three_ten_product. ((((exists pa_h_hj32_row4_three_ten_product_start. pa_h_hj32_row4_three_ten_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_three_ten_product)) /\ exists pa_q_hj32_row4_three_ten_product_start. pa_u_hj32_row4_three_ten_product = pa_q_hj32_row4_three_ten_product_start * S ((S (0)) * pa_v_hj32_row4_three_ten_product) + (1))) /\ ((((exists pa_h_hj32_row4_three_ten_product_terminal. pa_h_hj32_row4_three_ten_product_terminal + S (q) = S ((S (10)) * pa_v_hj32_row4_three_ten_product)) /\ exists pa_q_hj32_row4_three_ten_product_terminal. pa_u_hj32_row4_three_ten_product = pa_q_hj32_row4_three_ten_product_terminal * S ((S (10)) * pa_v_hj32_row4_three_ten_product) + (q))) /\ forall pa_i_hj32_row4_three_ten_product. (exists pa_lt_hj32_row4_three_ten_product_bound. pa_lt_hj32_row4_three_ten_product_bound + S pa_i_hj32_row4_three_ten_product = 10) -> exists pa_p_hj32_row4_three_ten_product pa_r_hj32_row4_three_ten_product pa_s_hj32_row4_three_ten_product. ((((exists pa_h_hj32_row4_three_ten_product_factor. pa_h_hj32_row4_three_ten_product_factor + S (pa_p_hj32_row4_three_ten_product) = S ((S (pa_i_hj32_row4_three_ten_product)) * pa_c_hj32_row4_three_ten)) /\ exists pa_q_hj32_row4_three_ten_product_factor. pa_b_hj32_row4_three_ten = pa_q_hj32_row4_three_ten_product_factor * S ((S (pa_i_hj32_row4_three_ten_product)) * pa_c_hj32_row4_three_ten) + (pa_p_hj32_row4_three_ten_product))) /\ ((((exists pa_h_hj32_row4_three_ten_product_partial. pa_h_hj32_row4_three_ten_product_partial + S (pa_r_hj32_row4_three_ten_product) = S ((S (pa_i_hj32_row4_three_ten_product)) * pa_v_hj32_row4_three_ten_product)) /\ exists pa_q_hj32_row4_three_ten_product_partial. pa_u_hj32_row4_three_ten_product = pa_q_hj32_row4_three_ten_product_partial * S ((S (pa_i_hj32_row4_three_ten_product)) * pa_v_hj32_row4_three_ten_product) + (pa_r_hj32_row4_three_ten_product))) /\ ((((exists pa_h_hj32_row4_three_ten_product_successor. pa_h_hj32_row4_three_ten_product_successor + S (pa_s_hj32_row4_three_ten_product) = S ((S (S pa_i_hj32_row4_three_ten_product)) * pa_v_hj32_row4_three_ten_product)) /\ exists pa_q_hj32_row4_three_ten_product_successor. pa_u_hj32_row4_three_ten_product = pa_q_hj32_row4_three_ten_product_successor * S ((S (S pa_i_hj32_row4_three_ten_product)) * pa_v_hj32_row4_three_ten_product) + (pa_s_hj32_row4_three_ten_product))) /\ pa_s_hj32_row4_three_ten_product = pa_r_hj32_row4_three_ten_product * pa_p_hj32_row4_three_ten_product)))))))) - 0024
specialize htotal 3 - 0025
specialize htotal 10 - 0026
exact htotal - 0027
cases hthree_ten - 0028
have hfour_eight : exists q. (exists pa_b_hj32_row4_four_eight pa_c_hj32_row4_four_eight. ((forall pa_i_hj32_row4_four_eight_repeat. (exists pa_lt_hj32_row4_four_eight_repeat_bound. pa_lt_hj32_row4_four_eight_repeat_bound + S pa_i_hj32_row4_four_eight_repeat = 8) -> (((exists pa_h_hj32_row4_four_eight_repeat_decoded. pa_h_hj32_row4_four_eight_repeat_decoded + S (4) = S ((S (pa_i_hj32_row4_four_eight_repeat)) * pa_c_hj32_row4_four_eight)) /\ exists pa_q_hj32_row4_four_eight_repeat_decoded. pa_b_hj32_row4_four_eight = pa_q_hj32_row4_four_eight_repeat_decoded * S ((S (pa_i_hj32_row4_four_eight_repeat)) * pa_c_hj32_row4_four_eight) + (4)))) /\ (exists pa_u_hj32_row4_four_eight_product pa_v_hj32_row4_four_eight_product. ((((exists pa_h_hj32_row4_four_eight_product_start. pa_h_hj32_row4_four_eight_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_four_eight_product)) /\ exists pa_q_hj32_row4_four_eight_product_start. pa_u_hj32_row4_four_eight_product = pa_q_hj32_row4_four_eight_product_start * S ((S (0)) * pa_v_hj32_row4_four_eight_product) + (1))) /\ ((((exists pa_h_hj32_row4_four_eight_product_terminal. pa_h_hj32_row4_four_eight_product_terminal + S (q) = S ((S (8)) * pa_v_hj32_row4_four_eight_product)) /\ exists pa_q_hj32_row4_four_eight_product_terminal. pa_u_hj32_row4_four_eight_product = pa_q_hj32_row4_four_eight_product_terminal * S ((S (8)) * pa_v_hj32_row4_four_eight_product) + (q))) /\ forall pa_i_hj32_row4_four_eight_product. (exists pa_lt_hj32_row4_four_eight_product_bound. pa_lt_hj32_row4_four_eight_product_bound + S pa_i_hj32_row4_four_eight_product = 8) -> exists pa_p_hj32_row4_four_eight_product pa_r_hj32_row4_four_eight_product pa_s_hj32_row4_four_eight_product. ((((exists pa_h_hj32_row4_four_eight_product_factor. pa_h_hj32_row4_four_eight_product_factor + S (pa_p_hj32_row4_four_eight_product) = S ((S (pa_i_hj32_row4_four_eight_product)) * pa_c_hj32_row4_four_eight)) /\ exists pa_q_hj32_row4_four_eight_product_factor. pa_b_hj32_row4_four_eight = pa_q_hj32_row4_four_eight_product_factor * S ((S (pa_i_hj32_row4_four_eight_product)) * pa_c_hj32_row4_four_eight) + (pa_p_hj32_row4_four_eight_product))) /\ ((((exists pa_h_hj32_row4_four_eight_product_partial. pa_h_hj32_row4_four_eight_product_partial + S (pa_r_hj32_row4_four_eight_product) = S ((S (pa_i_hj32_row4_four_eight_product)) * pa_v_hj32_row4_four_eight_product)) /\ exists pa_q_hj32_row4_four_eight_product_partial. pa_u_hj32_row4_four_eight_product = pa_q_hj32_row4_four_eight_product_partial * S ((S (pa_i_hj32_row4_four_eight_product)) * pa_v_hj32_row4_four_eight_product) + (pa_r_hj32_row4_four_eight_product))) /\ ((((exists pa_h_hj32_row4_four_eight_product_successor. pa_h_hj32_row4_four_eight_product_successor + S (pa_s_hj32_row4_four_eight_product) = S ((S (S pa_i_hj32_row4_four_eight_product)) * pa_v_hj32_row4_four_eight_product)) /\ exists pa_q_hj32_row4_four_eight_product_successor. pa_u_hj32_row4_four_eight_product = pa_q_hj32_row4_four_eight_product_successor * S ((S (S pa_i_hj32_row4_four_eight_product)) * pa_v_hj32_row4_four_eight_product) + (pa_s_hj32_row4_four_eight_product))) /\ pa_s_hj32_row4_four_eight_product = pa_r_hj32_row4_four_eight_product * pa_p_hj32_row4_four_eight_product)))))))) - 0029
specialize htotal 4 - 0030
specialize htotal 8 - 0031
exact htotal - 0032
cases hfour_eight - 0033
have hthree_ten_block : exists pa_b_hj32_row4_three_ten_block pa_c_hj32_row4_three_ten_block. ((forall pa_i_hj32_row4_three_ten_block_repeat. (exists pa_lt_hj32_row4_three_ten_block_repeat_bound. pa_lt_hj32_row4_three_ten_block_repeat_bound + S pa_i_hj32_row4_three_ten_block_repeat = 5 * 2) -> (((exists pa_h_hj32_row4_three_ten_block_repeat_decoded. pa_h_hj32_row4_three_ten_block_repeat_decoded + S (3) = S ((S (pa_i_hj32_row4_three_ten_block_repeat)) * pa_c_hj32_row4_three_ten_block)) /\ exists pa_q_hj32_row4_three_ten_block_repeat_decoded. pa_b_hj32_row4_three_ten_block = pa_q_hj32_row4_three_ten_block_repeat_decoded * S ((S (pa_i_hj32_row4_three_ten_block_repeat)) * pa_c_hj32_row4_three_ten_block) + (3)))) /\ (exists pa_u_hj32_row4_three_ten_block_product pa_v_hj32_row4_three_ten_block_product. ((((exists pa_h_hj32_row4_three_ten_block_product_start. pa_h_hj32_row4_three_ten_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_three_ten_block_product)) /\ exists pa_q_hj32_row4_three_ten_block_product_start. pa_u_hj32_row4_three_ten_block_product = pa_q_hj32_row4_three_ten_block_product_start * S ((S (0)) * pa_v_hj32_row4_three_ten_block_product) + (1))) /\ ((((exists pa_h_hj32_row4_three_ten_block_product_terminal. pa_h_hj32_row4_three_ten_block_product_terminal + S (x3) = S ((S (5 * 2)) * pa_v_hj32_row4_three_ten_block_product)) /\ exists pa_q_hj32_row4_three_ten_block_product_terminal. pa_u_hj32_row4_three_ten_block_product = pa_q_hj32_row4_three_ten_block_product_terminal * S ((S (5 * 2)) * pa_v_hj32_row4_three_ten_block_product) + (x3))) /\ forall pa_i_hj32_row4_three_ten_block_product. (exists pa_lt_hj32_row4_three_ten_block_product_bound. pa_lt_hj32_row4_three_ten_block_product_bound + S pa_i_hj32_row4_three_ten_block_product = 5 * 2) -> exists pa_p_hj32_row4_three_ten_block_product pa_r_hj32_row4_three_ten_block_product pa_s_hj32_row4_three_ten_block_product. ((((exists pa_h_hj32_row4_three_ten_block_product_factor. pa_h_hj32_row4_three_ten_block_product_factor + S (pa_p_hj32_row4_three_ten_block_product) = S ((S (pa_i_hj32_row4_three_ten_block_product)) * pa_c_hj32_row4_three_ten_block)) /\ exists pa_q_hj32_row4_three_ten_block_product_factor. pa_b_hj32_row4_three_ten_block = pa_q_hj32_row4_three_ten_block_product_factor * S ((S (pa_i_hj32_row4_three_ten_block_product)) * pa_c_hj32_row4_three_ten_block) + (pa_p_hj32_row4_three_ten_block_product))) /\ ((((exists pa_h_hj32_row4_three_ten_block_product_partial. pa_h_hj32_row4_three_ten_block_product_partial + S (pa_r_hj32_row4_three_ten_block_product) = S ((S (pa_i_hj32_row4_three_ten_block_product)) * pa_v_hj32_row4_three_ten_block_product)) /\ exists pa_q_hj32_row4_three_ten_block_product_partial. pa_u_hj32_row4_three_ten_block_product = pa_q_hj32_row4_three_ten_block_product_partial * S ((S (pa_i_hj32_row4_three_ten_block_product)) * pa_v_hj32_row4_three_ten_block_product) + (pa_r_hj32_row4_three_ten_block_product))) /\ ((((exists pa_h_hj32_row4_three_ten_block_product_successor. pa_h_hj32_row4_three_ten_block_product_successor + S (pa_s_hj32_row4_three_ten_block_product) = S ((S (S pa_i_hj32_row4_three_ten_block_product)) * pa_v_hj32_row4_three_ten_block_product)) /\ exists pa_q_hj32_row4_three_ten_block_product_successor. pa_u_hj32_row4_three_ten_block_product = pa_q_hj32_row4_three_ten_block_product_successor * S ((S (S pa_i_hj32_row4_three_ten_block_product)) * pa_v_hj32_row4_three_ten_block_product) + (pa_s_hj32_row4_three_ten_block_product))) /\ pa_s_hj32_row4_three_ten_block_product = pa_r_hj32_row4_three_ten_block_product * pa_p_hj32_row4_three_ten_block_product))))))) - 0034
have hthree_ten_exponent : 5 * 2 = 10 - 0035
norm_num - 0036
rewrite hthree_ten_exponent - 0037
rewrite hthree_ten_exponent - 0038
rewrite hthree_ten_exponent - 0039
rewrite hthree_ten_exponent - 0040
exact hthree_ten_witness - 0041
have hfour_eight_block : exists pa_b_hj32_row4_four_eight_block pa_c_hj32_row4_four_eight_block. ((forall pa_i_hj32_row4_four_eight_block_repeat. (exists pa_lt_hj32_row4_four_eight_block_repeat_bound. pa_lt_hj32_row4_four_eight_block_repeat_bound + S pa_i_hj32_row4_four_eight_block_repeat = 4 * 2) -> (((exists pa_h_hj32_row4_four_eight_block_repeat_decoded. pa_h_hj32_row4_four_eight_block_repeat_decoded + S (4) = S ((S (pa_i_hj32_row4_four_eight_block_repeat)) * pa_c_hj32_row4_four_eight_block)) /\ exists pa_q_hj32_row4_four_eight_block_repeat_decoded. pa_b_hj32_row4_four_eight_block = pa_q_hj32_row4_four_eight_block_repeat_decoded * S ((S (pa_i_hj32_row4_four_eight_block_repeat)) * pa_c_hj32_row4_four_eight_block) + (4)))) /\ (exists pa_u_hj32_row4_four_eight_block_product pa_v_hj32_row4_four_eight_block_product. ((((exists pa_h_hj32_row4_four_eight_block_product_start. pa_h_hj32_row4_four_eight_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_four_eight_block_product)) /\ exists pa_q_hj32_row4_four_eight_block_product_start. pa_u_hj32_row4_four_eight_block_product = pa_q_hj32_row4_four_eight_block_product_start * S ((S (0)) * pa_v_hj32_row4_four_eight_block_product) + (1))) /\ ((((exists pa_h_hj32_row4_four_eight_block_product_terminal. pa_h_hj32_row4_four_eight_block_product_terminal + S (x4) = S ((S (4 * 2)) * pa_v_hj32_row4_four_eight_block_product)) /\ exists pa_q_hj32_row4_four_eight_block_product_terminal. pa_u_hj32_row4_four_eight_block_product = pa_q_hj32_row4_four_eight_block_product_terminal * S ((S (4 * 2)) * pa_v_hj32_row4_four_eight_block_product) + (x4))) /\ forall pa_i_hj32_row4_four_eight_block_product. (exists pa_lt_hj32_row4_four_eight_block_product_bound. pa_lt_hj32_row4_four_eight_block_product_bound + S pa_i_hj32_row4_four_eight_block_product = 4 * 2) -> exists pa_p_hj32_row4_four_eight_block_product pa_r_hj32_row4_four_eight_block_product pa_s_hj32_row4_four_eight_block_product. ((((exists pa_h_hj32_row4_four_eight_block_product_factor. pa_h_hj32_row4_four_eight_block_product_factor + S (pa_p_hj32_row4_four_eight_block_product) = S ((S (pa_i_hj32_row4_four_eight_block_product)) * pa_c_hj32_row4_four_eight_block)) /\ exists pa_q_hj32_row4_four_eight_block_product_factor. pa_b_hj32_row4_four_eight_block = pa_q_hj32_row4_four_eight_block_product_factor * S ((S (pa_i_hj32_row4_four_eight_block_product)) * pa_c_hj32_row4_four_eight_block) + (pa_p_hj32_row4_four_eight_block_product))) /\ ((((exists pa_h_hj32_row4_four_eight_block_product_partial. pa_h_hj32_row4_four_eight_block_product_partial + S (pa_r_hj32_row4_four_eight_block_product) = S ((S (pa_i_hj32_row4_four_eight_block_product)) * pa_v_hj32_row4_four_eight_block_product)) /\ exists pa_q_hj32_row4_four_eight_block_product_partial. pa_u_hj32_row4_four_eight_block_product = pa_q_hj32_row4_four_eight_block_product_partial * S ((S (pa_i_hj32_row4_four_eight_block_product)) * pa_v_hj32_row4_four_eight_block_product) + (pa_r_hj32_row4_four_eight_block_product))) /\ ((((exists pa_h_hj32_row4_four_eight_block_product_successor. pa_h_hj32_row4_four_eight_block_product_successor + S (pa_s_hj32_row4_four_eight_block_product) = S ((S (S pa_i_hj32_row4_four_eight_block_product)) * pa_v_hj32_row4_four_eight_block_product)) /\ exists pa_q_hj32_row4_four_eight_block_product_successor. pa_u_hj32_row4_four_eight_block_product = pa_q_hj32_row4_four_eight_block_product_successor * S ((S (S pa_i_hj32_row4_four_eight_block_product)) * pa_v_hj32_row4_four_eight_block_product) + (pa_s_hj32_row4_four_eight_block_product))) /\ pa_s_hj32_row4_four_eight_block_product = pa_r_hj32_row4_four_eight_block_product * pa_p_hj32_row4_four_eight_block_product))))))) - 0042
have hfour_eight_exponent : 4 * 2 = 8 - 0043
norm_num - 0044
rewrite hfour_eight_exponent - 0045
rewrite hfour_eight_exponent - 0046
rewrite hfour_eight_exponent - 0047
rewrite hfour_eight_exponent - 0048
exact hfour_eight_witness - 0049
have hblock : exists bqb_le_gap_hj32_row4_block_bound. bqb_le_gap_hj32_row4_block_bound + (x3) = (x4) - 0050
specialize pow_block_bound_from_total 3 - 0051
specialize pow_block_bound_from_total 4 - 0052
specialize pow_block_bound_from_total 5 - 0053
specialize pow_block_bound_from_total 4 - 0054
specialize pow_block_bound_from_total 2 - 0055
specialize pow_block_bound_from_total x1 - 0056
specialize pow_block_bound_from_total x2 - 0057
specialize pow_block_bound_from_total x3 - 0058
specialize pow_block_bound_from_total x4 - 0059
apply pow_block_bound_from_total - 0060
exact htotal - 0061
exact hthree_five_witness - 0062
exact hfour_four_witness - 0063
exact hseed - 0064
exact hthree_ten_block - 0065
exact hfour_eight_block - 0066
have htwo_ten : exists q. (exists pa_b_hj32_row4_two_ten pa_c_hj32_row4_two_ten. ((forall pa_i_hj32_row4_two_ten_repeat. (exists pa_lt_hj32_row4_two_ten_repeat_bound. pa_lt_hj32_row4_two_ten_repeat_bound + S pa_i_hj32_row4_two_ten_repeat = 10) -> (((exists pa_h_hj32_row4_two_ten_repeat_decoded. pa_h_hj32_row4_two_ten_repeat_decoded + S (2) = S ((S (pa_i_hj32_row4_two_ten_repeat)) * pa_c_hj32_row4_two_ten)) /\ exists pa_q_hj32_row4_two_ten_repeat_decoded. pa_b_hj32_row4_two_ten = pa_q_hj32_row4_two_ten_repeat_decoded * S ((S (pa_i_hj32_row4_two_ten_repeat)) * pa_c_hj32_row4_two_ten) + (2)))) /\ (exists pa_u_hj32_row4_two_ten_product pa_v_hj32_row4_two_ten_product. ((((exists pa_h_hj32_row4_two_ten_product_start. pa_h_hj32_row4_two_ten_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_two_ten_product)) /\ exists pa_q_hj32_row4_two_ten_product_start. pa_u_hj32_row4_two_ten_product = pa_q_hj32_row4_two_ten_product_start * S ((S (0)) * pa_v_hj32_row4_two_ten_product) + (1))) /\ ((((exists pa_h_hj32_row4_two_ten_product_terminal. pa_h_hj32_row4_two_ten_product_terminal + S (q) = S ((S (10)) * pa_v_hj32_row4_two_ten_product)) /\ exists pa_q_hj32_row4_two_ten_product_terminal. pa_u_hj32_row4_two_ten_product = pa_q_hj32_row4_two_ten_product_terminal * S ((S (10)) * pa_v_hj32_row4_two_ten_product) + (q))) /\ forall pa_i_hj32_row4_two_ten_product. (exists pa_lt_hj32_row4_two_ten_product_bound. pa_lt_hj32_row4_two_ten_product_bound + S pa_i_hj32_row4_two_ten_product = 10) -> exists pa_p_hj32_row4_two_ten_product pa_r_hj32_row4_two_ten_product pa_s_hj32_row4_two_ten_product. ((((exists pa_h_hj32_row4_two_ten_product_factor. pa_h_hj32_row4_two_ten_product_factor + S (pa_p_hj32_row4_two_ten_product) = S ((S (pa_i_hj32_row4_two_ten_product)) * pa_c_hj32_row4_two_ten)) /\ exists pa_q_hj32_row4_two_ten_product_factor. pa_b_hj32_row4_two_ten = pa_q_hj32_row4_two_ten_product_factor * S ((S (pa_i_hj32_row4_two_ten_product)) * pa_c_hj32_row4_two_ten) + (pa_p_hj32_row4_two_ten_product))) /\ ((((exists pa_h_hj32_row4_two_ten_product_partial. pa_h_hj32_row4_two_ten_product_partial + S (pa_r_hj32_row4_two_ten_product) = S ((S (pa_i_hj32_row4_two_ten_product)) * pa_v_hj32_row4_two_ten_product)) /\ exists pa_q_hj32_row4_two_ten_product_partial. pa_u_hj32_row4_two_ten_product = pa_q_hj32_row4_two_ten_product_partial * S ((S (pa_i_hj32_row4_two_ten_product)) * pa_v_hj32_row4_two_ten_product) + (pa_r_hj32_row4_two_ten_product))) /\ ((((exists pa_h_hj32_row4_two_ten_product_successor. pa_h_hj32_row4_two_ten_product_successor + S (pa_s_hj32_row4_two_ten_product) = S ((S (S pa_i_hj32_row4_two_ten_product)) * pa_v_hj32_row4_two_ten_product)) /\ exists pa_q_hj32_row4_two_ten_product_successor. pa_u_hj32_row4_two_ten_product = pa_q_hj32_row4_two_ten_product_successor * S ((S (S pa_i_hj32_row4_two_ten_product)) * pa_v_hj32_row4_two_ten_product) + (pa_s_hj32_row4_two_ten_product))) /\ pa_s_hj32_row4_two_ten_product = pa_r_hj32_row4_two_ten_product * pa_p_hj32_row4_two_ten_product)))))))) - 0067
specialize htotal 2 - 0068
specialize htotal 10 - 0069
exact htotal - 0070
cases htwo_ten - 0071
have hfour_five : exists q. (exists pa_b_hj32_row4_four_five pa_c_hj32_row4_four_five. ((forall pa_i_hj32_row4_four_five_repeat. (exists pa_lt_hj32_row4_four_five_repeat_bound. pa_lt_hj32_row4_four_five_repeat_bound + S pa_i_hj32_row4_four_five_repeat = 5) -> (((exists pa_h_hj32_row4_four_five_repeat_decoded. pa_h_hj32_row4_four_five_repeat_decoded + S (4) = S ((S (pa_i_hj32_row4_four_five_repeat)) * pa_c_hj32_row4_four_five)) /\ exists pa_q_hj32_row4_four_five_repeat_decoded. pa_b_hj32_row4_four_five = pa_q_hj32_row4_four_five_repeat_decoded * S ((S (pa_i_hj32_row4_four_five_repeat)) * pa_c_hj32_row4_four_five) + (4)))) /\ (exists pa_u_hj32_row4_four_five_product pa_v_hj32_row4_four_five_product. ((((exists pa_h_hj32_row4_four_five_product_start. pa_h_hj32_row4_four_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_four_five_product)) /\ exists pa_q_hj32_row4_four_five_product_start. pa_u_hj32_row4_four_five_product = pa_q_hj32_row4_four_five_product_start * S ((S (0)) * pa_v_hj32_row4_four_five_product) + (1))) /\ ((((exists pa_h_hj32_row4_four_five_product_terminal. pa_h_hj32_row4_four_five_product_terminal + S (q) = S ((S (5)) * pa_v_hj32_row4_four_five_product)) /\ exists pa_q_hj32_row4_four_five_product_terminal. pa_u_hj32_row4_four_five_product = pa_q_hj32_row4_four_five_product_terminal * S ((S (5)) * pa_v_hj32_row4_four_five_product) + (q))) /\ forall pa_i_hj32_row4_four_five_product. (exists pa_lt_hj32_row4_four_five_product_bound. pa_lt_hj32_row4_four_five_product_bound + S pa_i_hj32_row4_four_five_product = 5) -> exists pa_p_hj32_row4_four_five_product pa_r_hj32_row4_four_five_product pa_s_hj32_row4_four_five_product. ((((exists pa_h_hj32_row4_four_five_product_factor. pa_h_hj32_row4_four_five_product_factor + S (pa_p_hj32_row4_four_five_product) = S ((S (pa_i_hj32_row4_four_five_product)) * pa_c_hj32_row4_four_five)) /\ exists pa_q_hj32_row4_four_five_product_factor. pa_b_hj32_row4_four_five = pa_q_hj32_row4_four_five_product_factor * S ((S (pa_i_hj32_row4_four_five_product)) * pa_c_hj32_row4_four_five) + (pa_p_hj32_row4_four_five_product))) /\ ((((exists pa_h_hj32_row4_four_five_product_partial. pa_h_hj32_row4_four_five_product_partial + S (pa_r_hj32_row4_four_five_product) = S ((S (pa_i_hj32_row4_four_five_product)) * pa_v_hj32_row4_four_five_product)) /\ exists pa_q_hj32_row4_four_five_product_partial. pa_u_hj32_row4_four_five_product = pa_q_hj32_row4_four_five_product_partial * S ((S (pa_i_hj32_row4_four_five_product)) * pa_v_hj32_row4_four_five_product) + (pa_r_hj32_row4_four_five_product))) /\ ((((exists pa_h_hj32_row4_four_five_product_successor. pa_h_hj32_row4_four_five_product_successor + S (pa_s_hj32_row4_four_five_product) = S ((S (S pa_i_hj32_row4_four_five_product)) * pa_v_hj32_row4_four_five_product)) /\ exists pa_q_hj32_row4_four_five_product_successor. pa_u_hj32_row4_four_five_product = pa_q_hj32_row4_four_five_product_successor * S ((S (S pa_i_hj32_row4_four_five_product)) * pa_v_hj32_row4_four_five_product) + (pa_s_hj32_row4_four_five_product))) /\ pa_s_hj32_row4_four_five_product = pa_r_hj32_row4_four_five_product * pa_p_hj32_row4_four_five_product)))))))) - 0072
specialize htotal 4 - 0073
specialize htotal 5 - 0074
exact htotal - 0075
cases hfour_five - 0076
have hseeds : (exists pa_b_hj32_seed_two_two pa_c_hj32_seed_two_two. ((forall pa_i_hj32_seed_two_two_repeat. (exists pa_lt_hj32_seed_two_two_repeat_bound. pa_lt_hj32_seed_two_two_repeat_bound + S pa_i_hj32_seed_two_two_repeat = 2) -> (((exists pa_h_hj32_seed_two_two_repeat_decoded. pa_h_hj32_seed_two_two_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_repeat_decoded. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_repeat_decoded * S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two) + (2)))) /\ (exists pa_u_hj32_seed_two_two_product pa_v_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_start. pa_h_hj32_seed_two_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_start. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_start * S ((S (0)) * pa_v_hj32_seed_two_two_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_two_product_terminal. pa_h_hj32_seed_two_two_product_terminal + S (4) = S ((S (2)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_terminal. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_terminal * S ((S (2)) * pa_v_hj32_seed_two_two_product) + (4))) /\ forall pa_i_hj32_seed_two_two_product. (exists pa_lt_hj32_seed_two_two_product_bound. pa_lt_hj32_seed_two_two_product_bound + S pa_i_hj32_seed_two_two_product = 2) -> exists pa_p_hj32_seed_two_two_product pa_r_hj32_seed_two_two_product pa_s_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_factor. pa_h_hj32_seed_two_two_product_factor + S (pa_p_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_product_factor. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_product_factor * S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two) + (pa_p_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_partial. pa_h_hj32_seed_two_two_product_partial + S (pa_r_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_partial. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_partial * S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_r_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_successor. pa_h_hj32_seed_two_two_product_successor + S (pa_s_hj32_seed_two_two_product) = S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_successor. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_successor * S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_s_hj32_seed_two_two_product))) /\ pa_s_hj32_seed_two_two_product = pa_r_hj32_seed_two_two_product * pa_p_hj32_seed_two_two_product)))))))) /\ (exists pa_b_hj32_seed_two_seven pa_c_hj32_seed_two_seven. ((forall pa_i_hj32_seed_two_seven_repeat. (exists pa_lt_hj32_seed_two_seven_repeat_bound. pa_lt_hj32_seed_two_seven_repeat_bound + S pa_i_hj32_seed_two_seven_repeat = 7) -> (((exists pa_h_hj32_seed_two_seven_repeat_decoded. pa_h_hj32_seed_two_seven_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_repeat_decoded. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_repeat_decoded * S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven) + (2)))) /\ (exists pa_u_hj32_seed_two_seven_product pa_v_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_start. pa_h_hj32_seed_two_seven_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_start. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_start * S ((S (0)) * pa_v_hj32_seed_two_seven_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_seven_product_terminal. pa_h_hj32_seed_two_seven_product_terminal + S (128) = S ((S (7)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_terminal. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_terminal * S ((S (7)) * pa_v_hj32_seed_two_seven_product) + (128))) /\ forall pa_i_hj32_seed_two_seven_product. (exists pa_lt_hj32_seed_two_seven_product_bound. pa_lt_hj32_seed_two_seven_product_bound + S pa_i_hj32_seed_two_seven_product = 7) -> exists pa_p_hj32_seed_two_seven_product pa_r_hj32_seed_two_seven_product pa_s_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_factor. pa_h_hj32_seed_two_seven_product_factor + S (pa_p_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_product_factor. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_product_factor * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven) + (pa_p_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_partial. pa_h_hj32_seed_two_seven_product_partial + S (pa_r_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_partial. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_partial * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_r_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_successor. pa_h_hj32_seed_two_seven_product_successor + S (pa_s_hj32_seed_two_seven_product) = S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_successor. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_successor * S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_s_hj32_seed_two_seven_product))) /\ pa_s_hj32_seed_two_seven_product = pa_r_hj32_seed_two_seven_product * pa_p_hj32_seed_two_seven_product)))))))) - 0077
apply pow_two_seed_bundle_from_total - 0078
exact htotal - 0079
cases hseeds - 0080
have htwo_bridge : x6 = x5 - 0081
specialize pow_mul_exp_from_total 2 - 0082
specialize pow_mul_exp_from_total 2 - 0083
specialize pow_mul_exp_from_total 5 - 0084
specialize pow_mul_exp_from_total 10 - 0085
specialize pow_mul_exp_from_total 4 - 0086
specialize pow_mul_exp_from_total x6 - 0087
specialize pow_mul_exp_from_total x5 - 0088
apply pow_mul_exp_from_total - 0089
exact htotal - 0090
norm_num - 0091
exact hseeds_left - 0092
exact hfour_five_witness - 0093
exact htwo_ten_witness - 0094
have hxfactor : exists pa_b_hj32_row4_six_factor pa_c_hj32_row4_six_factor. ((forall pa_i_hj32_row4_six_factor_repeat. (exists pa_lt_hj32_row4_six_factor_repeat_bound. pa_lt_hj32_row4_six_factor_repeat_bound + S pa_i_hj32_row4_six_factor_repeat = 10) -> (((exists pa_h_hj32_row4_six_factor_repeat_decoded. pa_h_hj32_row4_six_factor_repeat_decoded + S (2 * 3) = S ((S (pa_i_hj32_row4_six_factor_repeat)) * pa_c_hj32_row4_six_factor)) /\ exists pa_q_hj32_row4_six_factor_repeat_decoded. pa_b_hj32_row4_six_factor = pa_q_hj32_row4_six_factor_repeat_decoded * S ((S (pa_i_hj32_row4_six_factor_repeat)) * pa_c_hj32_row4_six_factor) + (2 * 3)))) /\ (exists pa_u_hj32_row4_six_factor_product pa_v_hj32_row4_six_factor_product. ((((exists pa_h_hj32_row4_six_factor_product_start. pa_h_hj32_row4_six_factor_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_six_factor_product)) /\ exists pa_q_hj32_row4_six_factor_product_start. pa_u_hj32_row4_six_factor_product = pa_q_hj32_row4_six_factor_product_start * S ((S (0)) * pa_v_hj32_row4_six_factor_product) + (1))) /\ ((((exists pa_h_hj32_row4_six_factor_product_terminal. pa_h_hj32_row4_six_factor_product_terminal + S (x) = S ((S (10)) * pa_v_hj32_row4_six_factor_product)) /\ exists pa_q_hj32_row4_six_factor_product_terminal. pa_u_hj32_row4_six_factor_product = pa_q_hj32_row4_six_factor_product_terminal * S ((S (10)) * pa_v_hj32_row4_six_factor_product) + (x))) /\ forall pa_i_hj32_row4_six_factor_product. (exists pa_lt_hj32_row4_six_factor_product_bound. pa_lt_hj32_row4_six_factor_product_bound + S pa_i_hj32_row4_six_factor_product = 10) -> exists pa_p_hj32_row4_six_factor_product pa_r_hj32_row4_six_factor_product pa_s_hj32_row4_six_factor_product. ((((exists pa_h_hj32_row4_six_factor_product_factor. pa_h_hj32_row4_six_factor_product_factor + S (pa_p_hj32_row4_six_factor_product) = S ((S (pa_i_hj32_row4_six_factor_product)) * pa_c_hj32_row4_six_factor)) /\ exists pa_q_hj32_row4_six_factor_product_factor. pa_b_hj32_row4_six_factor = pa_q_hj32_row4_six_factor_product_factor * S ((S (pa_i_hj32_row4_six_factor_product)) * pa_c_hj32_row4_six_factor) + (pa_p_hj32_row4_six_factor_product))) /\ ((((exists pa_h_hj32_row4_six_factor_product_partial. pa_h_hj32_row4_six_factor_product_partial + S (pa_r_hj32_row4_six_factor_product) = S ((S (pa_i_hj32_row4_six_factor_product)) * pa_v_hj32_row4_six_factor_product)) /\ exists pa_q_hj32_row4_six_factor_product_partial. pa_u_hj32_row4_six_factor_product = pa_q_hj32_row4_six_factor_product_partial * S ((S (pa_i_hj32_row4_six_factor_product)) * pa_v_hj32_row4_six_factor_product) + (pa_r_hj32_row4_six_factor_product))) /\ ((((exists pa_h_hj32_row4_six_factor_product_successor. pa_h_hj32_row4_six_factor_product_successor + S (pa_s_hj32_row4_six_factor_product) = S ((S (S pa_i_hj32_row4_six_factor_product)) * pa_v_hj32_row4_six_factor_product)) /\ exists pa_q_hj32_row4_six_factor_product_successor. pa_u_hj32_row4_six_factor_product = pa_q_hj32_row4_six_factor_product_successor * S ((S (S pa_i_hj32_row4_six_factor_product)) * pa_v_hj32_row4_six_factor_product) + (pa_s_hj32_row4_six_factor_product))) /\ pa_s_hj32_row4_six_factor_product = pa_r_hj32_row4_six_factor_product * pa_p_hj32_row4_six_factor_product))))))) - 0095
have hsix : 2 * 3 = 6 - 0096
norm_num - 0097
rewrite hsix - 0098
rewrite hsix - 0099
exact hx - 0100
have hxproduct : x = x5 * x3 - 0101
specialize pow_mul_base 2 - 0102
specialize pow_mul_base 3 - 0103
specialize pow_mul_base 10 - 0104
specialize pow_mul_base x5 - 0105
specialize pow_mul_base x3 - 0106
specialize pow_mul_base x - 0107
apply pow_mul_base - 0108
exact htwo_ten_witness - 0109
exact hthree_ten_witness - 0110
exact hxfactor - 0111
have hyproduct : y = x6 * x4 - 0112
specialize pow_add 4 - 0113
specialize pow_add 5 - 0114
specialize pow_add 8 - 0115
specialize pow_add 13 - 0116
specialize pow_add x6 - 0117
specialize pow_add x4 - 0118
specialize pow_add y - 0119
apply pow_add - 0120
norm_num - 0121
exact hfour_five_witness - 0122
exact hfour_eight_witness - 0123
exact hy - 0124
rewrite htwo_bridge at hyproduct - 0125
have hfactor_bound : exists bqb_le_gap_hj32_row4_product_bound. bqb_le_gap_hj32_row4_product_bound + (x5 * x3) = (x5 * x4) - 0126
specialize mul_le_mul x5 - 0127
specialize mul_le_mul x5 - 0128
specialize mul_le_mul x3 - 0129
specialize mul_le_mul x4 - 0130
apply mul_le_mul - 0131
specialize le_refl x5 - 0132
exact le_refl - 0133
exact hblock - 0134
rewrite <- hxproduct at hfactor_bound - 0135
rewrite <- hyproduct at hfactor_bound - 0136
exact hfactor_bound