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,6,x) → Pow(4,8,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
17 occurrences
Exact expanded native-PA statement
forall x y. (forall bpt_a_hj32_residual_six bpt_e_hj32_residual_six. exists bpt_x_hj32_residual_six. (exists ff_b_bpt_value_hj32_residual_six ff_c_bpt_value_hj32_residual_six. ((forall ff_i_bpt_value_hj32_residual_six_repeat. (exists ff_lt_bpt_value_hj32_residual_six_repeat_bound. ff_lt_bpt_value_hj32_residual_six_repeat_bound + S ff_i_bpt_value_hj32_residual_six_repeat = bpt_e_hj32_residual_six) -> (((exists ff_h_bpt_value_hj32_residual_six_repeat_decoded. ff_h_bpt_value_hj32_residual_six_repeat_decoded + S (bpt_a_hj32_residual_six) = S ((S (ff_i_bpt_value_hj32_residual_six_repeat)) * ff_c_bpt_value_hj32_residual_six)) /\ exists ff_q_bpt_value_hj32_residual_six_repeat_decoded. ff_b_bpt_value_hj32_residual_six = ff_q_bpt_value_hj32_residual_six_repeat_decoded * S ((S (ff_i_bpt_value_hj32_residual_six_repeat)) * ff_c_bpt_value_hj32_residual_six) + (bpt_a_hj32_residual_six)))) /\ (exists ff_u_bpt_value_hj32_residual_six_product ff_v_bpt_value_hj32_residual_six_product. ((((exists ff_h_bpt_value_hj32_residual_six_product_start. ff_h_bpt_value_hj32_residual_six_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_residual_six_product)) /\ exists ff_q_bpt_value_hj32_residual_six_product_start. ff_u_bpt_value_hj32_residual_six_product = ff_q_bpt_value_hj32_residual_six_product_start * S ((S (0)) * ff_v_bpt_value_hj32_residual_six_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_residual_six_product_terminal. ff_h_bpt_value_hj32_residual_six_product_terminal + S (bpt_x_hj32_residual_six) = S ((S (bpt_e_hj32_residual_six)) * ff_v_bpt_value_hj32_residual_six_product)) /\ exists ff_q_bpt_value_hj32_residual_six_product_terminal. ff_u_bpt_value_hj32_residual_six_product = ff_q_bpt_value_hj32_residual_six_product_terminal * S ((S (bpt_e_hj32_residual_six)) * ff_v_bpt_value_hj32_residual_six_product) + (bpt_x_hj32_residual_six))) /\ forall ff_i_bpt_value_hj32_residual_six_product. (exists ff_lt_bpt_value_hj32_residual_six_product_bound. ff_lt_bpt_value_hj32_residual_six_product_bound + S ff_i_bpt_value_hj32_residual_six_product = bpt_e_hj32_residual_six) -> exists ff_p_bpt_value_hj32_residual_six_product ff_r_bpt_value_hj32_residual_six_product ff_s_bpt_value_hj32_residual_six_product. ((((exists ff_h_bpt_value_hj32_residual_six_product_factor. ff_h_bpt_value_hj32_residual_six_product_factor + S (ff_p_bpt_value_hj32_residual_six_product) = S ((S (ff_i_bpt_value_hj32_residual_six_product)) * ff_c_bpt_value_hj32_residual_six)) /\ exists ff_q_bpt_value_hj32_residual_six_product_factor. ff_b_bpt_value_hj32_residual_six = ff_q_bpt_value_hj32_residual_six_product_factor * S ((S (ff_i_bpt_value_hj32_residual_six_product)) * ff_c_bpt_value_hj32_residual_six) + (ff_p_bpt_value_hj32_residual_six_product))) /\ ((((exists ff_h_bpt_value_hj32_residual_six_product_partial. ff_h_bpt_value_hj32_residual_six_product_partial + S (ff_r_bpt_value_hj32_residual_six_product) = S ((S (ff_i_bpt_value_hj32_residual_six_product)) * ff_v_bpt_value_hj32_residual_six_product)) /\ exists ff_q_bpt_value_hj32_residual_six_product_partial. ff_u_bpt_value_hj32_residual_six_product = ff_q_bpt_value_hj32_residual_six_product_partial * S ((S (ff_i_bpt_value_hj32_residual_six_product)) * ff_v_bpt_value_hj32_residual_six_product) + (ff_r_bpt_value_hj32_residual_six_product))) /\ ((((exists ff_h_bpt_value_hj32_residual_six_product_successor. ff_h_bpt_value_hj32_residual_six_product_successor + S (ff_s_bpt_value_hj32_residual_six_product) = S ((S (S ff_i_bpt_value_hj32_residual_six_product)) * ff_v_bpt_value_hj32_residual_six_product)) /\ exists ff_q_bpt_value_hj32_residual_six_product_successor. ff_u_bpt_value_hj32_residual_six_product = ff_q_bpt_value_hj32_residual_six_product_successor * S ((S (S ff_i_bpt_value_hj32_residual_six_product)) * ff_v_bpt_value_hj32_residual_six_product) + (ff_s_bpt_value_hj32_residual_six_product))) /\ ff_s_bpt_value_hj32_residual_six_product = ff_r_bpt_value_hj32_residual_six_product * ff_p_bpt_value_hj32_residual_six_product))))))))) -> (exists pa_b_hj32_residual_six_left pa_c_hj32_residual_six_left. ((forall pa_i_hj32_residual_six_left_repeat. (exists pa_lt_hj32_residual_six_left_repeat_bound. pa_lt_hj32_residual_six_left_repeat_bound + S pa_i_hj32_residual_six_left_repeat = 6) -> (((exists pa_h_hj32_residual_six_left_repeat_decoded. pa_h_hj32_residual_six_left_repeat_decoded + S (6) = S ((S (pa_i_hj32_residual_six_left_repeat)) * pa_c_hj32_residual_six_left)) /\ exists pa_q_hj32_residual_six_left_repeat_decoded. pa_b_hj32_residual_six_left = pa_q_hj32_residual_six_left_repeat_decoded * S ((S (pa_i_hj32_residual_six_left_repeat)) * pa_c_hj32_residual_six_left) + (6)))) /\ (exists pa_u_hj32_residual_six_left_product pa_v_hj32_residual_six_left_product. ((((exists pa_h_hj32_residual_six_left_product_start. pa_h_hj32_residual_six_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_residual_six_left_product)) /\ exists pa_q_hj32_residual_six_left_product_start. pa_u_hj32_residual_six_left_product = pa_q_hj32_residual_six_left_product_start * S ((S (0)) * pa_v_hj32_residual_six_left_product) + (1))) /\ ((((exists pa_h_hj32_residual_six_left_product_terminal. pa_h_hj32_residual_six_left_product_terminal + S (x) = S ((S (6)) * pa_v_hj32_residual_six_left_product)) /\ exists pa_q_hj32_residual_six_left_product_terminal. pa_u_hj32_residual_six_left_product = pa_q_hj32_residual_six_left_product_terminal * S ((S (6)) * pa_v_hj32_residual_six_left_product) + (x))) /\ forall pa_i_hj32_residual_six_left_product. (exists pa_lt_hj32_residual_six_left_product_bound. pa_lt_hj32_residual_six_left_product_bound + S pa_i_hj32_residual_six_left_product = 6) -> exists pa_p_hj32_residual_six_left_product pa_r_hj32_residual_six_left_product pa_s_hj32_residual_six_left_product. ((((exists pa_h_hj32_residual_six_left_product_factor. pa_h_hj32_residual_six_left_product_factor + S (pa_p_hj32_residual_six_left_product) = S ((S (pa_i_hj32_residual_six_left_product)) * pa_c_hj32_residual_six_left)) /\ exists pa_q_hj32_residual_six_left_product_factor. pa_b_hj32_residual_six_left = pa_q_hj32_residual_six_left_product_factor * S ((S (pa_i_hj32_residual_six_left_product)) * pa_c_hj32_residual_six_left) + (pa_p_hj32_residual_six_left_product))) /\ ((((exists pa_h_hj32_residual_six_left_product_partial. pa_h_hj32_residual_six_left_product_partial + S (pa_r_hj32_residual_six_left_product) = S ((S (pa_i_hj32_residual_six_left_product)) * pa_v_hj32_residual_six_left_product)) /\ exists pa_q_hj32_residual_six_left_product_partial. pa_u_hj32_residual_six_left_product = pa_q_hj32_residual_six_left_product_partial * S ((S (pa_i_hj32_residual_six_left_product)) * pa_v_hj32_residual_six_left_product) + (pa_r_hj32_residual_six_left_product))) /\ ((((exists pa_h_hj32_residual_six_left_product_successor. pa_h_hj32_residual_six_left_product_successor + S (pa_s_hj32_residual_six_left_product) = S ((S (S pa_i_hj32_residual_six_left_product)) * pa_v_hj32_residual_six_left_product)) /\ exists pa_q_hj32_residual_six_left_product_successor. pa_u_hj32_residual_six_left_product = pa_q_hj32_residual_six_left_product_successor * S ((S (S pa_i_hj32_residual_six_left_product)) * pa_v_hj32_residual_six_left_product) + (pa_s_hj32_residual_six_left_product))) /\ pa_s_hj32_residual_six_left_product = pa_r_hj32_residual_six_left_product * pa_p_hj32_residual_six_left_product)))))))) -> (exists pa_b_hj32_residual_six_right pa_c_hj32_residual_six_right. ((forall pa_i_hj32_residual_six_right_repeat. (exists pa_lt_hj32_residual_six_right_repeat_bound. pa_lt_hj32_residual_six_right_repeat_bound + S pa_i_hj32_residual_six_right_repeat = 8) -> (((exists pa_h_hj32_residual_six_right_repeat_decoded. pa_h_hj32_residual_six_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_residual_six_right_repeat)) * pa_c_hj32_residual_six_right)) /\ exists pa_q_hj32_residual_six_right_repeat_decoded. pa_b_hj32_residual_six_right = pa_q_hj32_residual_six_right_repeat_decoded * S ((S (pa_i_hj32_residual_six_right_repeat)) * pa_c_hj32_residual_six_right) + (4)))) /\ (exists pa_u_hj32_residual_six_right_product pa_v_hj32_residual_six_right_product. ((((exists pa_h_hj32_residual_six_right_product_start. pa_h_hj32_residual_six_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_residual_six_right_product)) /\ exists pa_q_hj32_residual_six_right_product_start. pa_u_hj32_residual_six_right_product = pa_q_hj32_residual_six_right_product_start * S ((S (0)) * pa_v_hj32_residual_six_right_product) + (1))) /\ ((((exists pa_h_hj32_residual_six_right_product_terminal. pa_h_hj32_residual_six_right_product_terminal + S (y) = S ((S (8)) * pa_v_hj32_residual_six_right_product)) /\ exists pa_q_hj32_residual_six_right_product_terminal. pa_u_hj32_residual_six_right_product = pa_q_hj32_residual_six_right_product_terminal * S ((S (8)) * pa_v_hj32_residual_six_right_product) + (y))) /\ forall pa_i_hj32_residual_six_right_product. (exists pa_lt_hj32_residual_six_right_product_bound. pa_lt_hj32_residual_six_right_product_bound + S pa_i_hj32_residual_six_right_product = 8) -> exists pa_p_hj32_residual_six_right_product pa_r_hj32_residual_six_right_product pa_s_hj32_residual_six_right_product. ((((exists pa_h_hj32_residual_six_right_product_factor. pa_h_hj32_residual_six_right_product_factor + S (pa_p_hj32_residual_six_right_product) = S ((S (pa_i_hj32_residual_six_right_product)) * pa_c_hj32_residual_six_right)) /\ exists pa_q_hj32_residual_six_right_product_factor. pa_b_hj32_residual_six_right = pa_q_hj32_residual_six_right_product_factor * S ((S (pa_i_hj32_residual_six_right_product)) * pa_c_hj32_residual_six_right) + (pa_p_hj32_residual_six_right_product))) /\ ((((exists pa_h_hj32_residual_six_right_product_partial. pa_h_hj32_residual_six_right_product_partial + S (pa_r_hj32_residual_six_right_product) = S ((S (pa_i_hj32_residual_six_right_product)) * pa_v_hj32_residual_six_right_product)) /\ exists pa_q_hj32_residual_six_right_product_partial. pa_u_hj32_residual_six_right_product = pa_q_hj32_residual_six_right_product_partial * S ((S (pa_i_hj32_residual_six_right_product)) * pa_v_hj32_residual_six_right_product) + (pa_r_hj32_residual_six_right_product))) /\ ((((exists pa_h_hj32_residual_six_right_product_successor. pa_h_hj32_residual_six_right_product_successor + S (pa_s_hj32_residual_six_right_product) = S ((S (S pa_i_hj32_residual_six_right_product)) * pa_v_hj32_residual_six_right_product)) /\ exists pa_q_hj32_residual_six_right_product_successor. pa_u_hj32_residual_six_right_product = pa_q_hj32_residual_six_right_product_successor * S ((S (S pa_i_hj32_residual_six_right_product)) * pa_v_hj32_residual_six_right_product) + (pa_s_hj32_residual_six_right_product))) /\ pa_s_hj32_residual_six_right_product = pa_r_hj32_residual_six_right_product * pa_p_hj32_residual_six_right_product)))))))) -> (exists bqb_le_gap_hj32_residual_six_result. bqb_le_gap_hj32_residual_six_result + (x) = (y))Proof neighborhood
Direct theorem prerequisites
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 BT00PY pow_base_monotone 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 rs_p3_fiveL6–9
Establish this local claim before using it. It is not an additional assumption.
- L6
have rs_p3_five : ∃ hj32_local_value_rs_p3_five. Pow(3,5,hj32_local_value_rs_p3_five)Definitions: Pow(3,5,hj32_local_value_rs_p3_five)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 rs_p3_five
04Establish rs_p4_fourL11–14
Establish this local claim before using it. It is not an additional assumption.
- L11
have rs_p4_four : ∃ hj32_local_value_rs_p4_four. Pow(4,4,hj32_local_value_rs_p4_four)Definitions: Pow(4,4,hj32_local_value_rs_p4_four)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 rs_p4_four
06Establish rs_seedL16–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 rs_p3_oneL23–26
Establish this local claim before using it. It is not an additional assumption.
- L23
have rs_p3_one : ∃ hj32_local_value_rs_p3_one. Pow(3,1,hj32_local_value_rs_p3_one)Definitions: Pow(3,1,hj32_local_value_rs_p3_one)Original native command in the exact edition - L24
specialize htotal 3 - L25
specialize htotal 1 - L26
exact htotal
08Separate the logical casesL27–27
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L27
cases rs_p3_one
09Establish rs_p4_oneL28–31
Establish this local claim before using it. It is not an additional assumption.
- L28
have rs_p4_one : ∃ hj32_local_value_rs_p4_one. Pow(4,1,hj32_local_value_rs_p4_one)Definitions: Pow(4,1,hj32_local_value_rs_p4_one)Original native command in the exact edition - L29
specialize htotal 4 - L30
specialize htotal 1 - L31
exact htotal
10Separate the logical casesL32–32
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L32
cases rs_p4_one
11Establish rs_baseL33–33
Establish this local claim before using it. It is not an additional assumption.
12Construct an explicit witnessL34–34
Supply the displayed value, then prove that it has the required property.
- L34
exists 1
13Calculate and transport equalitiesL35–35
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L35
norm_num
14Establish rs_one_boundL36–45
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow base monotone.
15Establish rs_p3_sixL46–49
Establish this local claim before using it. It is not an additional assumption.
- L46
have rs_p3_six : ∃ hj32_local_value_rs_p3_six. Pow(3,6,hj32_local_value_rs_p3_six)Definitions: Pow(3,6,hj32_local_value_rs_p3_six)Original native command in the exact edition - L47
specialize htotal 3 - L48
specialize htotal 6 - L49
exact htotal
16Separate the logical casesL50–50
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L50
cases rs_p3_six
17Establish rs_p4_fiveL51–54
Establish this local claim before using it. It is not an additional assumption.
- L51
have rs_p4_five : ∃ hj32_local_value_rs_p4_five. Pow(4,5,hj32_local_value_rs_p4_five)Definitions: Pow(4,5,hj32_local_value_rs_p4_five)Original native command in the exact edition - L52
specialize htotal 4 - L53
specialize htotal 5 - L54
exact htotal
18Separate the logical casesL55–55
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L55
cases rs_p4_five
19Establish rs_three_productL56–65
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.
20Use earlier factsL66–68
21Establish rs_four_productL69–78
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.
22Use earlier factsL79–81
23Establish rs_three_boundL82–91
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.
- L82
have rs_three_bound : Le(x1 · x3,x2 · x4)Definitions: Le(x1 · x3,x2 · x4)Original native command in the exact edition - L83
specialize mul_le_mul x1 - L84
specialize mul_le_mul x2 - L85
specialize mul_le_mul x3 - L86
specialize mul_le_mul x4 - L87
apply mul_le_mul - L88
exact rs_seed - L89
exact rs_one_bound - L90
rewrite <- rs_three_product at rs_three_bound - L91
rewrite <- rs_four_product at rs_three_bound
24Establish rs_seedsL92–94
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two seed bundle from total.
- L92
have rs_seeds : Pow(2,2,4) ∧ Pow(2,7,128)Definitions: Pow(2,2,4)Pow(2,7,128)Original native command in the exact edition - L93
apply pow_two_seed_bundle_from_total - L94
exact htotal
25Separate the logical casesL95–95
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L95
cases rs_seeds
26Establish rs_p2_sixL96–99
Establish this local claim before using it. It is not an additional assumption.
- L96
have rs_p2_six : ∃ hj32_local_value_rs_p2_six. Pow(2,6,hj32_local_value_rs_p2_six)Definitions: Pow(2,6,hj32_local_value_rs_p2_six)Original native command in the exact edition - L97
specialize htotal 2 - L98
specialize htotal 6 - L99
exact htotal
27Separate the logical casesL100–100
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L100
cases rs_p2_six
28Establish rs_p4_threeL101–104
Establish this local claim before using it. It is not an additional assumption.
- L101
have rs_p4_three : ∃ hj32_local_value_rs_p4_three. Pow(4,3,hj32_local_value_rs_p4_three)Definitions: Pow(4,3,hj32_local_value_rs_p4_three)Original native command in the exact edition - L102
specialize htotal 4 - L103
specialize htotal 3 - L104
exact htotal
29Separate the logical casesL105–105
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L105
cases rs_p4_three
30Establish rs_two_bridgeL106–115
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul exp from total.
- L106
have rs_two_bridge : x8 = x7 - L107
specialize pow_mul_exp_from_total 2 - L108
specialize pow_mul_exp_from_total 2 - L109
specialize pow_mul_exp_from_total 3 - L110
specialize pow_mul_exp_from_total 6 - L111
specialize pow_mul_exp_from_total 4 - L112
specialize pow_mul_exp_from_total x8 - L113
specialize pow_mul_exp_from_total x7 - L114
apply pow_mul_exp_from_total - L115
exact htotal
31Calculate and transport equalitiesL116–116
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L116
norm_num
32Use earlier factsL117–119
33Establish rs_two_boundL120–123
34Establish rs_six_product_graphL124–124
Establish this local claim before using it. It is not an additional assumption.
- L124
have rs_six_product_graph : Pow(2 · 3,6,x)Definitions: Pow(2 · 3,6,x)Original native command in the exact edition
35Establish rs_six_product_baseL125–129
36Establish rs_six_productL130–139
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul base.
37Use earlier factsL140–140
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L140
exact rs_six_product_graph
38Establish rs_eight_productL141–150
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.
39Use earlier factsL151–153
40Establish rs_resultL154–163
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.
- L154
have rs_result : Le(x7 · x5,x8 · x6)Definitions: Le(x7 · x5,x8 · x6)Original native command in the exact edition - L155
specialize mul_le_mul x7 - L156
specialize mul_le_mul x8 - L157
specialize mul_le_mul x5 - L158
specialize mul_le_mul x6 - L159
apply mul_le_mul - L160
exact rs_two_bound - L161
exact rs_three_bound - L162
rewrite <- rs_six_product at rs_result - L163
rewrite <- rs_eight_product at rs_result
41Use earlier factsL164–164
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L164
exact rs_result
Original defined command ledger · 164 lines
- 0001
intro x - 0002
intro y - 0003
intro htotal - 0004
intro hx - 0005
intro hy - 0006
have rs_p3_five : ∃ hj32_local_value_rs_p3_five. Pow(3,5,hj32_local_value_rs_p3_five)Exact native replay line
have rs_p3_five : exists hj32_local_value_rs_p3_five. (exists pa_b_hj32_local_total_rs_p3_five pa_c_hj32_local_total_rs_p3_five. ((forall pa_i_hj32_local_total_rs_p3_five_repeat. (exists pa_lt_hj32_local_total_rs_p3_five_repeat_bound. pa_lt_hj32_local_total_rs_p3_five_repeat_bound + S pa_i_hj32_local_total_rs_p3_five_repeat = 5) -> (((exists pa_h_hj32_local_total_rs_p3_five_repeat_decoded. pa_h_hj32_local_total_rs_p3_five_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_rs_p3_five_repeat)) * pa_c_hj32_local_total_rs_p3_five)) /\ exists pa_q_hj32_local_total_rs_p3_five_repeat_decoded. pa_b_hj32_local_total_rs_p3_five = pa_q_hj32_local_total_rs_p3_five_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p3_five_repeat)) * pa_c_hj32_local_total_rs_p3_five) + (3)))) /\ (exists pa_u_hj32_local_total_rs_p3_five_product pa_v_hj32_local_total_rs_p3_five_product. ((((exists pa_h_hj32_local_total_rs_p3_five_product_start. pa_h_hj32_local_total_rs_p3_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p3_five_product)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_start. pa_u_hj32_local_total_rs_p3_five_product = pa_q_hj32_local_total_rs_p3_five_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p3_five_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p3_five_product_terminal. pa_h_hj32_local_total_rs_p3_five_product_terminal + S (hj32_local_value_rs_p3_five) = S ((S (5)) * pa_v_hj32_local_total_rs_p3_five_product)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_terminal. pa_u_hj32_local_total_rs_p3_five_product = pa_q_hj32_local_total_rs_p3_five_product_terminal * S ((S (5)) * pa_v_hj32_local_total_rs_p3_five_product) + (hj32_local_value_rs_p3_five))) /\ forall pa_i_hj32_local_total_rs_p3_five_product. (exists pa_lt_hj32_local_total_rs_p3_five_product_bound. pa_lt_hj32_local_total_rs_p3_five_product_bound + S pa_i_hj32_local_total_rs_p3_five_product = 5) -> exists pa_p_hj32_local_total_rs_p3_five_product pa_r_hj32_local_total_rs_p3_five_product pa_s_hj32_local_total_rs_p3_five_product. ((((exists pa_h_hj32_local_total_rs_p3_five_product_factor. pa_h_hj32_local_total_rs_p3_five_product_factor + S (pa_p_hj32_local_total_rs_p3_five_product) = S ((S (pa_i_hj32_local_total_rs_p3_five_product)) * pa_c_hj32_local_total_rs_p3_five)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_factor. pa_b_hj32_local_total_rs_p3_five = pa_q_hj32_local_total_rs_p3_five_product_factor * S ((S (pa_i_hj32_local_total_rs_p3_five_product)) * pa_c_hj32_local_total_rs_p3_five) + (pa_p_hj32_local_total_rs_p3_five_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_five_product_partial. pa_h_hj32_local_total_rs_p3_five_product_partial + S (pa_r_hj32_local_total_rs_p3_five_product) = S ((S (pa_i_hj32_local_total_rs_p3_five_product)) * pa_v_hj32_local_total_rs_p3_five_product)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_partial. pa_u_hj32_local_total_rs_p3_five_product = pa_q_hj32_local_total_rs_p3_five_product_partial * S ((S (pa_i_hj32_local_total_rs_p3_five_product)) * pa_v_hj32_local_total_rs_p3_five_product) + (pa_r_hj32_local_total_rs_p3_five_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_five_product_successor. pa_h_hj32_local_total_rs_p3_five_product_successor + S (pa_s_hj32_local_total_rs_p3_five_product) = S ((S (S pa_i_hj32_local_total_rs_p3_five_product)) * pa_v_hj32_local_total_rs_p3_five_product)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_successor. pa_u_hj32_local_total_rs_p3_five_product = pa_q_hj32_local_total_rs_p3_five_product_successor * S ((S (S pa_i_hj32_local_total_rs_p3_five_product)) * pa_v_hj32_local_total_rs_p3_five_product) + (pa_s_hj32_local_total_rs_p3_five_product))) /\ pa_s_hj32_local_total_rs_p3_five_product = pa_r_hj32_local_total_rs_p3_five_product * pa_p_hj32_local_total_rs_p3_five_product)))))))) - 0007
specialize htotal 3 - 0008
specialize htotal 5 - 0009
exact htotal - 0010
cases rs_p3_five - 0011
have rs_p4_four : ∃ hj32_local_value_rs_p4_four. Pow(4,4,hj32_local_value_rs_p4_four)Exact native replay line
have rs_p4_four : exists hj32_local_value_rs_p4_four. (exists pa_b_hj32_local_total_rs_p4_four pa_c_hj32_local_total_rs_p4_four. ((forall pa_i_hj32_local_total_rs_p4_four_repeat. (exists pa_lt_hj32_local_total_rs_p4_four_repeat_bound. pa_lt_hj32_local_total_rs_p4_four_repeat_bound + S pa_i_hj32_local_total_rs_p4_four_repeat = 4) -> (((exists pa_h_hj32_local_total_rs_p4_four_repeat_decoded. pa_h_hj32_local_total_rs_p4_four_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rs_p4_four_repeat)) * pa_c_hj32_local_total_rs_p4_four)) /\ exists pa_q_hj32_local_total_rs_p4_four_repeat_decoded. pa_b_hj32_local_total_rs_p4_four = pa_q_hj32_local_total_rs_p4_four_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p4_four_repeat)) * pa_c_hj32_local_total_rs_p4_four) + (4)))) /\ (exists pa_u_hj32_local_total_rs_p4_four_product pa_v_hj32_local_total_rs_p4_four_product. ((((exists pa_h_hj32_local_total_rs_p4_four_product_start. pa_h_hj32_local_total_rs_p4_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p4_four_product)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_start. pa_u_hj32_local_total_rs_p4_four_product = pa_q_hj32_local_total_rs_p4_four_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p4_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p4_four_product_terminal. pa_h_hj32_local_total_rs_p4_four_product_terminal + S (hj32_local_value_rs_p4_four) = S ((S (4)) * pa_v_hj32_local_total_rs_p4_four_product)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_terminal. pa_u_hj32_local_total_rs_p4_four_product = pa_q_hj32_local_total_rs_p4_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_rs_p4_four_product) + (hj32_local_value_rs_p4_four))) /\ forall pa_i_hj32_local_total_rs_p4_four_product. (exists pa_lt_hj32_local_total_rs_p4_four_product_bound. pa_lt_hj32_local_total_rs_p4_four_product_bound + S pa_i_hj32_local_total_rs_p4_four_product = 4) -> exists pa_p_hj32_local_total_rs_p4_four_product pa_r_hj32_local_total_rs_p4_four_product pa_s_hj32_local_total_rs_p4_four_product. ((((exists pa_h_hj32_local_total_rs_p4_four_product_factor. pa_h_hj32_local_total_rs_p4_four_product_factor + S (pa_p_hj32_local_total_rs_p4_four_product) = S ((S (pa_i_hj32_local_total_rs_p4_four_product)) * pa_c_hj32_local_total_rs_p4_four)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_factor. pa_b_hj32_local_total_rs_p4_four = pa_q_hj32_local_total_rs_p4_four_product_factor * S ((S (pa_i_hj32_local_total_rs_p4_four_product)) * pa_c_hj32_local_total_rs_p4_four) + (pa_p_hj32_local_total_rs_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_four_product_partial. pa_h_hj32_local_total_rs_p4_four_product_partial + S (pa_r_hj32_local_total_rs_p4_four_product) = S ((S (pa_i_hj32_local_total_rs_p4_four_product)) * pa_v_hj32_local_total_rs_p4_four_product)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_partial. pa_u_hj32_local_total_rs_p4_four_product = pa_q_hj32_local_total_rs_p4_four_product_partial * S ((S (pa_i_hj32_local_total_rs_p4_four_product)) * pa_v_hj32_local_total_rs_p4_four_product) + (pa_r_hj32_local_total_rs_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_four_product_successor. pa_h_hj32_local_total_rs_p4_four_product_successor + S (pa_s_hj32_local_total_rs_p4_four_product) = S ((S (S pa_i_hj32_local_total_rs_p4_four_product)) * pa_v_hj32_local_total_rs_p4_four_product)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_successor. pa_u_hj32_local_total_rs_p4_four_product = pa_q_hj32_local_total_rs_p4_four_product_successor * S ((S (S pa_i_hj32_local_total_rs_p4_four_product)) * pa_v_hj32_local_total_rs_p4_four_product) + (pa_s_hj32_local_total_rs_p4_four_product))) /\ pa_s_hj32_local_total_rs_p4_four_product = pa_r_hj32_local_total_rs_p4_four_product * pa_p_hj32_local_total_rs_p4_four_product)))))))) - 0012
specialize htotal 4 - 0013
specialize htotal 4 - 0014
exact htotal - 0015
cases rs_p4_four - 0016
have rs_seed : Le(x1,x2)Exact native replay line
have rs_seed : exists bqb_le_gap_hj32_rs_seed. bqb_le_gap_hj32_rs_seed + (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 rs_p3_five_witness - 0022
exact rs_p4_four_witness - 0023
have rs_p3_one : ∃ hj32_local_value_rs_p3_one. Pow(3,1,hj32_local_value_rs_p3_one)Exact native replay line
have rs_p3_one : exists hj32_local_value_rs_p3_one. (exists pa_b_hj32_local_total_rs_p3_one pa_c_hj32_local_total_rs_p3_one. ((forall pa_i_hj32_local_total_rs_p3_one_repeat. (exists pa_lt_hj32_local_total_rs_p3_one_repeat_bound. pa_lt_hj32_local_total_rs_p3_one_repeat_bound + S pa_i_hj32_local_total_rs_p3_one_repeat = 1) -> (((exists pa_h_hj32_local_total_rs_p3_one_repeat_decoded. pa_h_hj32_local_total_rs_p3_one_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_rs_p3_one_repeat)) * pa_c_hj32_local_total_rs_p3_one)) /\ exists pa_q_hj32_local_total_rs_p3_one_repeat_decoded. pa_b_hj32_local_total_rs_p3_one = pa_q_hj32_local_total_rs_p3_one_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p3_one_repeat)) * pa_c_hj32_local_total_rs_p3_one) + (3)))) /\ (exists pa_u_hj32_local_total_rs_p3_one_product pa_v_hj32_local_total_rs_p3_one_product. ((((exists pa_h_hj32_local_total_rs_p3_one_product_start. pa_h_hj32_local_total_rs_p3_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p3_one_product)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_start. pa_u_hj32_local_total_rs_p3_one_product = pa_q_hj32_local_total_rs_p3_one_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p3_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p3_one_product_terminal. pa_h_hj32_local_total_rs_p3_one_product_terminal + S (hj32_local_value_rs_p3_one) = S ((S (1)) * pa_v_hj32_local_total_rs_p3_one_product)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_terminal. pa_u_hj32_local_total_rs_p3_one_product = pa_q_hj32_local_total_rs_p3_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_rs_p3_one_product) + (hj32_local_value_rs_p3_one))) /\ forall pa_i_hj32_local_total_rs_p3_one_product. (exists pa_lt_hj32_local_total_rs_p3_one_product_bound. pa_lt_hj32_local_total_rs_p3_one_product_bound + S pa_i_hj32_local_total_rs_p3_one_product = 1) -> exists pa_p_hj32_local_total_rs_p3_one_product pa_r_hj32_local_total_rs_p3_one_product pa_s_hj32_local_total_rs_p3_one_product. ((((exists pa_h_hj32_local_total_rs_p3_one_product_factor. pa_h_hj32_local_total_rs_p3_one_product_factor + S (pa_p_hj32_local_total_rs_p3_one_product) = S ((S (pa_i_hj32_local_total_rs_p3_one_product)) * pa_c_hj32_local_total_rs_p3_one)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_factor. pa_b_hj32_local_total_rs_p3_one = pa_q_hj32_local_total_rs_p3_one_product_factor * S ((S (pa_i_hj32_local_total_rs_p3_one_product)) * pa_c_hj32_local_total_rs_p3_one) + (pa_p_hj32_local_total_rs_p3_one_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_one_product_partial. pa_h_hj32_local_total_rs_p3_one_product_partial + S (pa_r_hj32_local_total_rs_p3_one_product) = S ((S (pa_i_hj32_local_total_rs_p3_one_product)) * pa_v_hj32_local_total_rs_p3_one_product)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_partial. pa_u_hj32_local_total_rs_p3_one_product = pa_q_hj32_local_total_rs_p3_one_product_partial * S ((S (pa_i_hj32_local_total_rs_p3_one_product)) * pa_v_hj32_local_total_rs_p3_one_product) + (pa_r_hj32_local_total_rs_p3_one_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_one_product_successor. pa_h_hj32_local_total_rs_p3_one_product_successor + S (pa_s_hj32_local_total_rs_p3_one_product) = S ((S (S pa_i_hj32_local_total_rs_p3_one_product)) * pa_v_hj32_local_total_rs_p3_one_product)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_successor. pa_u_hj32_local_total_rs_p3_one_product = pa_q_hj32_local_total_rs_p3_one_product_successor * S ((S (S pa_i_hj32_local_total_rs_p3_one_product)) * pa_v_hj32_local_total_rs_p3_one_product) + (pa_s_hj32_local_total_rs_p3_one_product))) /\ pa_s_hj32_local_total_rs_p3_one_product = pa_r_hj32_local_total_rs_p3_one_product * pa_p_hj32_local_total_rs_p3_one_product)))))))) - 0024
specialize htotal 3 - 0025
specialize htotal 1 - 0026
exact htotal - 0027
cases rs_p3_one - 0028
have rs_p4_one : ∃ hj32_local_value_rs_p4_one. Pow(4,1,hj32_local_value_rs_p4_one)Exact native replay line
have rs_p4_one : exists hj32_local_value_rs_p4_one. (exists pa_b_hj32_local_total_rs_p4_one pa_c_hj32_local_total_rs_p4_one. ((forall pa_i_hj32_local_total_rs_p4_one_repeat. (exists pa_lt_hj32_local_total_rs_p4_one_repeat_bound. pa_lt_hj32_local_total_rs_p4_one_repeat_bound + S pa_i_hj32_local_total_rs_p4_one_repeat = 1) -> (((exists pa_h_hj32_local_total_rs_p4_one_repeat_decoded. pa_h_hj32_local_total_rs_p4_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rs_p4_one_repeat)) * pa_c_hj32_local_total_rs_p4_one)) /\ exists pa_q_hj32_local_total_rs_p4_one_repeat_decoded. pa_b_hj32_local_total_rs_p4_one = pa_q_hj32_local_total_rs_p4_one_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p4_one_repeat)) * pa_c_hj32_local_total_rs_p4_one) + (4)))) /\ (exists pa_u_hj32_local_total_rs_p4_one_product pa_v_hj32_local_total_rs_p4_one_product. ((((exists pa_h_hj32_local_total_rs_p4_one_product_start. pa_h_hj32_local_total_rs_p4_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p4_one_product)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_start. pa_u_hj32_local_total_rs_p4_one_product = pa_q_hj32_local_total_rs_p4_one_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p4_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p4_one_product_terminal. pa_h_hj32_local_total_rs_p4_one_product_terminal + S (hj32_local_value_rs_p4_one) = S ((S (1)) * pa_v_hj32_local_total_rs_p4_one_product)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_terminal. pa_u_hj32_local_total_rs_p4_one_product = pa_q_hj32_local_total_rs_p4_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_rs_p4_one_product) + (hj32_local_value_rs_p4_one))) /\ forall pa_i_hj32_local_total_rs_p4_one_product. (exists pa_lt_hj32_local_total_rs_p4_one_product_bound. pa_lt_hj32_local_total_rs_p4_one_product_bound + S pa_i_hj32_local_total_rs_p4_one_product = 1) -> exists pa_p_hj32_local_total_rs_p4_one_product pa_r_hj32_local_total_rs_p4_one_product pa_s_hj32_local_total_rs_p4_one_product. ((((exists pa_h_hj32_local_total_rs_p4_one_product_factor. pa_h_hj32_local_total_rs_p4_one_product_factor + S (pa_p_hj32_local_total_rs_p4_one_product) = S ((S (pa_i_hj32_local_total_rs_p4_one_product)) * pa_c_hj32_local_total_rs_p4_one)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_factor. pa_b_hj32_local_total_rs_p4_one = pa_q_hj32_local_total_rs_p4_one_product_factor * S ((S (pa_i_hj32_local_total_rs_p4_one_product)) * pa_c_hj32_local_total_rs_p4_one) + (pa_p_hj32_local_total_rs_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_one_product_partial. pa_h_hj32_local_total_rs_p4_one_product_partial + S (pa_r_hj32_local_total_rs_p4_one_product) = S ((S (pa_i_hj32_local_total_rs_p4_one_product)) * pa_v_hj32_local_total_rs_p4_one_product)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_partial. pa_u_hj32_local_total_rs_p4_one_product = pa_q_hj32_local_total_rs_p4_one_product_partial * S ((S (pa_i_hj32_local_total_rs_p4_one_product)) * pa_v_hj32_local_total_rs_p4_one_product) + (pa_r_hj32_local_total_rs_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_one_product_successor. pa_h_hj32_local_total_rs_p4_one_product_successor + S (pa_s_hj32_local_total_rs_p4_one_product) = S ((S (S pa_i_hj32_local_total_rs_p4_one_product)) * pa_v_hj32_local_total_rs_p4_one_product)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_successor. pa_u_hj32_local_total_rs_p4_one_product = pa_q_hj32_local_total_rs_p4_one_product_successor * S ((S (S pa_i_hj32_local_total_rs_p4_one_product)) * pa_v_hj32_local_total_rs_p4_one_product) + (pa_s_hj32_local_total_rs_p4_one_product))) /\ pa_s_hj32_local_total_rs_p4_one_product = pa_r_hj32_local_total_rs_p4_one_product * pa_p_hj32_local_total_rs_p4_one_product)))))))) - 0029
specialize htotal 4 - 0030
specialize htotal 1 - 0031
exact htotal - 0032
cases rs_p4_one - 0033
have rs_base : Lt(2,4)Exact native replay line
have rs_base : exists bqb_le_gap_hj32_rs_base. bqb_le_gap_hj32_rs_base + (3) = (4) - 0034
exists 1 - 0035
norm_num - 0036
have rs_one_bound : Le(x3,x4)Exact native replay line
have rs_one_bound : exists bqb_le_gap_hj32_local_base_bound_rs_one_bound. bqb_le_gap_hj32_local_base_bound_rs_one_bound + (x3) = (x4) - 0037
specialize pow_base_monotone 3 - 0038
specialize pow_base_monotone 4 - 0039
specialize pow_base_monotone 1 - 0040
specialize pow_base_monotone x3 - 0041
specialize pow_base_monotone x4 - 0042
apply pow_base_monotone - 0043
exact rs_base - 0044
exact rs_p3_one_witness - 0045
exact rs_p4_one_witness - 0046
have rs_p3_six : ∃ hj32_local_value_rs_p3_six. Pow(3,6,hj32_local_value_rs_p3_six)Exact native replay line
have rs_p3_six : exists hj32_local_value_rs_p3_six. (exists pa_b_hj32_local_total_rs_p3_six pa_c_hj32_local_total_rs_p3_six. ((forall pa_i_hj32_local_total_rs_p3_six_repeat. (exists pa_lt_hj32_local_total_rs_p3_six_repeat_bound. pa_lt_hj32_local_total_rs_p3_six_repeat_bound + S pa_i_hj32_local_total_rs_p3_six_repeat = 6) -> (((exists pa_h_hj32_local_total_rs_p3_six_repeat_decoded. pa_h_hj32_local_total_rs_p3_six_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_rs_p3_six_repeat)) * pa_c_hj32_local_total_rs_p3_six)) /\ exists pa_q_hj32_local_total_rs_p3_six_repeat_decoded. pa_b_hj32_local_total_rs_p3_six = pa_q_hj32_local_total_rs_p3_six_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p3_six_repeat)) * pa_c_hj32_local_total_rs_p3_six) + (3)))) /\ (exists pa_u_hj32_local_total_rs_p3_six_product pa_v_hj32_local_total_rs_p3_six_product. ((((exists pa_h_hj32_local_total_rs_p3_six_product_start. pa_h_hj32_local_total_rs_p3_six_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p3_six_product)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_start. pa_u_hj32_local_total_rs_p3_six_product = pa_q_hj32_local_total_rs_p3_six_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p3_six_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p3_six_product_terminal. pa_h_hj32_local_total_rs_p3_six_product_terminal + S (hj32_local_value_rs_p3_six) = S ((S (6)) * pa_v_hj32_local_total_rs_p3_six_product)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_terminal. pa_u_hj32_local_total_rs_p3_six_product = pa_q_hj32_local_total_rs_p3_six_product_terminal * S ((S (6)) * pa_v_hj32_local_total_rs_p3_six_product) + (hj32_local_value_rs_p3_six))) /\ forall pa_i_hj32_local_total_rs_p3_six_product. (exists pa_lt_hj32_local_total_rs_p3_six_product_bound. pa_lt_hj32_local_total_rs_p3_six_product_bound + S pa_i_hj32_local_total_rs_p3_six_product = 6) -> exists pa_p_hj32_local_total_rs_p3_six_product pa_r_hj32_local_total_rs_p3_six_product pa_s_hj32_local_total_rs_p3_six_product. ((((exists pa_h_hj32_local_total_rs_p3_six_product_factor. pa_h_hj32_local_total_rs_p3_six_product_factor + S (pa_p_hj32_local_total_rs_p3_six_product) = S ((S (pa_i_hj32_local_total_rs_p3_six_product)) * pa_c_hj32_local_total_rs_p3_six)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_factor. pa_b_hj32_local_total_rs_p3_six = pa_q_hj32_local_total_rs_p3_six_product_factor * S ((S (pa_i_hj32_local_total_rs_p3_six_product)) * pa_c_hj32_local_total_rs_p3_six) + (pa_p_hj32_local_total_rs_p3_six_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_six_product_partial. pa_h_hj32_local_total_rs_p3_six_product_partial + S (pa_r_hj32_local_total_rs_p3_six_product) = S ((S (pa_i_hj32_local_total_rs_p3_six_product)) * pa_v_hj32_local_total_rs_p3_six_product)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_partial. pa_u_hj32_local_total_rs_p3_six_product = pa_q_hj32_local_total_rs_p3_six_product_partial * S ((S (pa_i_hj32_local_total_rs_p3_six_product)) * pa_v_hj32_local_total_rs_p3_six_product) + (pa_r_hj32_local_total_rs_p3_six_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_six_product_successor. pa_h_hj32_local_total_rs_p3_six_product_successor + S (pa_s_hj32_local_total_rs_p3_six_product) = S ((S (S pa_i_hj32_local_total_rs_p3_six_product)) * pa_v_hj32_local_total_rs_p3_six_product)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_successor. pa_u_hj32_local_total_rs_p3_six_product = pa_q_hj32_local_total_rs_p3_six_product_successor * S ((S (S pa_i_hj32_local_total_rs_p3_six_product)) * pa_v_hj32_local_total_rs_p3_six_product) + (pa_s_hj32_local_total_rs_p3_six_product))) /\ pa_s_hj32_local_total_rs_p3_six_product = pa_r_hj32_local_total_rs_p3_six_product * pa_p_hj32_local_total_rs_p3_six_product)))))))) - 0047
specialize htotal 3 - 0048
specialize htotal 6 - 0049
exact htotal - 0050
cases rs_p3_six - 0051
have rs_p4_five : ∃ hj32_local_value_rs_p4_five. Pow(4,5,hj32_local_value_rs_p4_five)Exact native replay line
have rs_p4_five : exists hj32_local_value_rs_p4_five. (exists pa_b_hj32_local_total_rs_p4_five pa_c_hj32_local_total_rs_p4_five. ((forall pa_i_hj32_local_total_rs_p4_five_repeat. (exists pa_lt_hj32_local_total_rs_p4_five_repeat_bound. pa_lt_hj32_local_total_rs_p4_five_repeat_bound + S pa_i_hj32_local_total_rs_p4_five_repeat = 5) -> (((exists pa_h_hj32_local_total_rs_p4_five_repeat_decoded. pa_h_hj32_local_total_rs_p4_five_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rs_p4_five_repeat)) * pa_c_hj32_local_total_rs_p4_five)) /\ exists pa_q_hj32_local_total_rs_p4_five_repeat_decoded. pa_b_hj32_local_total_rs_p4_five = pa_q_hj32_local_total_rs_p4_five_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p4_five_repeat)) * pa_c_hj32_local_total_rs_p4_five) + (4)))) /\ (exists pa_u_hj32_local_total_rs_p4_five_product pa_v_hj32_local_total_rs_p4_five_product. ((((exists pa_h_hj32_local_total_rs_p4_five_product_start. pa_h_hj32_local_total_rs_p4_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p4_five_product)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_start. pa_u_hj32_local_total_rs_p4_five_product = pa_q_hj32_local_total_rs_p4_five_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p4_five_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p4_five_product_terminal. pa_h_hj32_local_total_rs_p4_five_product_terminal + S (hj32_local_value_rs_p4_five) = S ((S (5)) * pa_v_hj32_local_total_rs_p4_five_product)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_terminal. pa_u_hj32_local_total_rs_p4_five_product = pa_q_hj32_local_total_rs_p4_five_product_terminal * S ((S (5)) * pa_v_hj32_local_total_rs_p4_five_product) + (hj32_local_value_rs_p4_five))) /\ forall pa_i_hj32_local_total_rs_p4_five_product. (exists pa_lt_hj32_local_total_rs_p4_five_product_bound. pa_lt_hj32_local_total_rs_p4_five_product_bound + S pa_i_hj32_local_total_rs_p4_five_product = 5) -> exists pa_p_hj32_local_total_rs_p4_five_product pa_r_hj32_local_total_rs_p4_five_product pa_s_hj32_local_total_rs_p4_five_product. ((((exists pa_h_hj32_local_total_rs_p4_five_product_factor. pa_h_hj32_local_total_rs_p4_five_product_factor + S (pa_p_hj32_local_total_rs_p4_five_product) = S ((S (pa_i_hj32_local_total_rs_p4_five_product)) * pa_c_hj32_local_total_rs_p4_five)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_factor. pa_b_hj32_local_total_rs_p4_five = pa_q_hj32_local_total_rs_p4_five_product_factor * S ((S (pa_i_hj32_local_total_rs_p4_five_product)) * pa_c_hj32_local_total_rs_p4_five) + (pa_p_hj32_local_total_rs_p4_five_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_five_product_partial. pa_h_hj32_local_total_rs_p4_five_product_partial + S (pa_r_hj32_local_total_rs_p4_five_product) = S ((S (pa_i_hj32_local_total_rs_p4_five_product)) * pa_v_hj32_local_total_rs_p4_five_product)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_partial. pa_u_hj32_local_total_rs_p4_five_product = pa_q_hj32_local_total_rs_p4_five_product_partial * S ((S (pa_i_hj32_local_total_rs_p4_five_product)) * pa_v_hj32_local_total_rs_p4_five_product) + (pa_r_hj32_local_total_rs_p4_five_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_five_product_successor. pa_h_hj32_local_total_rs_p4_five_product_successor + S (pa_s_hj32_local_total_rs_p4_five_product) = S ((S (S pa_i_hj32_local_total_rs_p4_five_product)) * pa_v_hj32_local_total_rs_p4_five_product)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_successor. pa_u_hj32_local_total_rs_p4_five_product = pa_q_hj32_local_total_rs_p4_five_product_successor * S ((S (S pa_i_hj32_local_total_rs_p4_five_product)) * pa_v_hj32_local_total_rs_p4_five_product) + (pa_s_hj32_local_total_rs_p4_five_product))) /\ pa_s_hj32_local_total_rs_p4_five_product = pa_r_hj32_local_total_rs_p4_five_product * pa_p_hj32_local_total_rs_p4_five_product)))))))) - 0052
specialize htotal 4 - 0053
specialize htotal 5 - 0054
exact htotal - 0055
cases rs_p4_five - 0056
have rs_three_product : x5 = x1 * x3 - 0057
specialize pow_add 3 - 0058
specialize pow_add 5 - 0059
specialize pow_add 1 - 0060
specialize pow_add 6 - 0061
specialize pow_add x1 - 0062
specialize pow_add x3 - 0063
specialize pow_add x5 - 0064
apply pow_add - 0065
norm_num - 0066
exact rs_p3_five_witness - 0067
exact rs_p3_one_witness - 0068
exact rs_p3_six_witness - 0069
have rs_four_product : x6 = x2 * x4 - 0070
specialize pow_add 4 - 0071
specialize pow_add 4 - 0072
specialize pow_add 1 - 0073
specialize pow_add 5 - 0074
specialize pow_add x2 - 0075
specialize pow_add x4 - 0076
specialize pow_add x6 - 0077
apply pow_add - 0078
norm_num - 0079
exact rs_p4_four_witness - 0080
exact rs_p4_one_witness - 0081
exact rs_p4_five_witness - 0082
have rs_three_bound : Le(x1 · x3,x2 · x4)Exact native replay line
have rs_three_bound : exists bqb_le_gap_hj32_local_product_bound_rs_three_bound. bqb_le_gap_hj32_local_product_bound_rs_three_bound + (x1 * x3) = (x2 * x4) - 0083
specialize mul_le_mul x1 - 0084
specialize mul_le_mul x2 - 0085
specialize mul_le_mul x3 - 0086
specialize mul_le_mul x4 - 0087
apply mul_le_mul - 0088
exact rs_seed - 0089
exact rs_one_bound - 0090
rewrite <- rs_three_product at rs_three_bound - 0091
rewrite <- rs_four_product at rs_three_bound - 0092
have rs_seeds : Pow(2,2,4) ∧ Pow(2,7,128)Exact native replay line
have rs_seeds : (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)))))))) - 0093
apply pow_two_seed_bundle_from_total - 0094
exact htotal - 0095
cases rs_seeds - 0096
have rs_p2_six : ∃ hj32_local_value_rs_p2_six. Pow(2,6,hj32_local_value_rs_p2_six)Exact native replay line
have rs_p2_six : exists hj32_local_value_rs_p2_six. (exists pa_b_hj32_local_total_rs_p2_six pa_c_hj32_local_total_rs_p2_six. ((forall pa_i_hj32_local_total_rs_p2_six_repeat. (exists pa_lt_hj32_local_total_rs_p2_six_repeat_bound. pa_lt_hj32_local_total_rs_p2_six_repeat_bound + S pa_i_hj32_local_total_rs_p2_six_repeat = 6) -> (((exists pa_h_hj32_local_total_rs_p2_six_repeat_decoded. pa_h_hj32_local_total_rs_p2_six_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_rs_p2_six_repeat)) * pa_c_hj32_local_total_rs_p2_six)) /\ exists pa_q_hj32_local_total_rs_p2_six_repeat_decoded. pa_b_hj32_local_total_rs_p2_six = pa_q_hj32_local_total_rs_p2_six_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p2_six_repeat)) * pa_c_hj32_local_total_rs_p2_six) + (2)))) /\ (exists pa_u_hj32_local_total_rs_p2_six_product pa_v_hj32_local_total_rs_p2_six_product. ((((exists pa_h_hj32_local_total_rs_p2_six_product_start. pa_h_hj32_local_total_rs_p2_six_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p2_six_product)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_start. pa_u_hj32_local_total_rs_p2_six_product = pa_q_hj32_local_total_rs_p2_six_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p2_six_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p2_six_product_terminal. pa_h_hj32_local_total_rs_p2_six_product_terminal + S (hj32_local_value_rs_p2_six) = S ((S (6)) * pa_v_hj32_local_total_rs_p2_six_product)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_terminal. pa_u_hj32_local_total_rs_p2_six_product = pa_q_hj32_local_total_rs_p2_six_product_terminal * S ((S (6)) * pa_v_hj32_local_total_rs_p2_six_product) + (hj32_local_value_rs_p2_six))) /\ forall pa_i_hj32_local_total_rs_p2_six_product. (exists pa_lt_hj32_local_total_rs_p2_six_product_bound. pa_lt_hj32_local_total_rs_p2_six_product_bound + S pa_i_hj32_local_total_rs_p2_six_product = 6) -> exists pa_p_hj32_local_total_rs_p2_six_product pa_r_hj32_local_total_rs_p2_six_product pa_s_hj32_local_total_rs_p2_six_product. ((((exists pa_h_hj32_local_total_rs_p2_six_product_factor. pa_h_hj32_local_total_rs_p2_six_product_factor + S (pa_p_hj32_local_total_rs_p2_six_product) = S ((S (pa_i_hj32_local_total_rs_p2_six_product)) * pa_c_hj32_local_total_rs_p2_six)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_factor. pa_b_hj32_local_total_rs_p2_six = pa_q_hj32_local_total_rs_p2_six_product_factor * S ((S (pa_i_hj32_local_total_rs_p2_six_product)) * pa_c_hj32_local_total_rs_p2_six) + (pa_p_hj32_local_total_rs_p2_six_product))) /\ ((((exists pa_h_hj32_local_total_rs_p2_six_product_partial. pa_h_hj32_local_total_rs_p2_six_product_partial + S (pa_r_hj32_local_total_rs_p2_six_product) = S ((S (pa_i_hj32_local_total_rs_p2_six_product)) * pa_v_hj32_local_total_rs_p2_six_product)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_partial. pa_u_hj32_local_total_rs_p2_six_product = pa_q_hj32_local_total_rs_p2_six_product_partial * S ((S (pa_i_hj32_local_total_rs_p2_six_product)) * pa_v_hj32_local_total_rs_p2_six_product) + (pa_r_hj32_local_total_rs_p2_six_product))) /\ ((((exists pa_h_hj32_local_total_rs_p2_six_product_successor. pa_h_hj32_local_total_rs_p2_six_product_successor + S (pa_s_hj32_local_total_rs_p2_six_product) = S ((S (S pa_i_hj32_local_total_rs_p2_six_product)) * pa_v_hj32_local_total_rs_p2_six_product)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_successor. pa_u_hj32_local_total_rs_p2_six_product = pa_q_hj32_local_total_rs_p2_six_product_successor * S ((S (S pa_i_hj32_local_total_rs_p2_six_product)) * pa_v_hj32_local_total_rs_p2_six_product) + (pa_s_hj32_local_total_rs_p2_six_product))) /\ pa_s_hj32_local_total_rs_p2_six_product = pa_r_hj32_local_total_rs_p2_six_product * pa_p_hj32_local_total_rs_p2_six_product)))))))) - 0097
specialize htotal 2 - 0098
specialize htotal 6 - 0099
exact htotal - 0100
cases rs_p2_six - 0101
have rs_p4_three : ∃ hj32_local_value_rs_p4_three. Pow(4,3,hj32_local_value_rs_p4_three)Exact native replay line
have rs_p4_three : exists hj32_local_value_rs_p4_three. (exists pa_b_hj32_local_total_rs_p4_three pa_c_hj32_local_total_rs_p4_three. ((forall pa_i_hj32_local_total_rs_p4_three_repeat. (exists pa_lt_hj32_local_total_rs_p4_three_repeat_bound. pa_lt_hj32_local_total_rs_p4_three_repeat_bound + S pa_i_hj32_local_total_rs_p4_three_repeat = 3) -> (((exists pa_h_hj32_local_total_rs_p4_three_repeat_decoded. pa_h_hj32_local_total_rs_p4_three_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rs_p4_three_repeat)) * pa_c_hj32_local_total_rs_p4_three)) /\ exists pa_q_hj32_local_total_rs_p4_three_repeat_decoded. pa_b_hj32_local_total_rs_p4_three = pa_q_hj32_local_total_rs_p4_three_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p4_three_repeat)) * pa_c_hj32_local_total_rs_p4_three) + (4)))) /\ (exists pa_u_hj32_local_total_rs_p4_three_product pa_v_hj32_local_total_rs_p4_three_product. ((((exists pa_h_hj32_local_total_rs_p4_three_product_start. pa_h_hj32_local_total_rs_p4_three_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p4_three_product)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_start. pa_u_hj32_local_total_rs_p4_three_product = pa_q_hj32_local_total_rs_p4_three_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p4_three_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p4_three_product_terminal. pa_h_hj32_local_total_rs_p4_three_product_terminal + S (hj32_local_value_rs_p4_three) = S ((S (3)) * pa_v_hj32_local_total_rs_p4_three_product)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_terminal. pa_u_hj32_local_total_rs_p4_three_product = pa_q_hj32_local_total_rs_p4_three_product_terminal * S ((S (3)) * pa_v_hj32_local_total_rs_p4_three_product) + (hj32_local_value_rs_p4_three))) /\ forall pa_i_hj32_local_total_rs_p4_three_product. (exists pa_lt_hj32_local_total_rs_p4_three_product_bound. pa_lt_hj32_local_total_rs_p4_three_product_bound + S pa_i_hj32_local_total_rs_p4_three_product = 3) -> exists pa_p_hj32_local_total_rs_p4_three_product pa_r_hj32_local_total_rs_p4_three_product pa_s_hj32_local_total_rs_p4_three_product. ((((exists pa_h_hj32_local_total_rs_p4_three_product_factor. pa_h_hj32_local_total_rs_p4_three_product_factor + S (pa_p_hj32_local_total_rs_p4_three_product) = S ((S (pa_i_hj32_local_total_rs_p4_three_product)) * pa_c_hj32_local_total_rs_p4_three)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_factor. pa_b_hj32_local_total_rs_p4_three = pa_q_hj32_local_total_rs_p4_three_product_factor * S ((S (pa_i_hj32_local_total_rs_p4_three_product)) * pa_c_hj32_local_total_rs_p4_three) + (pa_p_hj32_local_total_rs_p4_three_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_three_product_partial. pa_h_hj32_local_total_rs_p4_three_product_partial + S (pa_r_hj32_local_total_rs_p4_three_product) = S ((S (pa_i_hj32_local_total_rs_p4_three_product)) * pa_v_hj32_local_total_rs_p4_three_product)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_partial. pa_u_hj32_local_total_rs_p4_three_product = pa_q_hj32_local_total_rs_p4_three_product_partial * S ((S (pa_i_hj32_local_total_rs_p4_three_product)) * pa_v_hj32_local_total_rs_p4_three_product) + (pa_r_hj32_local_total_rs_p4_three_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_three_product_successor. pa_h_hj32_local_total_rs_p4_three_product_successor + S (pa_s_hj32_local_total_rs_p4_three_product) = S ((S (S pa_i_hj32_local_total_rs_p4_three_product)) * pa_v_hj32_local_total_rs_p4_three_product)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_successor. pa_u_hj32_local_total_rs_p4_three_product = pa_q_hj32_local_total_rs_p4_three_product_successor * S ((S (S pa_i_hj32_local_total_rs_p4_three_product)) * pa_v_hj32_local_total_rs_p4_three_product) + (pa_s_hj32_local_total_rs_p4_three_product))) /\ pa_s_hj32_local_total_rs_p4_three_product = pa_r_hj32_local_total_rs_p4_three_product * pa_p_hj32_local_total_rs_p4_three_product)))))))) - 0102
specialize htotal 4 - 0103
specialize htotal 3 - 0104
exact htotal - 0105
cases rs_p4_three - 0106
have rs_two_bridge : x8 = x7 - 0107
specialize pow_mul_exp_from_total 2 - 0108
specialize pow_mul_exp_from_total 2 - 0109
specialize pow_mul_exp_from_total 3 - 0110
specialize pow_mul_exp_from_total 6 - 0111
specialize pow_mul_exp_from_total 4 - 0112
specialize pow_mul_exp_from_total x8 - 0113
specialize pow_mul_exp_from_total x7 - 0114
apply pow_mul_exp_from_total - 0115
exact htotal - 0116
norm_num - 0117
exact rs_seeds_left - 0118
exact rs_p4_three_witness - 0119
exact rs_p2_six_witness - 0120
have rs_two_bound : Le(x7,x8)Exact native replay line
have rs_two_bound : exists bqb_le_gap_hj32_rs_two_bound. bqb_le_gap_hj32_rs_two_bound + (x7) = (x8) - 0121
rewrite rs_two_bridge - 0122
specialize le_refl x7 - 0123
exact le_refl - 0124
have rs_six_product_graph : Pow(2 · 3,6,x)Exact native replay line
have rs_six_product_graph : exists pa_b_hj32_local_product_rs_six_product pa_c_hj32_local_product_rs_six_product. ((forall pa_i_hj32_local_product_rs_six_product_repeat. (exists pa_lt_hj32_local_product_rs_six_product_repeat_bound. pa_lt_hj32_local_product_rs_six_product_repeat_bound + S pa_i_hj32_local_product_rs_six_product_repeat = 6) -> (((exists pa_h_hj32_local_product_rs_six_product_repeat_decoded. pa_h_hj32_local_product_rs_six_product_repeat_decoded + S (2 * 3) = S ((S (pa_i_hj32_local_product_rs_six_product_repeat)) * pa_c_hj32_local_product_rs_six_product)) /\ exists pa_q_hj32_local_product_rs_six_product_repeat_decoded. pa_b_hj32_local_product_rs_six_product = pa_q_hj32_local_product_rs_six_product_repeat_decoded * S ((S (pa_i_hj32_local_product_rs_six_product_repeat)) * pa_c_hj32_local_product_rs_six_product) + (2 * 3)))) /\ (exists pa_u_hj32_local_product_rs_six_product_product pa_v_hj32_local_product_rs_six_product_product. ((((exists pa_h_hj32_local_product_rs_six_product_product_start. pa_h_hj32_local_product_rs_six_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_rs_six_product_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_start. pa_u_hj32_local_product_rs_six_product_product = pa_q_hj32_local_product_rs_six_product_product_start * S ((S (0)) * pa_v_hj32_local_product_rs_six_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_rs_six_product_product_terminal. pa_h_hj32_local_product_rs_six_product_product_terminal + S (x) = S ((S (6)) * pa_v_hj32_local_product_rs_six_product_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_terminal. pa_u_hj32_local_product_rs_six_product_product = pa_q_hj32_local_product_rs_six_product_product_terminal * S ((S (6)) * pa_v_hj32_local_product_rs_six_product_product) + (x))) /\ forall pa_i_hj32_local_product_rs_six_product_product. (exists pa_lt_hj32_local_product_rs_six_product_product_bound. pa_lt_hj32_local_product_rs_six_product_product_bound + S pa_i_hj32_local_product_rs_six_product_product = 6) -> exists pa_p_hj32_local_product_rs_six_product_product pa_r_hj32_local_product_rs_six_product_product pa_s_hj32_local_product_rs_six_product_product. ((((exists pa_h_hj32_local_product_rs_six_product_product_factor. pa_h_hj32_local_product_rs_six_product_product_factor + S (pa_p_hj32_local_product_rs_six_product_product) = S ((S (pa_i_hj32_local_product_rs_six_product_product)) * pa_c_hj32_local_product_rs_six_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_factor. pa_b_hj32_local_product_rs_six_product = pa_q_hj32_local_product_rs_six_product_product_factor * S ((S (pa_i_hj32_local_product_rs_six_product_product)) * pa_c_hj32_local_product_rs_six_product) + (pa_p_hj32_local_product_rs_six_product_product))) /\ ((((exists pa_h_hj32_local_product_rs_six_product_product_partial. pa_h_hj32_local_product_rs_six_product_product_partial + S (pa_r_hj32_local_product_rs_six_product_product) = S ((S (pa_i_hj32_local_product_rs_six_product_product)) * pa_v_hj32_local_product_rs_six_product_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_partial. pa_u_hj32_local_product_rs_six_product_product = pa_q_hj32_local_product_rs_six_product_product_partial * S ((S (pa_i_hj32_local_product_rs_six_product_product)) * pa_v_hj32_local_product_rs_six_product_product) + (pa_r_hj32_local_product_rs_six_product_product))) /\ ((((exists pa_h_hj32_local_product_rs_six_product_product_successor. pa_h_hj32_local_product_rs_six_product_product_successor + S (pa_s_hj32_local_product_rs_six_product_product) = S ((S (S pa_i_hj32_local_product_rs_six_product_product)) * pa_v_hj32_local_product_rs_six_product_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_successor. pa_u_hj32_local_product_rs_six_product_product = pa_q_hj32_local_product_rs_six_product_product_successor * S ((S (S pa_i_hj32_local_product_rs_six_product_product)) * pa_v_hj32_local_product_rs_six_product_product) + (pa_s_hj32_local_product_rs_six_product_product))) /\ pa_s_hj32_local_product_rs_six_product_product = pa_r_hj32_local_product_rs_six_product_product * pa_p_hj32_local_product_rs_six_product_product))))))) - 0125
have rs_six_product_base : 2 * 3 = 6 - 0126
norm_num - 0127
rewrite rs_six_product_base - 0128
rewrite rs_six_product_base - 0129
exact hx - 0130
have rs_six_product : x = x7 * x5 - 0131
specialize pow_mul_base 2 - 0132
specialize pow_mul_base 3 - 0133
specialize pow_mul_base 6 - 0134
specialize pow_mul_base x7 - 0135
specialize pow_mul_base x5 - 0136
specialize pow_mul_base x - 0137
apply pow_mul_base - 0138
exact rs_p2_six_witness - 0139
exact rs_p3_six_witness - 0140
exact rs_six_product_graph - 0141
have rs_eight_product : y = x8 * x6 - 0142
specialize pow_add 4 - 0143
specialize pow_add 3 - 0144
specialize pow_add 5 - 0145
specialize pow_add 8 - 0146
specialize pow_add x8 - 0147
specialize pow_add x6 - 0148
specialize pow_add y - 0149
apply pow_add - 0150
norm_num - 0151
exact rs_p4_three_witness - 0152
exact rs_p4_five_witness - 0153
exact hy - 0154
have rs_result : Le(x7 · x5,x8 · x6)Exact native replay line
have rs_result : exists bqb_le_gap_hj32_local_product_bound_rs_result. bqb_le_gap_hj32_local_product_bound_rs_result + (x7 * x5) = (x8 * x6) - 0155
specialize mul_le_mul x7 - 0156
specialize mul_le_mul x8 - 0157
specialize mul_le_mul x5 - 0158
specialize mul_le_mul x6 - 0159
apply mul_le_mul - 0160
exact rs_two_bound - 0161
exact rs_three_bound - 0162
rewrite <- rs_six_product at rs_result - 0163
rewrite <- rs_eight_product at rs_result - 0164
exact rs_result