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(3,5,x) → Pow(4,4,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
13 occurrences
Exact expanded native-PA statement
forall x y. (forall bpt_a_hj32_three_four bpt_e_hj32_three_four. exists bpt_x_hj32_three_four. (exists ff_b_bpt_value_hj32_three_four ff_c_bpt_value_hj32_three_four. ((forall ff_i_bpt_value_hj32_three_four_repeat. (exists ff_lt_bpt_value_hj32_three_four_repeat_bound. ff_lt_bpt_value_hj32_three_four_repeat_bound + S ff_i_bpt_value_hj32_three_four_repeat = bpt_e_hj32_three_four) -> (((exists ff_h_bpt_value_hj32_three_four_repeat_decoded. ff_h_bpt_value_hj32_three_four_repeat_decoded + S (bpt_a_hj32_three_four) = S ((S (ff_i_bpt_value_hj32_three_four_repeat)) * ff_c_bpt_value_hj32_three_four)) /\ exists ff_q_bpt_value_hj32_three_four_repeat_decoded. ff_b_bpt_value_hj32_three_four = ff_q_bpt_value_hj32_three_four_repeat_decoded * S ((S (ff_i_bpt_value_hj32_three_four_repeat)) * ff_c_bpt_value_hj32_three_four) + (bpt_a_hj32_three_four)))) /\ (exists ff_u_bpt_value_hj32_three_four_product ff_v_bpt_value_hj32_three_four_product. ((((exists ff_h_bpt_value_hj32_three_four_product_start. ff_h_bpt_value_hj32_three_four_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_three_four_product)) /\ exists ff_q_bpt_value_hj32_three_four_product_start. ff_u_bpt_value_hj32_three_four_product = ff_q_bpt_value_hj32_three_four_product_start * S ((S (0)) * ff_v_bpt_value_hj32_three_four_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_three_four_product_terminal. ff_h_bpt_value_hj32_three_four_product_terminal + S (bpt_x_hj32_three_four) = S ((S (bpt_e_hj32_three_four)) * ff_v_bpt_value_hj32_three_four_product)) /\ exists ff_q_bpt_value_hj32_three_four_product_terminal. ff_u_bpt_value_hj32_three_four_product = ff_q_bpt_value_hj32_three_four_product_terminal * S ((S (bpt_e_hj32_three_four)) * ff_v_bpt_value_hj32_three_four_product) + (bpt_x_hj32_three_four))) /\ forall ff_i_bpt_value_hj32_three_four_product. (exists ff_lt_bpt_value_hj32_three_four_product_bound. ff_lt_bpt_value_hj32_three_four_product_bound + S ff_i_bpt_value_hj32_three_four_product = bpt_e_hj32_three_four) -> exists ff_p_bpt_value_hj32_three_four_product ff_r_bpt_value_hj32_three_four_product ff_s_bpt_value_hj32_three_four_product. ((((exists ff_h_bpt_value_hj32_three_four_product_factor. ff_h_bpt_value_hj32_three_four_product_factor + S (ff_p_bpt_value_hj32_three_four_product) = S ((S (ff_i_bpt_value_hj32_three_four_product)) * ff_c_bpt_value_hj32_three_four)) /\ exists ff_q_bpt_value_hj32_three_four_product_factor. ff_b_bpt_value_hj32_three_four = ff_q_bpt_value_hj32_three_four_product_factor * S ((S (ff_i_bpt_value_hj32_three_four_product)) * ff_c_bpt_value_hj32_three_four) + (ff_p_bpt_value_hj32_three_four_product))) /\ ((((exists ff_h_bpt_value_hj32_three_four_product_partial. ff_h_bpt_value_hj32_three_four_product_partial + S (ff_r_bpt_value_hj32_three_four_product) = S ((S (ff_i_bpt_value_hj32_three_four_product)) * ff_v_bpt_value_hj32_three_four_product)) /\ exists ff_q_bpt_value_hj32_three_four_product_partial. ff_u_bpt_value_hj32_three_four_product = ff_q_bpt_value_hj32_three_four_product_partial * S ((S (ff_i_bpt_value_hj32_three_four_product)) * ff_v_bpt_value_hj32_three_four_product) + (ff_r_bpt_value_hj32_three_four_product))) /\ ((((exists ff_h_bpt_value_hj32_three_four_product_successor. ff_h_bpt_value_hj32_three_four_product_successor + S (ff_s_bpt_value_hj32_three_four_product) = S ((S (S ff_i_bpt_value_hj32_three_four_product)) * ff_v_bpt_value_hj32_three_four_product)) /\ exists ff_q_bpt_value_hj32_three_four_product_successor. ff_u_bpt_value_hj32_three_four_product = ff_q_bpt_value_hj32_three_four_product_successor * S ((S (S ff_i_bpt_value_hj32_three_four_product)) * ff_v_bpt_value_hj32_three_four_product) + (ff_s_bpt_value_hj32_three_four_product))) /\ ff_s_bpt_value_hj32_three_four_product = ff_r_bpt_value_hj32_three_four_product * ff_p_bpt_value_hj32_three_four_product))))))))) -> (exists pa_b_hj32_three_five pa_c_hj32_three_five. ((forall pa_i_hj32_three_five_repeat. (exists pa_lt_hj32_three_five_repeat_bound. pa_lt_hj32_three_five_repeat_bound + S pa_i_hj32_three_five_repeat = 5) -> (((exists pa_h_hj32_three_five_repeat_decoded. pa_h_hj32_three_five_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_five_repeat)) * pa_c_hj32_three_five)) /\ exists pa_q_hj32_three_five_repeat_decoded. pa_b_hj32_three_five = pa_q_hj32_three_five_repeat_decoded * S ((S (pa_i_hj32_three_five_repeat)) * pa_c_hj32_three_five) + (3)))) /\ (exists pa_u_hj32_three_five_product pa_v_hj32_three_five_product. ((((exists pa_h_hj32_three_five_product_start. pa_h_hj32_three_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_five_product)) /\ exists pa_q_hj32_three_five_product_start. pa_u_hj32_three_five_product = pa_q_hj32_three_five_product_start * S ((S (0)) * pa_v_hj32_three_five_product) + (1))) /\ ((((exists pa_h_hj32_three_five_product_terminal. pa_h_hj32_three_five_product_terminal + S (x) = S ((S (5)) * pa_v_hj32_three_five_product)) /\ exists pa_q_hj32_three_five_product_terminal. pa_u_hj32_three_five_product = pa_q_hj32_three_five_product_terminal * S ((S (5)) * pa_v_hj32_three_five_product) + (x))) /\ forall pa_i_hj32_three_five_product. (exists pa_lt_hj32_three_five_product_bound. pa_lt_hj32_three_five_product_bound + S pa_i_hj32_three_five_product = 5) -> exists pa_p_hj32_three_five_product pa_r_hj32_three_five_product pa_s_hj32_three_five_product. ((((exists pa_h_hj32_three_five_product_factor. pa_h_hj32_three_five_product_factor + S (pa_p_hj32_three_five_product) = S ((S (pa_i_hj32_three_five_product)) * pa_c_hj32_three_five)) /\ exists pa_q_hj32_three_five_product_factor. pa_b_hj32_three_five = pa_q_hj32_three_five_product_factor * S ((S (pa_i_hj32_three_five_product)) * pa_c_hj32_three_five) + (pa_p_hj32_three_five_product))) /\ ((((exists pa_h_hj32_three_five_product_partial. pa_h_hj32_three_five_product_partial + S (pa_r_hj32_three_five_product) = S ((S (pa_i_hj32_three_five_product)) * pa_v_hj32_three_five_product)) /\ exists pa_q_hj32_three_five_product_partial. pa_u_hj32_three_five_product = pa_q_hj32_three_five_product_partial * S ((S (pa_i_hj32_three_five_product)) * pa_v_hj32_three_five_product) + (pa_r_hj32_three_five_product))) /\ ((((exists pa_h_hj32_three_five_product_successor. pa_h_hj32_three_five_product_successor + S (pa_s_hj32_three_five_product) = S ((S (S pa_i_hj32_three_five_product)) * pa_v_hj32_three_five_product)) /\ exists pa_q_hj32_three_five_product_successor. pa_u_hj32_three_five_product = pa_q_hj32_three_five_product_successor * S ((S (S pa_i_hj32_three_five_product)) * pa_v_hj32_three_five_product) + (pa_s_hj32_three_five_product))) /\ pa_s_hj32_three_five_product = pa_r_hj32_three_five_product * pa_p_hj32_three_five_product)))))))) -> (exists pa_b_hj32_four_four pa_c_hj32_four_four. ((forall pa_i_hj32_four_four_repeat. (exists pa_lt_hj32_four_four_repeat_bound. pa_lt_hj32_four_four_repeat_bound + S pa_i_hj32_four_four_repeat = 4) -> (((exists pa_h_hj32_four_four_repeat_decoded. pa_h_hj32_four_four_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_four_repeat)) * pa_c_hj32_four_four)) /\ exists pa_q_hj32_four_four_repeat_decoded. pa_b_hj32_four_four = pa_q_hj32_four_four_repeat_decoded * S ((S (pa_i_hj32_four_four_repeat)) * pa_c_hj32_four_four) + (4)))) /\ (exists pa_u_hj32_four_four_product pa_v_hj32_four_four_product. ((((exists pa_h_hj32_four_four_product_start. pa_h_hj32_four_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_four_product)) /\ exists pa_q_hj32_four_four_product_start. pa_u_hj32_four_four_product = pa_q_hj32_four_four_product_start * S ((S (0)) * pa_v_hj32_four_four_product) + (1))) /\ ((((exists pa_h_hj32_four_four_product_terminal. pa_h_hj32_four_four_product_terminal + S (y) = S ((S (4)) * pa_v_hj32_four_four_product)) /\ exists pa_q_hj32_four_four_product_terminal. pa_u_hj32_four_four_product = pa_q_hj32_four_four_product_terminal * S ((S (4)) * pa_v_hj32_four_four_product) + (y))) /\ forall pa_i_hj32_four_four_product. (exists pa_lt_hj32_four_four_product_bound. pa_lt_hj32_four_four_product_bound + S pa_i_hj32_four_four_product = 4) -> exists pa_p_hj32_four_four_product pa_r_hj32_four_four_product pa_s_hj32_four_four_product. ((((exists pa_h_hj32_four_four_product_factor. pa_h_hj32_four_four_product_factor + S (pa_p_hj32_four_four_product) = S ((S (pa_i_hj32_four_four_product)) * pa_c_hj32_four_four)) /\ exists pa_q_hj32_four_four_product_factor. pa_b_hj32_four_four = pa_q_hj32_four_four_product_factor * S ((S (pa_i_hj32_four_four_product)) * pa_c_hj32_four_four) + (pa_p_hj32_four_four_product))) /\ ((((exists pa_h_hj32_four_four_product_partial. pa_h_hj32_four_four_product_partial + S (pa_r_hj32_four_four_product) = S ((S (pa_i_hj32_four_four_product)) * pa_v_hj32_four_four_product)) /\ exists pa_q_hj32_four_four_product_partial. pa_u_hj32_four_four_product = pa_q_hj32_four_four_product_partial * S ((S (pa_i_hj32_four_four_product)) * pa_v_hj32_four_four_product) + (pa_r_hj32_four_four_product))) /\ ((((exists pa_h_hj32_four_four_product_successor. pa_h_hj32_four_four_product_successor + S (pa_s_hj32_four_four_product) = S ((S (S pa_i_hj32_four_four_product)) * pa_v_hj32_four_four_product)) /\ exists pa_q_hj32_four_four_product_successor. pa_u_hj32_four_four_product = pa_q_hj32_four_four_product_successor * S ((S (S pa_i_hj32_four_four_product)) * pa_v_hj32_four_four_product) + (pa_s_hj32_four_four_product))) /\ pa_s_hj32_four_four_product = pa_r_hj32_four_four_product * pa_p_hj32_four_four_product)))))))) -> (exists bqb_le_gap_hj32_three_four_result. bqb_le_gap_hj32_three_four_result + (x) = (y))Proof neighborhood
Direct theorem prerequisites
BT0081 pow_zero BT00SL pow_successor_compose_from_total BT0082 pow_functional BT000B add_mul BT0003 add_assoc BT0002 add_commDirect theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (6)
01Fix variables and assumptionsL1–5
02Establish hthree_zero_anyL6–9
Establish this local claim before using it. It is not an additional assumption.
- L6
have hthree_zero_any : ∃ q. Pow(3,0,q)Definitions: Pow(3,0,q)Original native command in the exact edition - L7
specialize htotal 3 - L8
specialize htotal 0 - L9
exact htotal
03Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
cases hthree_zero_any
04Establish hthree_zero_valueL11–17
05Establish hthree_zeroL18–21
Establish this local claim before using it. It is not an additional assumption.
06Establish hthree_oneL22–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L22
have hthree_one : Pow(3,1,1 · 3)Definitions: Pow(3,1,1 · 3)Original native command in the exact edition - L23
specialize pow_successor_compose_from_total 3 - L24
specialize pow_successor_compose_from_total 0 - L25
specialize pow_successor_compose_from_total 1 - L26
specialize pow_successor_compose_from_total (1 * 3) - L27
apply pow_successor_compose_from_total - L28
exact htotal - L29
exact hthree_zero - L30
refl
07Establish hthree_twoL31–39
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L31
have hthree_two : Pow(3,2,1 · 3 · 3)Definitions: Pow(3,2,1 · 3 · 3)Original native command in the exact edition - L32
specialize pow_successor_compose_from_total 3 - L33
specialize pow_successor_compose_from_total 1 - L34
specialize pow_successor_compose_from_total (1 * 3) - L35
specialize pow_successor_compose_from_total ((1 * 3) * 3) - L36
apply pow_successor_compose_from_total - L37
exact htotal - L38
exact hthree_one - L39
refl
08Establish hthree_threeL40–48
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L40
have hthree_three : Pow(3,3,1 · 3 · 3 · 3)Definitions: Pow(3,3,1 · 3 · 3 · 3)Original native command in the exact edition - L41
specialize pow_successor_compose_from_total 3 - L42
specialize pow_successor_compose_from_total 2 - L43
specialize pow_successor_compose_from_total ((1 * 3) * 3) - L44
specialize pow_successor_compose_from_total (((1 * 3) * 3) * 3) - L45
apply pow_successor_compose_from_total - L46
exact htotal - L47
exact hthree_two - L48
refl
09Establish hthree_fourL49–57
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L49
have hthree_four : Pow(3,4,1 · 3 · 3 · 3 · 3)Definitions: Pow(3,4,1 · 3 · 3 · 3 · 3)Original native command in the exact edition - L50
specialize pow_successor_compose_from_total 3 - L51
specialize pow_successor_compose_from_total 3 - L52
specialize pow_successor_compose_from_total (((1 * 3) * 3) * 3) - L53
specialize pow_successor_compose_from_total ((((1 * 3) * 3) * 3) * 3) - L54
apply pow_successor_compose_from_total - L55
exact htotal - L56
exact hthree_three - L57
refl
10Establish hthree_fiveL58–66
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L58
have hthree_five : Pow(3,5,1 · 3 · 3 · 3 · 3 · 3)Definitions: Pow(3,5,1 · 3 · 3 · 3 · 3 · 3)Original native command in the exact edition - L59
specialize pow_successor_compose_from_total 3 - L60
specialize pow_successor_compose_from_total 4 - L61
specialize pow_successor_compose_from_total ((((1 * 3) * 3) * 3) * 3) - L62
specialize pow_successor_compose_from_total (((((1 * 3) * 3) * 3) * 3) * 3) - L63
apply pow_successor_compose_from_total - L64
exact htotal - L65
exact hthree_four - L66
refl
11Establish hfour_zero_anyL67–70
Establish this local claim before using it. It is not an additional assumption.
- L67
have hfour_zero_any : ∃ q. Pow(4,0,q)Definitions: Pow(4,0,q)Original native command in the exact edition - L68
specialize htotal 4 - L69
specialize htotal 0 - L70
exact htotal
12Separate the logical casesL71–71
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L71
cases hfour_zero_any
13Establish hfour_zero_valueL72–78
14Establish hfour_zeroL79–82
Establish this local claim before using it. It is not an additional assumption.
15Establish hfour_oneL83–91
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L83
have hfour_one : Pow(4,1,1 · 4)Definitions: Pow(4,1,1 · 4)Original native command in the exact edition - L84
specialize pow_successor_compose_from_total 4 - L85
specialize pow_successor_compose_from_total 0 - L86
specialize pow_successor_compose_from_total 1 - L87
specialize pow_successor_compose_from_total (1 * 4) - L88
apply pow_successor_compose_from_total - L89
exact htotal - L90
exact hfour_zero - L91
refl
16Establish hfour_twoL92–100
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L92
have hfour_two : Pow(4,2,1 · 4 · 4)Definitions: Pow(4,2,1 · 4 · 4)Original native command in the exact edition - L93
specialize pow_successor_compose_from_total 4 - L94
specialize pow_successor_compose_from_total 1 - L95
specialize pow_successor_compose_from_total (1 * 4) - L96
specialize pow_successor_compose_from_total ((1 * 4) * 4) - L97
apply pow_successor_compose_from_total - L98
exact htotal - L99
exact hfour_one - L100
refl
17Establish hfour_threeL101–109
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L101
have hfour_three : Pow(4,3,1 · 4 · 4 · 4)Definitions: Pow(4,3,1 · 4 · 4 · 4)Original native command in the exact edition - L102
specialize pow_successor_compose_from_total 4 - L103
specialize pow_successor_compose_from_total 2 - L104
specialize pow_successor_compose_from_total ((1 * 4) * 4) - L105
specialize pow_successor_compose_from_total (((1 * 4) * 4) * 4) - L106
apply pow_successor_compose_from_total - L107
exact htotal - L108
exact hfour_two - L109
refl
18Establish hfour_fourL110–118
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L110
have hfour_four : Pow(4,4,1 · 4 · 4 · 4 · 4)Definitions: Pow(4,4,1 · 4 · 4 · 4 · 4)Original native command in the exact edition - L111
specialize pow_successor_compose_from_total 4 - L112
specialize pow_successor_compose_from_total 3 - L113
specialize pow_successor_compose_from_total (((1 * 4) * 4) * 4) - L114
specialize pow_successor_compose_from_total ((((1 * 4) * 4) * 4) * 4) - L115
apply pow_successor_compose_from_total - L116
exact htotal - L117
exact hfour_three - L118
refl
19Establish hx_valueL119–126
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow functional.
20Establish hy_valueL127–136
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow functional.
21Construct an explicit witnessL137–137
Supply the displayed value, then prove that it has the required property.
- L137
exists 13
22Establish hthree_four_splitL138–144
Establish this local claim before using it. It is not an additional assumption.
23Establish hfour_stepL145–147
24Establish hseventeen_threeL148–150
25Establish hthirteen_fifty_oneL151–160
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add assoc.
- L151
have hthirteen_fifty_one : 13 + 51 = ((1 * 4) * 4) * 4 - L152
norm_num - L153
trans (13 + (((1 * 4) * 4) * 4) * 3) + 51 - L154
symm - L155
specialize add_assoc 13 - L156
specialize add_assoc ((((1 * 4) * 4) * 4) * 3) - L157
specialize add_assoc 51 - L158
apply add_assoc - L159
trans ((((1 * 4) * 4) * 4) * 3 + 13) + 51 - L160
congr
26Use earlier factsL161–163
27Calculate and transport equalitiesL164–165
28Use earlier factsL166–169
Original defined command ledger · 171 lines
- 0001
intro x - 0002
intro y - 0003
intro htotal - 0004
intro hx - 0005
intro hy - 0006
have hthree_zero_any : ∃ q. Pow(3,0,q)Exact native replay line
have hthree_zero_any : exists q. (exists pa_b_hj32_three_zero_any pa_c_hj32_three_zero_any. ((forall pa_i_hj32_three_zero_any_repeat. (exists pa_lt_hj32_three_zero_any_repeat_bound. pa_lt_hj32_three_zero_any_repeat_bound + S pa_i_hj32_three_zero_any_repeat = 0) -> (((exists pa_h_hj32_three_zero_any_repeat_decoded. pa_h_hj32_three_zero_any_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_zero_any_repeat)) * pa_c_hj32_three_zero_any)) /\ exists pa_q_hj32_three_zero_any_repeat_decoded. pa_b_hj32_three_zero_any = pa_q_hj32_three_zero_any_repeat_decoded * S ((S (pa_i_hj32_three_zero_any_repeat)) * pa_c_hj32_three_zero_any) + (3)))) /\ (exists pa_u_hj32_three_zero_any_product pa_v_hj32_three_zero_any_product. ((((exists pa_h_hj32_three_zero_any_product_start. pa_h_hj32_three_zero_any_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_zero_any_product)) /\ exists pa_q_hj32_three_zero_any_product_start. pa_u_hj32_three_zero_any_product = pa_q_hj32_three_zero_any_product_start * S ((S (0)) * pa_v_hj32_three_zero_any_product) + (1))) /\ ((((exists pa_h_hj32_three_zero_any_product_terminal. pa_h_hj32_three_zero_any_product_terminal + S (q) = S ((S (0)) * pa_v_hj32_three_zero_any_product)) /\ exists pa_q_hj32_three_zero_any_product_terminal. pa_u_hj32_three_zero_any_product = pa_q_hj32_three_zero_any_product_terminal * S ((S (0)) * pa_v_hj32_three_zero_any_product) + (q))) /\ forall pa_i_hj32_three_zero_any_product. (exists pa_lt_hj32_three_zero_any_product_bound. pa_lt_hj32_three_zero_any_product_bound + S pa_i_hj32_three_zero_any_product = 0) -> exists pa_p_hj32_three_zero_any_product pa_r_hj32_three_zero_any_product pa_s_hj32_three_zero_any_product. ((((exists pa_h_hj32_three_zero_any_product_factor. pa_h_hj32_three_zero_any_product_factor + S (pa_p_hj32_three_zero_any_product) = S ((S (pa_i_hj32_three_zero_any_product)) * pa_c_hj32_three_zero_any)) /\ exists pa_q_hj32_three_zero_any_product_factor. pa_b_hj32_three_zero_any = pa_q_hj32_three_zero_any_product_factor * S ((S (pa_i_hj32_three_zero_any_product)) * pa_c_hj32_three_zero_any) + (pa_p_hj32_three_zero_any_product))) /\ ((((exists pa_h_hj32_three_zero_any_product_partial. pa_h_hj32_three_zero_any_product_partial + S (pa_r_hj32_three_zero_any_product) = S ((S (pa_i_hj32_three_zero_any_product)) * pa_v_hj32_three_zero_any_product)) /\ exists pa_q_hj32_three_zero_any_product_partial. pa_u_hj32_three_zero_any_product = pa_q_hj32_three_zero_any_product_partial * S ((S (pa_i_hj32_three_zero_any_product)) * pa_v_hj32_three_zero_any_product) + (pa_r_hj32_three_zero_any_product))) /\ ((((exists pa_h_hj32_three_zero_any_product_successor. pa_h_hj32_three_zero_any_product_successor + S (pa_s_hj32_three_zero_any_product) = S ((S (S pa_i_hj32_three_zero_any_product)) * pa_v_hj32_three_zero_any_product)) /\ exists pa_q_hj32_three_zero_any_product_successor. pa_u_hj32_three_zero_any_product = pa_q_hj32_three_zero_any_product_successor * S ((S (S pa_i_hj32_three_zero_any_product)) * pa_v_hj32_three_zero_any_product) + (pa_s_hj32_three_zero_any_product))) /\ pa_s_hj32_three_zero_any_product = pa_r_hj32_three_zero_any_product * pa_p_hj32_three_zero_any_product)))))))) - 0007
specialize htotal 3 - 0008
specialize htotal 0 - 0009
exact htotal - 0010
cases hthree_zero_any - 0011
have hthree_zero_value : x1 = 1 - 0012
specialize pow_zero 3 - 0013
specialize pow_zero 0 - 0014
specialize pow_zero x1 - 0015
apply pow_zero - 0016
refl - 0017
exact hthree_zero_any_witness - 0018
have hthree_zero : Pow(3,0,1)Exact native replay line
have hthree_zero : exists pa_b_hj32_three_zero pa_c_hj32_three_zero. ((forall pa_i_hj32_three_zero_repeat. (exists pa_lt_hj32_three_zero_repeat_bound. pa_lt_hj32_three_zero_repeat_bound + S pa_i_hj32_three_zero_repeat = 0) -> (((exists pa_h_hj32_three_zero_repeat_decoded. pa_h_hj32_three_zero_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_zero_repeat)) * pa_c_hj32_three_zero)) /\ exists pa_q_hj32_three_zero_repeat_decoded. pa_b_hj32_three_zero = pa_q_hj32_three_zero_repeat_decoded * S ((S (pa_i_hj32_three_zero_repeat)) * pa_c_hj32_three_zero) + (3)))) /\ (exists pa_u_hj32_three_zero_product pa_v_hj32_three_zero_product. ((((exists pa_h_hj32_three_zero_product_start. pa_h_hj32_three_zero_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_zero_product)) /\ exists pa_q_hj32_three_zero_product_start. pa_u_hj32_three_zero_product = pa_q_hj32_three_zero_product_start * S ((S (0)) * pa_v_hj32_three_zero_product) + (1))) /\ ((((exists pa_h_hj32_three_zero_product_terminal. pa_h_hj32_three_zero_product_terminal + S (1) = S ((S (0)) * pa_v_hj32_three_zero_product)) /\ exists pa_q_hj32_three_zero_product_terminal. pa_u_hj32_three_zero_product = pa_q_hj32_three_zero_product_terminal * S ((S (0)) * pa_v_hj32_three_zero_product) + (1))) /\ forall pa_i_hj32_three_zero_product. (exists pa_lt_hj32_three_zero_product_bound. pa_lt_hj32_three_zero_product_bound + S pa_i_hj32_three_zero_product = 0) -> exists pa_p_hj32_three_zero_product pa_r_hj32_three_zero_product pa_s_hj32_three_zero_product. ((((exists pa_h_hj32_three_zero_product_factor. pa_h_hj32_three_zero_product_factor + S (pa_p_hj32_three_zero_product) = S ((S (pa_i_hj32_three_zero_product)) * pa_c_hj32_three_zero)) /\ exists pa_q_hj32_three_zero_product_factor. pa_b_hj32_three_zero = pa_q_hj32_three_zero_product_factor * S ((S (pa_i_hj32_three_zero_product)) * pa_c_hj32_three_zero) + (pa_p_hj32_three_zero_product))) /\ ((((exists pa_h_hj32_three_zero_product_partial. pa_h_hj32_three_zero_product_partial + S (pa_r_hj32_three_zero_product) = S ((S (pa_i_hj32_three_zero_product)) * pa_v_hj32_three_zero_product)) /\ exists pa_q_hj32_three_zero_product_partial. pa_u_hj32_three_zero_product = pa_q_hj32_three_zero_product_partial * S ((S (pa_i_hj32_three_zero_product)) * pa_v_hj32_three_zero_product) + (pa_r_hj32_three_zero_product))) /\ ((((exists pa_h_hj32_three_zero_product_successor. pa_h_hj32_three_zero_product_successor + S (pa_s_hj32_three_zero_product) = S ((S (S pa_i_hj32_three_zero_product)) * pa_v_hj32_three_zero_product)) /\ exists pa_q_hj32_three_zero_product_successor. pa_u_hj32_three_zero_product = pa_q_hj32_three_zero_product_successor * S ((S (S pa_i_hj32_three_zero_product)) * pa_v_hj32_three_zero_product) + (pa_s_hj32_three_zero_product))) /\ pa_s_hj32_three_zero_product = pa_r_hj32_three_zero_product * pa_p_hj32_three_zero_product))))))) - 0019
rewrite hthree_zero_value at hthree_zero_any_witness - 0020
rewrite hthree_zero_value at hthree_zero_any_witness - 0021
exact hthree_zero_any_witness - 0022
have hthree_one : Pow(3,1,1 · 3)Exact native replay line
have hthree_one : exists pa_b_hj32_three_one pa_c_hj32_three_one. ((forall pa_i_hj32_three_one_repeat. (exists pa_lt_hj32_three_one_repeat_bound. pa_lt_hj32_three_one_repeat_bound + S pa_i_hj32_three_one_repeat = 1) -> (((exists pa_h_hj32_three_one_repeat_decoded. pa_h_hj32_three_one_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_one_repeat)) * pa_c_hj32_three_one)) /\ exists pa_q_hj32_three_one_repeat_decoded. pa_b_hj32_three_one = pa_q_hj32_three_one_repeat_decoded * S ((S (pa_i_hj32_three_one_repeat)) * pa_c_hj32_three_one) + (3)))) /\ (exists pa_u_hj32_three_one_product pa_v_hj32_three_one_product. ((((exists pa_h_hj32_three_one_product_start. pa_h_hj32_three_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_one_product)) /\ exists pa_q_hj32_three_one_product_start. pa_u_hj32_three_one_product = pa_q_hj32_three_one_product_start * S ((S (0)) * pa_v_hj32_three_one_product) + (1))) /\ ((((exists pa_h_hj32_three_one_product_terminal. pa_h_hj32_three_one_product_terminal + S (1 * 3) = S ((S (1)) * pa_v_hj32_three_one_product)) /\ exists pa_q_hj32_three_one_product_terminal. pa_u_hj32_three_one_product = pa_q_hj32_three_one_product_terminal * S ((S (1)) * pa_v_hj32_three_one_product) + (1 * 3))) /\ forall pa_i_hj32_three_one_product. (exists pa_lt_hj32_three_one_product_bound. pa_lt_hj32_three_one_product_bound + S pa_i_hj32_three_one_product = 1) -> exists pa_p_hj32_three_one_product pa_r_hj32_three_one_product pa_s_hj32_three_one_product. ((((exists pa_h_hj32_three_one_product_factor. pa_h_hj32_three_one_product_factor + S (pa_p_hj32_three_one_product) = S ((S (pa_i_hj32_three_one_product)) * pa_c_hj32_three_one)) /\ exists pa_q_hj32_three_one_product_factor. pa_b_hj32_three_one = pa_q_hj32_three_one_product_factor * S ((S (pa_i_hj32_three_one_product)) * pa_c_hj32_three_one) + (pa_p_hj32_three_one_product))) /\ ((((exists pa_h_hj32_three_one_product_partial. pa_h_hj32_three_one_product_partial + S (pa_r_hj32_three_one_product) = S ((S (pa_i_hj32_three_one_product)) * pa_v_hj32_three_one_product)) /\ exists pa_q_hj32_three_one_product_partial. pa_u_hj32_three_one_product = pa_q_hj32_three_one_product_partial * S ((S (pa_i_hj32_three_one_product)) * pa_v_hj32_three_one_product) + (pa_r_hj32_three_one_product))) /\ ((((exists pa_h_hj32_three_one_product_successor. pa_h_hj32_three_one_product_successor + S (pa_s_hj32_three_one_product) = S ((S (S pa_i_hj32_three_one_product)) * pa_v_hj32_three_one_product)) /\ exists pa_q_hj32_three_one_product_successor. pa_u_hj32_three_one_product = pa_q_hj32_three_one_product_successor * S ((S (S pa_i_hj32_three_one_product)) * pa_v_hj32_three_one_product) + (pa_s_hj32_three_one_product))) /\ pa_s_hj32_three_one_product = pa_r_hj32_three_one_product * pa_p_hj32_three_one_product))))))) - 0023
specialize pow_successor_compose_from_total 3 - 0024
specialize pow_successor_compose_from_total 0 - 0025
specialize pow_successor_compose_from_total 1 - 0026
specialize pow_successor_compose_from_total (1 * 3) - 0027
apply pow_successor_compose_from_total - 0028
exact htotal - 0029
exact hthree_zero - 0030
refl - 0031
have hthree_two : Pow(3,2,1 · 3 · 3)Exact native replay line
have hthree_two : exists pa_b_hj32_three_two pa_c_hj32_three_two. ((forall pa_i_hj32_three_two_repeat. (exists pa_lt_hj32_three_two_repeat_bound. pa_lt_hj32_three_two_repeat_bound + S pa_i_hj32_three_two_repeat = 2) -> (((exists pa_h_hj32_three_two_repeat_decoded. pa_h_hj32_three_two_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_two_repeat)) * pa_c_hj32_three_two)) /\ exists pa_q_hj32_three_two_repeat_decoded. pa_b_hj32_three_two = pa_q_hj32_three_two_repeat_decoded * S ((S (pa_i_hj32_three_two_repeat)) * pa_c_hj32_three_two) + (3)))) /\ (exists pa_u_hj32_three_two_product pa_v_hj32_three_two_product. ((((exists pa_h_hj32_three_two_product_start. pa_h_hj32_three_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_two_product)) /\ exists pa_q_hj32_three_two_product_start. pa_u_hj32_three_two_product = pa_q_hj32_three_two_product_start * S ((S (0)) * pa_v_hj32_three_two_product) + (1))) /\ ((((exists pa_h_hj32_three_two_product_terminal. pa_h_hj32_three_two_product_terminal + S ((1 * 3) * 3) = S ((S (2)) * pa_v_hj32_three_two_product)) /\ exists pa_q_hj32_three_two_product_terminal. pa_u_hj32_three_two_product = pa_q_hj32_three_two_product_terminal * S ((S (2)) * pa_v_hj32_three_two_product) + ((1 * 3) * 3))) /\ forall pa_i_hj32_three_two_product. (exists pa_lt_hj32_three_two_product_bound. pa_lt_hj32_three_two_product_bound + S pa_i_hj32_three_two_product = 2) -> exists pa_p_hj32_three_two_product pa_r_hj32_three_two_product pa_s_hj32_three_two_product. ((((exists pa_h_hj32_three_two_product_factor. pa_h_hj32_three_two_product_factor + S (pa_p_hj32_three_two_product) = S ((S (pa_i_hj32_three_two_product)) * pa_c_hj32_three_two)) /\ exists pa_q_hj32_three_two_product_factor. pa_b_hj32_three_two = pa_q_hj32_three_two_product_factor * S ((S (pa_i_hj32_three_two_product)) * pa_c_hj32_three_two) + (pa_p_hj32_three_two_product))) /\ ((((exists pa_h_hj32_three_two_product_partial. pa_h_hj32_three_two_product_partial + S (pa_r_hj32_three_two_product) = S ((S (pa_i_hj32_three_two_product)) * pa_v_hj32_three_two_product)) /\ exists pa_q_hj32_three_two_product_partial. pa_u_hj32_three_two_product = pa_q_hj32_three_two_product_partial * S ((S (pa_i_hj32_three_two_product)) * pa_v_hj32_three_two_product) + (pa_r_hj32_three_two_product))) /\ ((((exists pa_h_hj32_three_two_product_successor. pa_h_hj32_three_two_product_successor + S (pa_s_hj32_three_two_product) = S ((S (S pa_i_hj32_three_two_product)) * pa_v_hj32_three_two_product)) /\ exists pa_q_hj32_three_two_product_successor. pa_u_hj32_three_two_product = pa_q_hj32_three_two_product_successor * S ((S (S pa_i_hj32_three_two_product)) * pa_v_hj32_three_two_product) + (pa_s_hj32_three_two_product))) /\ pa_s_hj32_three_two_product = pa_r_hj32_three_two_product * pa_p_hj32_three_two_product))))))) - 0032
specialize pow_successor_compose_from_total 3 - 0033
specialize pow_successor_compose_from_total 1 - 0034
specialize pow_successor_compose_from_total (1 * 3) - 0035
specialize pow_successor_compose_from_total ((1 * 3) * 3) - 0036
apply pow_successor_compose_from_total - 0037
exact htotal - 0038
exact hthree_one - 0039
refl - 0040
have hthree_three : Pow(3,3,1 · 3 · 3 · 3)Exact native replay line
have hthree_three : exists pa_b_hj32_three_three pa_c_hj32_three_three. ((forall pa_i_hj32_three_three_repeat. (exists pa_lt_hj32_three_three_repeat_bound. pa_lt_hj32_three_three_repeat_bound + S pa_i_hj32_three_three_repeat = 3) -> (((exists pa_h_hj32_three_three_repeat_decoded. pa_h_hj32_three_three_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_three_repeat)) * pa_c_hj32_three_three)) /\ exists pa_q_hj32_three_three_repeat_decoded. pa_b_hj32_three_three = pa_q_hj32_three_three_repeat_decoded * S ((S (pa_i_hj32_three_three_repeat)) * pa_c_hj32_three_three) + (3)))) /\ (exists pa_u_hj32_three_three_product pa_v_hj32_three_three_product. ((((exists pa_h_hj32_three_three_product_start. pa_h_hj32_three_three_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_three_product)) /\ exists pa_q_hj32_three_three_product_start. pa_u_hj32_three_three_product = pa_q_hj32_three_three_product_start * S ((S (0)) * pa_v_hj32_three_three_product) + (1))) /\ ((((exists pa_h_hj32_three_three_product_terminal. pa_h_hj32_three_three_product_terminal + S (((1 * 3) * 3) * 3) = S ((S (3)) * pa_v_hj32_three_three_product)) /\ exists pa_q_hj32_three_three_product_terminal. pa_u_hj32_three_three_product = pa_q_hj32_three_three_product_terminal * S ((S (3)) * pa_v_hj32_three_three_product) + (((1 * 3) * 3) * 3))) /\ forall pa_i_hj32_three_three_product. (exists pa_lt_hj32_three_three_product_bound. pa_lt_hj32_three_three_product_bound + S pa_i_hj32_three_three_product = 3) -> exists pa_p_hj32_three_three_product pa_r_hj32_three_three_product pa_s_hj32_three_three_product. ((((exists pa_h_hj32_three_three_product_factor. pa_h_hj32_three_three_product_factor + S (pa_p_hj32_three_three_product) = S ((S (pa_i_hj32_three_three_product)) * pa_c_hj32_three_three)) /\ exists pa_q_hj32_three_three_product_factor. pa_b_hj32_three_three = pa_q_hj32_three_three_product_factor * S ((S (pa_i_hj32_three_three_product)) * pa_c_hj32_three_three) + (pa_p_hj32_three_three_product))) /\ ((((exists pa_h_hj32_three_three_product_partial. pa_h_hj32_three_three_product_partial + S (pa_r_hj32_three_three_product) = S ((S (pa_i_hj32_three_three_product)) * pa_v_hj32_three_three_product)) /\ exists pa_q_hj32_three_three_product_partial. pa_u_hj32_three_three_product = pa_q_hj32_three_three_product_partial * S ((S (pa_i_hj32_three_three_product)) * pa_v_hj32_three_three_product) + (pa_r_hj32_three_three_product))) /\ ((((exists pa_h_hj32_three_three_product_successor. pa_h_hj32_three_three_product_successor + S (pa_s_hj32_three_three_product) = S ((S (S pa_i_hj32_three_three_product)) * pa_v_hj32_three_three_product)) /\ exists pa_q_hj32_three_three_product_successor. pa_u_hj32_three_three_product = pa_q_hj32_three_three_product_successor * S ((S (S pa_i_hj32_three_three_product)) * pa_v_hj32_three_three_product) + (pa_s_hj32_three_three_product))) /\ pa_s_hj32_three_three_product = pa_r_hj32_three_three_product * pa_p_hj32_three_three_product))))))) - 0041
specialize pow_successor_compose_from_total 3 - 0042
specialize pow_successor_compose_from_total 2 - 0043
specialize pow_successor_compose_from_total ((1 * 3) * 3) - 0044
specialize pow_successor_compose_from_total (((1 * 3) * 3) * 3) - 0045
apply pow_successor_compose_from_total - 0046
exact htotal - 0047
exact hthree_two - 0048
refl - 0049
have hthree_four : Pow(3,4,1 · 3 · 3 · 3 · 3)Exact native replay line
have hthree_four : exists pa_b_hj32_three_four pa_c_hj32_three_four. ((forall pa_i_hj32_three_four_repeat. (exists pa_lt_hj32_three_four_repeat_bound. pa_lt_hj32_three_four_repeat_bound + S pa_i_hj32_three_four_repeat = 4) -> (((exists pa_h_hj32_three_four_repeat_decoded. pa_h_hj32_three_four_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_four_repeat)) * pa_c_hj32_three_four)) /\ exists pa_q_hj32_three_four_repeat_decoded. pa_b_hj32_three_four = pa_q_hj32_three_four_repeat_decoded * S ((S (pa_i_hj32_three_four_repeat)) * pa_c_hj32_three_four) + (3)))) /\ (exists pa_u_hj32_three_four_product pa_v_hj32_three_four_product. ((((exists pa_h_hj32_three_four_product_start. pa_h_hj32_three_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_four_product)) /\ exists pa_q_hj32_three_four_product_start. pa_u_hj32_three_four_product = pa_q_hj32_three_four_product_start * S ((S (0)) * pa_v_hj32_three_four_product) + (1))) /\ ((((exists pa_h_hj32_three_four_product_terminal. pa_h_hj32_three_four_product_terminal + S ((((1 * 3) * 3) * 3) * 3) = S ((S (4)) * pa_v_hj32_three_four_product)) /\ exists pa_q_hj32_three_four_product_terminal. pa_u_hj32_three_four_product = pa_q_hj32_three_four_product_terminal * S ((S (4)) * pa_v_hj32_three_four_product) + ((((1 * 3) * 3) * 3) * 3))) /\ forall pa_i_hj32_three_four_product. (exists pa_lt_hj32_three_four_product_bound. pa_lt_hj32_three_four_product_bound + S pa_i_hj32_three_four_product = 4) -> exists pa_p_hj32_three_four_product pa_r_hj32_three_four_product pa_s_hj32_three_four_product. ((((exists pa_h_hj32_three_four_product_factor. pa_h_hj32_three_four_product_factor + S (pa_p_hj32_three_four_product) = S ((S (pa_i_hj32_three_four_product)) * pa_c_hj32_three_four)) /\ exists pa_q_hj32_three_four_product_factor. pa_b_hj32_three_four = pa_q_hj32_three_four_product_factor * S ((S (pa_i_hj32_three_four_product)) * pa_c_hj32_three_four) + (pa_p_hj32_three_four_product))) /\ ((((exists pa_h_hj32_three_four_product_partial. pa_h_hj32_three_four_product_partial + S (pa_r_hj32_three_four_product) = S ((S (pa_i_hj32_three_four_product)) * pa_v_hj32_three_four_product)) /\ exists pa_q_hj32_three_four_product_partial. pa_u_hj32_three_four_product = pa_q_hj32_three_four_product_partial * S ((S (pa_i_hj32_three_four_product)) * pa_v_hj32_three_four_product) + (pa_r_hj32_three_four_product))) /\ ((((exists pa_h_hj32_three_four_product_successor. pa_h_hj32_three_four_product_successor + S (pa_s_hj32_three_four_product) = S ((S (S pa_i_hj32_three_four_product)) * pa_v_hj32_three_four_product)) /\ exists pa_q_hj32_three_four_product_successor. pa_u_hj32_three_four_product = pa_q_hj32_three_four_product_successor * S ((S (S pa_i_hj32_three_four_product)) * pa_v_hj32_three_four_product) + (pa_s_hj32_three_four_product))) /\ pa_s_hj32_three_four_product = pa_r_hj32_three_four_product * pa_p_hj32_three_four_product))))))) - 0050
specialize pow_successor_compose_from_total 3 - 0051
specialize pow_successor_compose_from_total 3 - 0052
specialize pow_successor_compose_from_total (((1 * 3) * 3) * 3) - 0053
specialize pow_successor_compose_from_total ((((1 * 3) * 3) * 3) * 3) - 0054
apply pow_successor_compose_from_total - 0055
exact htotal - 0056
exact hthree_three - 0057
refl - 0058
have hthree_five : Pow(3,5,1 · 3 · 3 · 3 · 3 · 3)Exact native replay line
have hthree_five : exists pa_b_hj32_three_five_exact pa_c_hj32_three_five_exact. ((forall pa_i_hj32_three_five_exact_repeat. (exists pa_lt_hj32_three_five_exact_repeat_bound. pa_lt_hj32_three_five_exact_repeat_bound + S pa_i_hj32_three_five_exact_repeat = 5) -> (((exists pa_h_hj32_three_five_exact_repeat_decoded. pa_h_hj32_three_five_exact_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_five_exact_repeat)) * pa_c_hj32_three_five_exact)) /\ exists pa_q_hj32_three_five_exact_repeat_decoded. pa_b_hj32_three_five_exact = pa_q_hj32_three_five_exact_repeat_decoded * S ((S (pa_i_hj32_three_five_exact_repeat)) * pa_c_hj32_three_five_exact) + (3)))) /\ (exists pa_u_hj32_three_five_exact_product pa_v_hj32_three_five_exact_product. ((((exists pa_h_hj32_three_five_exact_product_start. pa_h_hj32_three_five_exact_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_five_exact_product)) /\ exists pa_q_hj32_three_five_exact_product_start. pa_u_hj32_three_five_exact_product = pa_q_hj32_three_five_exact_product_start * S ((S (0)) * pa_v_hj32_three_five_exact_product) + (1))) /\ ((((exists pa_h_hj32_three_five_exact_product_terminal. pa_h_hj32_three_five_exact_product_terminal + S (((((1 * 3) * 3) * 3) * 3) * 3) = S ((S (5)) * pa_v_hj32_three_five_exact_product)) /\ exists pa_q_hj32_three_five_exact_product_terminal. pa_u_hj32_three_five_exact_product = pa_q_hj32_three_five_exact_product_terminal * S ((S (5)) * pa_v_hj32_three_five_exact_product) + (((((1 * 3) * 3) * 3) * 3) * 3))) /\ forall pa_i_hj32_three_five_exact_product. (exists pa_lt_hj32_three_five_exact_product_bound. pa_lt_hj32_three_five_exact_product_bound + S pa_i_hj32_three_five_exact_product = 5) -> exists pa_p_hj32_three_five_exact_product pa_r_hj32_three_five_exact_product pa_s_hj32_three_five_exact_product. ((((exists pa_h_hj32_three_five_exact_product_factor. pa_h_hj32_three_five_exact_product_factor + S (pa_p_hj32_three_five_exact_product) = S ((S (pa_i_hj32_three_five_exact_product)) * pa_c_hj32_three_five_exact)) /\ exists pa_q_hj32_three_five_exact_product_factor. pa_b_hj32_three_five_exact = pa_q_hj32_three_five_exact_product_factor * S ((S (pa_i_hj32_three_five_exact_product)) * pa_c_hj32_three_five_exact) + (pa_p_hj32_three_five_exact_product))) /\ ((((exists pa_h_hj32_three_five_exact_product_partial. pa_h_hj32_three_five_exact_product_partial + S (pa_r_hj32_three_five_exact_product) = S ((S (pa_i_hj32_three_five_exact_product)) * pa_v_hj32_three_five_exact_product)) /\ exists pa_q_hj32_three_five_exact_product_partial. pa_u_hj32_three_five_exact_product = pa_q_hj32_three_five_exact_product_partial * S ((S (pa_i_hj32_three_five_exact_product)) * pa_v_hj32_three_five_exact_product) + (pa_r_hj32_three_five_exact_product))) /\ ((((exists pa_h_hj32_three_five_exact_product_successor. pa_h_hj32_three_five_exact_product_successor + S (pa_s_hj32_three_five_exact_product) = S ((S (S pa_i_hj32_three_five_exact_product)) * pa_v_hj32_three_five_exact_product)) /\ exists pa_q_hj32_three_five_exact_product_successor. pa_u_hj32_three_five_exact_product = pa_q_hj32_three_five_exact_product_successor * S ((S (S pa_i_hj32_three_five_exact_product)) * pa_v_hj32_three_five_exact_product) + (pa_s_hj32_three_five_exact_product))) /\ pa_s_hj32_three_five_exact_product = pa_r_hj32_three_five_exact_product * pa_p_hj32_three_five_exact_product))))))) - 0059
specialize pow_successor_compose_from_total 3 - 0060
specialize pow_successor_compose_from_total 4 - 0061
specialize pow_successor_compose_from_total ((((1 * 3) * 3) * 3) * 3) - 0062
specialize pow_successor_compose_from_total (((((1 * 3) * 3) * 3) * 3) * 3) - 0063
apply pow_successor_compose_from_total - 0064
exact htotal - 0065
exact hthree_four - 0066
refl - 0067
have hfour_zero_any : ∃ q. Pow(4,0,q)Exact native replay line
have hfour_zero_any : exists q. (exists pa_b_hj32_four_zero_any pa_c_hj32_four_zero_any. ((forall pa_i_hj32_four_zero_any_repeat. (exists pa_lt_hj32_four_zero_any_repeat_bound. pa_lt_hj32_four_zero_any_repeat_bound + S pa_i_hj32_four_zero_any_repeat = 0) -> (((exists pa_h_hj32_four_zero_any_repeat_decoded. pa_h_hj32_four_zero_any_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_zero_any_repeat)) * pa_c_hj32_four_zero_any)) /\ exists pa_q_hj32_four_zero_any_repeat_decoded. pa_b_hj32_four_zero_any = pa_q_hj32_four_zero_any_repeat_decoded * S ((S (pa_i_hj32_four_zero_any_repeat)) * pa_c_hj32_four_zero_any) + (4)))) /\ (exists pa_u_hj32_four_zero_any_product pa_v_hj32_four_zero_any_product. ((((exists pa_h_hj32_four_zero_any_product_start. pa_h_hj32_four_zero_any_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_zero_any_product)) /\ exists pa_q_hj32_four_zero_any_product_start. pa_u_hj32_four_zero_any_product = pa_q_hj32_four_zero_any_product_start * S ((S (0)) * pa_v_hj32_four_zero_any_product) + (1))) /\ ((((exists pa_h_hj32_four_zero_any_product_terminal. pa_h_hj32_four_zero_any_product_terminal + S (q) = S ((S (0)) * pa_v_hj32_four_zero_any_product)) /\ exists pa_q_hj32_four_zero_any_product_terminal. pa_u_hj32_four_zero_any_product = pa_q_hj32_four_zero_any_product_terminal * S ((S (0)) * pa_v_hj32_four_zero_any_product) + (q))) /\ forall pa_i_hj32_four_zero_any_product. (exists pa_lt_hj32_four_zero_any_product_bound. pa_lt_hj32_four_zero_any_product_bound + S pa_i_hj32_four_zero_any_product = 0) -> exists pa_p_hj32_four_zero_any_product pa_r_hj32_four_zero_any_product pa_s_hj32_four_zero_any_product. ((((exists pa_h_hj32_four_zero_any_product_factor. pa_h_hj32_four_zero_any_product_factor + S (pa_p_hj32_four_zero_any_product) = S ((S (pa_i_hj32_four_zero_any_product)) * pa_c_hj32_four_zero_any)) /\ exists pa_q_hj32_four_zero_any_product_factor. pa_b_hj32_four_zero_any = pa_q_hj32_four_zero_any_product_factor * S ((S (pa_i_hj32_four_zero_any_product)) * pa_c_hj32_four_zero_any) + (pa_p_hj32_four_zero_any_product))) /\ ((((exists pa_h_hj32_four_zero_any_product_partial. pa_h_hj32_four_zero_any_product_partial + S (pa_r_hj32_four_zero_any_product) = S ((S (pa_i_hj32_four_zero_any_product)) * pa_v_hj32_four_zero_any_product)) /\ exists pa_q_hj32_four_zero_any_product_partial. pa_u_hj32_four_zero_any_product = pa_q_hj32_four_zero_any_product_partial * S ((S (pa_i_hj32_four_zero_any_product)) * pa_v_hj32_four_zero_any_product) + (pa_r_hj32_four_zero_any_product))) /\ ((((exists pa_h_hj32_four_zero_any_product_successor. pa_h_hj32_four_zero_any_product_successor + S (pa_s_hj32_four_zero_any_product) = S ((S (S pa_i_hj32_four_zero_any_product)) * pa_v_hj32_four_zero_any_product)) /\ exists pa_q_hj32_four_zero_any_product_successor. pa_u_hj32_four_zero_any_product = pa_q_hj32_four_zero_any_product_successor * S ((S (S pa_i_hj32_four_zero_any_product)) * pa_v_hj32_four_zero_any_product) + (pa_s_hj32_four_zero_any_product))) /\ pa_s_hj32_four_zero_any_product = pa_r_hj32_four_zero_any_product * pa_p_hj32_four_zero_any_product)))))))) - 0068
specialize htotal 4 - 0069
specialize htotal 0 - 0070
exact htotal - 0071
cases hfour_zero_any - 0072
have hfour_zero_value : x2 = 1 - 0073
specialize pow_zero 4 - 0074
specialize pow_zero 0 - 0075
specialize pow_zero x2 - 0076
apply pow_zero - 0077
refl - 0078
exact hfour_zero_any_witness - 0079
have hfour_zero : Pow(4,0,1)Exact native replay line
have hfour_zero : exists pa_b_hj32_four_zero pa_c_hj32_four_zero. ((forall pa_i_hj32_four_zero_repeat. (exists pa_lt_hj32_four_zero_repeat_bound. pa_lt_hj32_four_zero_repeat_bound + S pa_i_hj32_four_zero_repeat = 0) -> (((exists pa_h_hj32_four_zero_repeat_decoded. pa_h_hj32_four_zero_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_zero_repeat)) * pa_c_hj32_four_zero)) /\ exists pa_q_hj32_four_zero_repeat_decoded. pa_b_hj32_four_zero = pa_q_hj32_four_zero_repeat_decoded * S ((S (pa_i_hj32_four_zero_repeat)) * pa_c_hj32_four_zero) + (4)))) /\ (exists pa_u_hj32_four_zero_product pa_v_hj32_four_zero_product. ((((exists pa_h_hj32_four_zero_product_start. pa_h_hj32_four_zero_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_zero_product)) /\ exists pa_q_hj32_four_zero_product_start. pa_u_hj32_four_zero_product = pa_q_hj32_four_zero_product_start * S ((S (0)) * pa_v_hj32_four_zero_product) + (1))) /\ ((((exists pa_h_hj32_four_zero_product_terminal. pa_h_hj32_four_zero_product_terminal + S (1) = S ((S (0)) * pa_v_hj32_four_zero_product)) /\ exists pa_q_hj32_four_zero_product_terminal. pa_u_hj32_four_zero_product = pa_q_hj32_four_zero_product_terminal * S ((S (0)) * pa_v_hj32_four_zero_product) + (1))) /\ forall pa_i_hj32_four_zero_product. (exists pa_lt_hj32_four_zero_product_bound. pa_lt_hj32_four_zero_product_bound + S pa_i_hj32_four_zero_product = 0) -> exists pa_p_hj32_four_zero_product pa_r_hj32_four_zero_product pa_s_hj32_four_zero_product. ((((exists pa_h_hj32_four_zero_product_factor. pa_h_hj32_four_zero_product_factor + S (pa_p_hj32_four_zero_product) = S ((S (pa_i_hj32_four_zero_product)) * pa_c_hj32_four_zero)) /\ exists pa_q_hj32_four_zero_product_factor. pa_b_hj32_four_zero = pa_q_hj32_four_zero_product_factor * S ((S (pa_i_hj32_four_zero_product)) * pa_c_hj32_four_zero) + (pa_p_hj32_four_zero_product))) /\ ((((exists pa_h_hj32_four_zero_product_partial. pa_h_hj32_four_zero_product_partial + S (pa_r_hj32_four_zero_product) = S ((S (pa_i_hj32_four_zero_product)) * pa_v_hj32_four_zero_product)) /\ exists pa_q_hj32_four_zero_product_partial. pa_u_hj32_four_zero_product = pa_q_hj32_four_zero_product_partial * S ((S (pa_i_hj32_four_zero_product)) * pa_v_hj32_four_zero_product) + (pa_r_hj32_four_zero_product))) /\ ((((exists pa_h_hj32_four_zero_product_successor. pa_h_hj32_four_zero_product_successor + S (pa_s_hj32_four_zero_product) = S ((S (S pa_i_hj32_four_zero_product)) * pa_v_hj32_four_zero_product)) /\ exists pa_q_hj32_four_zero_product_successor. pa_u_hj32_four_zero_product = pa_q_hj32_four_zero_product_successor * S ((S (S pa_i_hj32_four_zero_product)) * pa_v_hj32_four_zero_product) + (pa_s_hj32_four_zero_product))) /\ pa_s_hj32_four_zero_product = pa_r_hj32_four_zero_product * pa_p_hj32_four_zero_product))))))) - 0080
rewrite hfour_zero_value at hfour_zero_any_witness - 0081
rewrite hfour_zero_value at hfour_zero_any_witness - 0082
exact hfour_zero_any_witness - 0083
have hfour_one : Pow(4,1,1 · 4)Exact native replay line
have hfour_one : exists pa_b_hj32_four_one pa_c_hj32_four_one. ((forall pa_i_hj32_four_one_repeat. (exists pa_lt_hj32_four_one_repeat_bound. pa_lt_hj32_four_one_repeat_bound + S pa_i_hj32_four_one_repeat = 1) -> (((exists pa_h_hj32_four_one_repeat_decoded. pa_h_hj32_four_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_one_repeat)) * pa_c_hj32_four_one)) /\ exists pa_q_hj32_four_one_repeat_decoded. pa_b_hj32_four_one = pa_q_hj32_four_one_repeat_decoded * S ((S (pa_i_hj32_four_one_repeat)) * pa_c_hj32_four_one) + (4)))) /\ (exists pa_u_hj32_four_one_product pa_v_hj32_four_one_product. ((((exists pa_h_hj32_four_one_product_start. pa_h_hj32_four_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_one_product)) /\ exists pa_q_hj32_four_one_product_start. pa_u_hj32_four_one_product = pa_q_hj32_four_one_product_start * S ((S (0)) * pa_v_hj32_four_one_product) + (1))) /\ ((((exists pa_h_hj32_four_one_product_terminal. pa_h_hj32_four_one_product_terminal + S (1 * 4) = S ((S (1)) * pa_v_hj32_four_one_product)) /\ exists pa_q_hj32_four_one_product_terminal. pa_u_hj32_four_one_product = pa_q_hj32_four_one_product_terminal * S ((S (1)) * pa_v_hj32_four_one_product) + (1 * 4))) /\ forall pa_i_hj32_four_one_product. (exists pa_lt_hj32_four_one_product_bound. pa_lt_hj32_four_one_product_bound + S pa_i_hj32_four_one_product = 1) -> exists pa_p_hj32_four_one_product pa_r_hj32_four_one_product pa_s_hj32_four_one_product. ((((exists pa_h_hj32_four_one_product_factor. pa_h_hj32_four_one_product_factor + S (pa_p_hj32_four_one_product) = S ((S (pa_i_hj32_four_one_product)) * pa_c_hj32_four_one)) /\ exists pa_q_hj32_four_one_product_factor. pa_b_hj32_four_one = pa_q_hj32_four_one_product_factor * S ((S (pa_i_hj32_four_one_product)) * pa_c_hj32_four_one) + (pa_p_hj32_four_one_product))) /\ ((((exists pa_h_hj32_four_one_product_partial. pa_h_hj32_four_one_product_partial + S (pa_r_hj32_four_one_product) = S ((S (pa_i_hj32_four_one_product)) * pa_v_hj32_four_one_product)) /\ exists pa_q_hj32_four_one_product_partial. pa_u_hj32_four_one_product = pa_q_hj32_four_one_product_partial * S ((S (pa_i_hj32_four_one_product)) * pa_v_hj32_four_one_product) + (pa_r_hj32_four_one_product))) /\ ((((exists pa_h_hj32_four_one_product_successor. pa_h_hj32_four_one_product_successor + S (pa_s_hj32_four_one_product) = S ((S (S pa_i_hj32_four_one_product)) * pa_v_hj32_four_one_product)) /\ exists pa_q_hj32_four_one_product_successor. pa_u_hj32_four_one_product = pa_q_hj32_four_one_product_successor * S ((S (S pa_i_hj32_four_one_product)) * pa_v_hj32_four_one_product) + (pa_s_hj32_four_one_product))) /\ pa_s_hj32_four_one_product = pa_r_hj32_four_one_product * pa_p_hj32_four_one_product))))))) - 0084
specialize pow_successor_compose_from_total 4 - 0085
specialize pow_successor_compose_from_total 0 - 0086
specialize pow_successor_compose_from_total 1 - 0087
specialize pow_successor_compose_from_total (1 * 4) - 0088
apply pow_successor_compose_from_total - 0089
exact htotal - 0090
exact hfour_zero - 0091
refl - 0092
have hfour_two : Pow(4,2,1 · 4 · 4)Exact native replay line
have hfour_two : exists pa_b_hj32_four_two pa_c_hj32_four_two. ((forall pa_i_hj32_four_two_repeat. (exists pa_lt_hj32_four_two_repeat_bound. pa_lt_hj32_four_two_repeat_bound + S pa_i_hj32_four_two_repeat = 2) -> (((exists pa_h_hj32_four_two_repeat_decoded. pa_h_hj32_four_two_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_two_repeat)) * pa_c_hj32_four_two)) /\ exists pa_q_hj32_four_two_repeat_decoded. pa_b_hj32_four_two = pa_q_hj32_four_two_repeat_decoded * S ((S (pa_i_hj32_four_two_repeat)) * pa_c_hj32_four_two) + (4)))) /\ (exists pa_u_hj32_four_two_product pa_v_hj32_four_two_product. ((((exists pa_h_hj32_four_two_product_start. pa_h_hj32_four_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_two_product)) /\ exists pa_q_hj32_four_two_product_start. pa_u_hj32_four_two_product = pa_q_hj32_four_two_product_start * S ((S (0)) * pa_v_hj32_four_two_product) + (1))) /\ ((((exists pa_h_hj32_four_two_product_terminal. pa_h_hj32_four_two_product_terminal + S ((1 * 4) * 4) = S ((S (2)) * pa_v_hj32_four_two_product)) /\ exists pa_q_hj32_four_two_product_terminal. pa_u_hj32_four_two_product = pa_q_hj32_four_two_product_terminal * S ((S (2)) * pa_v_hj32_four_two_product) + ((1 * 4) * 4))) /\ forall pa_i_hj32_four_two_product. (exists pa_lt_hj32_four_two_product_bound. pa_lt_hj32_four_two_product_bound + S pa_i_hj32_four_two_product = 2) -> exists pa_p_hj32_four_two_product pa_r_hj32_four_two_product pa_s_hj32_four_two_product. ((((exists pa_h_hj32_four_two_product_factor. pa_h_hj32_four_two_product_factor + S (pa_p_hj32_four_two_product) = S ((S (pa_i_hj32_four_two_product)) * pa_c_hj32_four_two)) /\ exists pa_q_hj32_four_two_product_factor. pa_b_hj32_four_two = pa_q_hj32_four_two_product_factor * S ((S (pa_i_hj32_four_two_product)) * pa_c_hj32_four_two) + (pa_p_hj32_four_two_product))) /\ ((((exists pa_h_hj32_four_two_product_partial. pa_h_hj32_four_two_product_partial + S (pa_r_hj32_four_two_product) = S ((S (pa_i_hj32_four_two_product)) * pa_v_hj32_four_two_product)) /\ exists pa_q_hj32_four_two_product_partial. pa_u_hj32_four_two_product = pa_q_hj32_four_two_product_partial * S ((S (pa_i_hj32_four_two_product)) * pa_v_hj32_four_two_product) + (pa_r_hj32_four_two_product))) /\ ((((exists pa_h_hj32_four_two_product_successor. pa_h_hj32_four_two_product_successor + S (pa_s_hj32_four_two_product) = S ((S (S pa_i_hj32_four_two_product)) * pa_v_hj32_four_two_product)) /\ exists pa_q_hj32_four_two_product_successor. pa_u_hj32_four_two_product = pa_q_hj32_four_two_product_successor * S ((S (S pa_i_hj32_four_two_product)) * pa_v_hj32_four_two_product) + (pa_s_hj32_four_two_product))) /\ pa_s_hj32_four_two_product = pa_r_hj32_four_two_product * pa_p_hj32_four_two_product))))))) - 0093
specialize pow_successor_compose_from_total 4 - 0094
specialize pow_successor_compose_from_total 1 - 0095
specialize pow_successor_compose_from_total (1 * 4) - 0096
specialize pow_successor_compose_from_total ((1 * 4) * 4) - 0097
apply pow_successor_compose_from_total - 0098
exact htotal - 0099
exact hfour_one - 0100
refl - 0101
have hfour_three : Pow(4,3,1 · 4 · 4 · 4)Exact native replay line
have hfour_three : exists pa_b_hj32_four_three pa_c_hj32_four_three. ((forall pa_i_hj32_four_three_repeat. (exists pa_lt_hj32_four_three_repeat_bound. pa_lt_hj32_four_three_repeat_bound + S pa_i_hj32_four_three_repeat = 3) -> (((exists pa_h_hj32_four_three_repeat_decoded. pa_h_hj32_four_three_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_three_repeat)) * pa_c_hj32_four_three)) /\ exists pa_q_hj32_four_three_repeat_decoded. pa_b_hj32_four_three = pa_q_hj32_four_three_repeat_decoded * S ((S (pa_i_hj32_four_three_repeat)) * pa_c_hj32_four_three) + (4)))) /\ (exists pa_u_hj32_four_three_product pa_v_hj32_four_three_product. ((((exists pa_h_hj32_four_three_product_start. pa_h_hj32_four_three_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_three_product)) /\ exists pa_q_hj32_four_three_product_start. pa_u_hj32_four_three_product = pa_q_hj32_four_three_product_start * S ((S (0)) * pa_v_hj32_four_three_product) + (1))) /\ ((((exists pa_h_hj32_four_three_product_terminal. pa_h_hj32_four_three_product_terminal + S (((1 * 4) * 4) * 4) = S ((S (3)) * pa_v_hj32_four_three_product)) /\ exists pa_q_hj32_four_three_product_terminal. pa_u_hj32_four_three_product = pa_q_hj32_four_three_product_terminal * S ((S (3)) * pa_v_hj32_four_three_product) + (((1 * 4) * 4) * 4))) /\ forall pa_i_hj32_four_three_product. (exists pa_lt_hj32_four_three_product_bound. pa_lt_hj32_four_three_product_bound + S pa_i_hj32_four_three_product = 3) -> exists pa_p_hj32_four_three_product pa_r_hj32_four_three_product pa_s_hj32_four_three_product. ((((exists pa_h_hj32_four_three_product_factor. pa_h_hj32_four_three_product_factor + S (pa_p_hj32_four_three_product) = S ((S (pa_i_hj32_four_three_product)) * pa_c_hj32_four_three)) /\ exists pa_q_hj32_four_three_product_factor. pa_b_hj32_four_three = pa_q_hj32_four_three_product_factor * S ((S (pa_i_hj32_four_three_product)) * pa_c_hj32_four_three) + (pa_p_hj32_four_three_product))) /\ ((((exists pa_h_hj32_four_three_product_partial. pa_h_hj32_four_three_product_partial + S (pa_r_hj32_four_three_product) = S ((S (pa_i_hj32_four_three_product)) * pa_v_hj32_four_three_product)) /\ exists pa_q_hj32_four_three_product_partial. pa_u_hj32_four_three_product = pa_q_hj32_four_three_product_partial * S ((S (pa_i_hj32_four_three_product)) * pa_v_hj32_four_three_product) + (pa_r_hj32_four_three_product))) /\ ((((exists pa_h_hj32_four_three_product_successor. pa_h_hj32_four_three_product_successor + S (pa_s_hj32_four_three_product) = S ((S (S pa_i_hj32_four_three_product)) * pa_v_hj32_four_three_product)) /\ exists pa_q_hj32_four_three_product_successor. pa_u_hj32_four_three_product = pa_q_hj32_four_three_product_successor * S ((S (S pa_i_hj32_four_three_product)) * pa_v_hj32_four_three_product) + (pa_s_hj32_four_three_product))) /\ pa_s_hj32_four_three_product = pa_r_hj32_four_three_product * pa_p_hj32_four_three_product))))))) - 0102
specialize pow_successor_compose_from_total 4 - 0103
specialize pow_successor_compose_from_total 2 - 0104
specialize pow_successor_compose_from_total ((1 * 4) * 4) - 0105
specialize pow_successor_compose_from_total (((1 * 4) * 4) * 4) - 0106
apply pow_successor_compose_from_total - 0107
exact htotal - 0108
exact hfour_two - 0109
refl - 0110
have hfour_four : Pow(4,4,1 · 4 · 4 · 4 · 4)Exact native replay line
have hfour_four : exists pa_b_hj32_four_four_exact pa_c_hj32_four_four_exact. ((forall pa_i_hj32_four_four_exact_repeat. (exists pa_lt_hj32_four_four_exact_repeat_bound. pa_lt_hj32_four_four_exact_repeat_bound + S pa_i_hj32_four_four_exact_repeat = 4) -> (((exists pa_h_hj32_four_four_exact_repeat_decoded. pa_h_hj32_four_four_exact_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_four_exact_repeat)) * pa_c_hj32_four_four_exact)) /\ exists pa_q_hj32_four_four_exact_repeat_decoded. pa_b_hj32_four_four_exact = pa_q_hj32_four_four_exact_repeat_decoded * S ((S (pa_i_hj32_four_four_exact_repeat)) * pa_c_hj32_four_four_exact) + (4)))) /\ (exists pa_u_hj32_four_four_exact_product pa_v_hj32_four_four_exact_product. ((((exists pa_h_hj32_four_four_exact_product_start. pa_h_hj32_four_four_exact_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_four_exact_product)) /\ exists pa_q_hj32_four_four_exact_product_start. pa_u_hj32_four_four_exact_product = pa_q_hj32_four_four_exact_product_start * S ((S (0)) * pa_v_hj32_four_four_exact_product) + (1))) /\ ((((exists pa_h_hj32_four_four_exact_product_terminal. pa_h_hj32_four_four_exact_product_terminal + S ((((1 * 4) * 4) * 4) * 4) = S ((S (4)) * pa_v_hj32_four_four_exact_product)) /\ exists pa_q_hj32_four_four_exact_product_terminal. pa_u_hj32_four_four_exact_product = pa_q_hj32_four_four_exact_product_terminal * S ((S (4)) * pa_v_hj32_four_four_exact_product) + ((((1 * 4) * 4) * 4) * 4))) /\ forall pa_i_hj32_four_four_exact_product. (exists pa_lt_hj32_four_four_exact_product_bound. pa_lt_hj32_four_four_exact_product_bound + S pa_i_hj32_four_four_exact_product = 4) -> exists pa_p_hj32_four_four_exact_product pa_r_hj32_four_four_exact_product pa_s_hj32_four_four_exact_product. ((((exists pa_h_hj32_four_four_exact_product_factor. pa_h_hj32_four_four_exact_product_factor + S (pa_p_hj32_four_four_exact_product) = S ((S (pa_i_hj32_four_four_exact_product)) * pa_c_hj32_four_four_exact)) /\ exists pa_q_hj32_four_four_exact_product_factor. pa_b_hj32_four_four_exact = pa_q_hj32_four_four_exact_product_factor * S ((S (pa_i_hj32_four_four_exact_product)) * pa_c_hj32_four_four_exact) + (pa_p_hj32_four_four_exact_product))) /\ ((((exists pa_h_hj32_four_four_exact_product_partial. pa_h_hj32_four_four_exact_product_partial + S (pa_r_hj32_four_four_exact_product) = S ((S (pa_i_hj32_four_four_exact_product)) * pa_v_hj32_four_four_exact_product)) /\ exists pa_q_hj32_four_four_exact_product_partial. pa_u_hj32_four_four_exact_product = pa_q_hj32_four_four_exact_product_partial * S ((S (pa_i_hj32_four_four_exact_product)) * pa_v_hj32_four_four_exact_product) + (pa_r_hj32_four_four_exact_product))) /\ ((((exists pa_h_hj32_four_four_exact_product_successor. pa_h_hj32_four_four_exact_product_successor + S (pa_s_hj32_four_four_exact_product) = S ((S (S pa_i_hj32_four_four_exact_product)) * pa_v_hj32_four_four_exact_product)) /\ exists pa_q_hj32_four_four_exact_product_successor. pa_u_hj32_four_four_exact_product = pa_q_hj32_four_four_exact_product_successor * S ((S (S pa_i_hj32_four_four_exact_product)) * pa_v_hj32_four_four_exact_product) + (pa_s_hj32_four_four_exact_product))) /\ pa_s_hj32_four_four_exact_product = pa_r_hj32_four_four_exact_product * pa_p_hj32_four_four_exact_product))))))) - 0111
specialize pow_successor_compose_from_total 4 - 0112
specialize pow_successor_compose_from_total 3 - 0113
specialize pow_successor_compose_from_total (((1 * 4) * 4) * 4) - 0114
specialize pow_successor_compose_from_total ((((1 * 4) * 4) * 4) * 4) - 0115
apply pow_successor_compose_from_total - 0116
exact htotal - 0117
exact hfour_three - 0118
refl - 0119
have hx_value : x = ((((1 * 3) * 3) * 3) * 3) * 3 - 0120
specialize pow_functional 3 - 0121
specialize pow_functional 5 - 0122
specialize pow_functional x - 0123
specialize pow_functional (((((1 * 3) * 3) * 3) * 3) * 3) - 0124
apply pow_functional - 0125
exact hx - 0126
exact hthree_five - 0127
have hy_value : y = (((1 * 4) * 4) * 4) * 4 - 0128
specialize pow_functional 4 - 0129
specialize pow_functional 4 - 0130
specialize pow_functional y - 0131
specialize pow_functional ((((1 * 4) * 4) * 4) * 4) - 0132
apply pow_functional - 0133
exact hy - 0134
exact hfour_four - 0135
rewrite hx_value - 0136
rewrite hy_value - 0137
exists 13 - 0138
have hthree_four_split : (((1 * 3) * 3) * 3) * 3 = (((1 * 4) * 4) * 4) + 17 - 0139
norm_num - 0140
rewrite hthree_four_split - 0141
specialize add_mul (((1 * 4) * 4) * 4) - 0142
specialize add_mul 17 - 0143
specialize add_mul 3 - 0144
rewrite add_mul - 0145
have hfour_step : (((1 * 4) * 4) * 4) * 4 = (((1 * 4) * 4) * 4) * 3 + (((1 * 4) * 4) * 4) - 0146
apply PA6 - 0147
rewrite hfour_step - 0148
have hseventeen_three : 17 * 3 = 51 - 0149
norm_num - 0150
rewrite hseventeen_three - 0151
have hthirteen_fifty_one : 13 + 51 = ((1 * 4) * 4) * 4 - 0152
norm_num - 0153
trans (13 + (((1 * 4) * 4) * 4) * 3) + 51 - 0154
symm - 0155
specialize add_assoc 13 - 0156
specialize add_assoc ((((1 * 4) * 4) * 4) * 3) - 0157
specialize add_assoc 51 - 0158
apply add_assoc - 0159
trans ((((1 * 4) * 4) * 4) * 3 + 13) + 51 - 0160
congr - 0161
specialize add_comm 13 - 0162
specialize add_comm ((((1 * 4) * 4) * 4) * 3) - 0163
apply add_comm - 0164
refl - 0165
trans (((1 * 4) * 4) * 4) * 3 + (13 + 51) - 0166
specialize add_assoc ((((1 * 4) * 4) * 4) * 3) - 0167
specialize add_assoc 13 - 0168
specialize add_assoc 51 - 0169
apply add_assoc - 0170
rewrite hthirteen_fifty_one - 0171
refl