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
∀ x. ∀ y. (∀ z. ∀ n. ∃ m. Pow(z,n,m)) → Pow(6,10,x) → Pow(4,13,y) → Le(x,y)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
4 occurrences
In local proof propositions
14 occurrences
Exact expanded native-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))Proof neighborhood
Direct theorem prerequisites
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 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–5
02Establish hthree_fiveL6–9
Establish this local claim before using it. It is not an additional assumption.
- L6
have hthree_five : ∃ q. Pow(3,5,q)Definitions: Pow(3,5,q)Original native command in the exact edition - L7
specialize htotal 3 - L8
specialize htotal 5 - L9
exact htotal
03Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
cases hthree_five
04Establish hfour_fourL11–14
Establish this local claim before using it. It is not an additional assumption.
- L11
have hfour_four : ∃ q. Pow(4,4,q)Definitions: Pow(4,4,q)Original native command in the exact edition - L12
specialize htotal 4 - L13
specialize htotal 4 - L14
exact htotal
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.
07Establish hthree_tenL23–26
Establish this local claim before using it. It is not an additional assumption.
- L23
have hthree_ten : ∃ q. Pow(3,10,q)Definitions: Pow(3,10,q)Original native command in the exact edition - L24
specialize htotal 3 - L25
specialize htotal 10 - L26
exact htotal
08Separate the logical casesL27–27
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L27
cases hthree_ten
09Establish hfour_eightL28–31
Establish this local claim before using it. It is not an additional assumption.
- L28
have hfour_eight : ∃ q. Pow(4,8,q)Definitions: Pow(4,8,q)Original native command in the exact edition - L29
specialize htotal 4 - L30
specialize htotal 8 - L31
exact htotal
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
Establish this local claim before using it. It is not an additional assumption.
- L33
have hthree_ten_block : Pow(3,5 · 2,x3)Definitions: Pow(3,5 · 2,x3)Original native command in the exact edition
12Establish hthree_ten_exponentL34–40
13Establish hfour_eight_blockL41–41
Establish this local claim before using it. It is not an additional assumption.
- L41
have hfour_eight_block : Pow(4,4 · 2,x4)Definitions: Pow(4,4 · 2,x4)Original native command in the exact edition
14Establish hfour_eight_exponentL42–48
15Establish hblockL49–58
Establish this local claim before using it. It is not an additional assumption.
- L49
- 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
Establish this local claim before using it. It is not an additional assumption.
- L66
have htwo_ten : ∃ q. Pow(2,10,q)Definitions: Pow(2,10,q)Original native command in the exact edition - L67
specialize htotal 2 - L68
specialize htotal 10 - L69
exact htotal
18Separate the logical casesL70–70
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L70
cases htwo_ten
19Establish hfour_fiveL71–74
Establish this local claim before using it. It is not an additional assumption.
- L71
have hfour_five : ∃ q. Pow(4,5,q)Definitions: Pow(4,5,q)Original native command in the exact edition - L72
specialize htotal 4 - L73
specialize htotal 5 - L74
exact htotal
20Separate the logical casesL75–75
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L75
cases hfour_five
21Establish hseedsL76–78
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two seed bundle from total.
- L76
have hseeds : Pow(2,2,4) ∧ Pow(2,7,128)Definitions: Pow(2,2,4)Pow(2,7,128)Original native command in the exact edition - L77
apply pow_two_seed_bundle_from_total - L78
exact htotal
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
Establish this local claim before using it. It is not an additional assumption.
- L94
have hxfactor : Pow(2 · 3,10,x)Definitions: Pow(2 · 3,10,x)Original native command in the exact edition
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 : Le(x5 · x3,x5 · x4)Definitions: Le(x5 · x3,x5 · x4)Original native command in the exact edition - 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 defined command ledger · 136 lines
- 0001
intro x - 0002
intro y - 0003
intro htotal - 0004
intro hx - 0005
intro hy - 0006
have hthree_five : ∃ q. Pow(3,5,q)Exact native replay line
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 : ∃ q. Pow(4,4,q)Exact native replay line
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 : Le(x1,x2)Exact native replay line
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 : ∃ q. Pow(3,10,q)Exact native replay line
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 : ∃ q. Pow(4,8,q)Exact native replay line
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 : Pow(3,5 · 2,x3)Exact native replay line
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 : Pow(4,4 · 2,x4)Exact native replay line
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 : Le(x3,x4)Exact native replay line
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 : ∃ q. Pow(2,10,q)Exact native replay line
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 : ∃ q. Pow(4,5,q)Exact native replay line
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 : Pow(2,2,4) ∧ Pow(2,7,128)Exact native replay line
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 : Pow(2 · 3,10,x)Exact native replay line
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 : Le(x5 · x3,x5 · x4)Exact native replay line
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