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,4,x) → Pow(4,6,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
11 occurrences
Exact expanded native-PA statement
forall x y. (forall bpt_a_hj32_residual_four bpt_e_hj32_residual_four. exists bpt_x_hj32_residual_four. (exists ff_b_bpt_value_hj32_residual_four ff_c_bpt_value_hj32_residual_four. ((forall ff_i_bpt_value_hj32_residual_four_repeat. (exists ff_lt_bpt_value_hj32_residual_four_repeat_bound. ff_lt_bpt_value_hj32_residual_four_repeat_bound + S ff_i_bpt_value_hj32_residual_four_repeat = bpt_e_hj32_residual_four) -> (((exists ff_h_bpt_value_hj32_residual_four_repeat_decoded. ff_h_bpt_value_hj32_residual_four_repeat_decoded + S (bpt_a_hj32_residual_four) = S ((S (ff_i_bpt_value_hj32_residual_four_repeat)) * ff_c_bpt_value_hj32_residual_four)) /\ exists ff_q_bpt_value_hj32_residual_four_repeat_decoded. ff_b_bpt_value_hj32_residual_four = ff_q_bpt_value_hj32_residual_four_repeat_decoded * S ((S (ff_i_bpt_value_hj32_residual_four_repeat)) * ff_c_bpt_value_hj32_residual_four) + (bpt_a_hj32_residual_four)))) /\ (exists ff_u_bpt_value_hj32_residual_four_product ff_v_bpt_value_hj32_residual_four_product. ((((exists ff_h_bpt_value_hj32_residual_four_product_start. ff_h_bpt_value_hj32_residual_four_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_residual_four_product)) /\ exists ff_q_bpt_value_hj32_residual_four_product_start. ff_u_bpt_value_hj32_residual_four_product = ff_q_bpt_value_hj32_residual_four_product_start * S ((S (0)) * ff_v_bpt_value_hj32_residual_four_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_residual_four_product_terminal. ff_h_bpt_value_hj32_residual_four_product_terminal + S (bpt_x_hj32_residual_four) = S ((S (bpt_e_hj32_residual_four)) * ff_v_bpt_value_hj32_residual_four_product)) /\ exists ff_q_bpt_value_hj32_residual_four_product_terminal. ff_u_bpt_value_hj32_residual_four_product = ff_q_bpt_value_hj32_residual_four_product_terminal * S ((S (bpt_e_hj32_residual_four)) * ff_v_bpt_value_hj32_residual_four_product) + (bpt_x_hj32_residual_four))) /\ forall ff_i_bpt_value_hj32_residual_four_product. (exists ff_lt_bpt_value_hj32_residual_four_product_bound. ff_lt_bpt_value_hj32_residual_four_product_bound + S ff_i_bpt_value_hj32_residual_four_product = bpt_e_hj32_residual_four) -> exists ff_p_bpt_value_hj32_residual_four_product ff_r_bpt_value_hj32_residual_four_product ff_s_bpt_value_hj32_residual_four_product. ((((exists ff_h_bpt_value_hj32_residual_four_product_factor. ff_h_bpt_value_hj32_residual_four_product_factor + S (ff_p_bpt_value_hj32_residual_four_product) = S ((S (ff_i_bpt_value_hj32_residual_four_product)) * ff_c_bpt_value_hj32_residual_four)) /\ exists ff_q_bpt_value_hj32_residual_four_product_factor. ff_b_bpt_value_hj32_residual_four = ff_q_bpt_value_hj32_residual_four_product_factor * S ((S (ff_i_bpt_value_hj32_residual_four_product)) * ff_c_bpt_value_hj32_residual_four) + (ff_p_bpt_value_hj32_residual_four_product))) /\ ((((exists ff_h_bpt_value_hj32_residual_four_product_partial. ff_h_bpt_value_hj32_residual_four_product_partial + S (ff_r_bpt_value_hj32_residual_four_product) = S ((S (ff_i_bpt_value_hj32_residual_four_product)) * ff_v_bpt_value_hj32_residual_four_product)) /\ exists ff_q_bpt_value_hj32_residual_four_product_partial. ff_u_bpt_value_hj32_residual_four_product = ff_q_bpt_value_hj32_residual_four_product_partial * S ((S (ff_i_bpt_value_hj32_residual_four_product)) * ff_v_bpt_value_hj32_residual_four_product) + (ff_r_bpt_value_hj32_residual_four_product))) /\ ((((exists ff_h_bpt_value_hj32_residual_four_product_successor. ff_h_bpt_value_hj32_residual_four_product_successor + S (ff_s_bpt_value_hj32_residual_four_product) = S ((S (S ff_i_bpt_value_hj32_residual_four_product)) * ff_v_bpt_value_hj32_residual_four_product)) /\ exists ff_q_bpt_value_hj32_residual_four_product_successor. ff_u_bpt_value_hj32_residual_four_product = ff_q_bpt_value_hj32_residual_four_product_successor * S ((S (S ff_i_bpt_value_hj32_residual_four_product)) * ff_v_bpt_value_hj32_residual_four_product) + (ff_s_bpt_value_hj32_residual_four_product))) /\ ff_s_bpt_value_hj32_residual_four_product = ff_r_bpt_value_hj32_residual_four_product * ff_p_bpt_value_hj32_residual_four_product))))))))) -> (exists pa_b_hj32_residual_four_left pa_c_hj32_residual_four_left. ((forall pa_i_hj32_residual_four_left_repeat. (exists pa_lt_hj32_residual_four_left_repeat_bound. pa_lt_hj32_residual_four_left_repeat_bound + S pa_i_hj32_residual_four_left_repeat = 4) -> (((exists pa_h_hj32_residual_four_left_repeat_decoded. pa_h_hj32_residual_four_left_repeat_decoded + S (6) = S ((S (pa_i_hj32_residual_four_left_repeat)) * pa_c_hj32_residual_four_left)) /\ exists pa_q_hj32_residual_four_left_repeat_decoded. pa_b_hj32_residual_four_left = pa_q_hj32_residual_four_left_repeat_decoded * S ((S (pa_i_hj32_residual_four_left_repeat)) * pa_c_hj32_residual_four_left) + (6)))) /\ (exists pa_u_hj32_residual_four_left_product pa_v_hj32_residual_four_left_product. ((((exists pa_h_hj32_residual_four_left_product_start. pa_h_hj32_residual_four_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_residual_four_left_product)) /\ exists pa_q_hj32_residual_four_left_product_start. pa_u_hj32_residual_four_left_product = pa_q_hj32_residual_four_left_product_start * S ((S (0)) * pa_v_hj32_residual_four_left_product) + (1))) /\ ((((exists pa_h_hj32_residual_four_left_product_terminal. pa_h_hj32_residual_four_left_product_terminal + S (x) = S ((S (4)) * pa_v_hj32_residual_four_left_product)) /\ exists pa_q_hj32_residual_four_left_product_terminal. pa_u_hj32_residual_four_left_product = pa_q_hj32_residual_four_left_product_terminal * S ((S (4)) * pa_v_hj32_residual_four_left_product) + (x))) /\ forall pa_i_hj32_residual_four_left_product. (exists pa_lt_hj32_residual_four_left_product_bound. pa_lt_hj32_residual_four_left_product_bound + S pa_i_hj32_residual_four_left_product = 4) -> exists pa_p_hj32_residual_four_left_product pa_r_hj32_residual_four_left_product pa_s_hj32_residual_four_left_product. ((((exists pa_h_hj32_residual_four_left_product_factor. pa_h_hj32_residual_four_left_product_factor + S (pa_p_hj32_residual_four_left_product) = S ((S (pa_i_hj32_residual_four_left_product)) * pa_c_hj32_residual_four_left)) /\ exists pa_q_hj32_residual_four_left_product_factor. pa_b_hj32_residual_four_left = pa_q_hj32_residual_four_left_product_factor * S ((S (pa_i_hj32_residual_four_left_product)) * pa_c_hj32_residual_four_left) + (pa_p_hj32_residual_four_left_product))) /\ ((((exists pa_h_hj32_residual_four_left_product_partial. pa_h_hj32_residual_four_left_product_partial + S (pa_r_hj32_residual_four_left_product) = S ((S (pa_i_hj32_residual_four_left_product)) * pa_v_hj32_residual_four_left_product)) /\ exists pa_q_hj32_residual_four_left_product_partial. pa_u_hj32_residual_four_left_product = pa_q_hj32_residual_four_left_product_partial * S ((S (pa_i_hj32_residual_four_left_product)) * pa_v_hj32_residual_four_left_product) + (pa_r_hj32_residual_four_left_product))) /\ ((((exists pa_h_hj32_residual_four_left_product_successor. pa_h_hj32_residual_four_left_product_successor + S (pa_s_hj32_residual_four_left_product) = S ((S (S pa_i_hj32_residual_four_left_product)) * pa_v_hj32_residual_four_left_product)) /\ exists pa_q_hj32_residual_four_left_product_successor. pa_u_hj32_residual_four_left_product = pa_q_hj32_residual_four_left_product_successor * S ((S (S pa_i_hj32_residual_four_left_product)) * pa_v_hj32_residual_four_left_product) + (pa_s_hj32_residual_four_left_product))) /\ pa_s_hj32_residual_four_left_product = pa_r_hj32_residual_four_left_product * pa_p_hj32_residual_four_left_product)))))))) -> (exists pa_b_hj32_residual_four_right pa_c_hj32_residual_four_right. ((forall pa_i_hj32_residual_four_right_repeat. (exists pa_lt_hj32_residual_four_right_repeat_bound. pa_lt_hj32_residual_four_right_repeat_bound + S pa_i_hj32_residual_four_right_repeat = 6) -> (((exists pa_h_hj32_residual_four_right_repeat_decoded. pa_h_hj32_residual_four_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_residual_four_right_repeat)) * pa_c_hj32_residual_four_right)) /\ exists pa_q_hj32_residual_four_right_repeat_decoded. pa_b_hj32_residual_four_right = pa_q_hj32_residual_four_right_repeat_decoded * S ((S (pa_i_hj32_residual_four_right_repeat)) * pa_c_hj32_residual_four_right) + (4)))) /\ (exists pa_u_hj32_residual_four_right_product pa_v_hj32_residual_four_right_product. ((((exists pa_h_hj32_residual_four_right_product_start. pa_h_hj32_residual_four_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_residual_four_right_product)) /\ exists pa_q_hj32_residual_four_right_product_start. pa_u_hj32_residual_four_right_product = pa_q_hj32_residual_four_right_product_start * S ((S (0)) * pa_v_hj32_residual_four_right_product) + (1))) /\ ((((exists pa_h_hj32_residual_four_right_product_terminal. pa_h_hj32_residual_four_right_product_terminal + S (y) = S ((S (6)) * pa_v_hj32_residual_four_right_product)) /\ exists pa_q_hj32_residual_four_right_product_terminal. pa_u_hj32_residual_four_right_product = pa_q_hj32_residual_four_right_product_terminal * S ((S (6)) * pa_v_hj32_residual_four_right_product) + (y))) /\ forall pa_i_hj32_residual_four_right_product. (exists pa_lt_hj32_residual_four_right_product_bound. pa_lt_hj32_residual_four_right_product_bound + S pa_i_hj32_residual_four_right_product = 6) -> exists pa_p_hj32_residual_four_right_product pa_r_hj32_residual_four_right_product pa_s_hj32_residual_four_right_product. ((((exists pa_h_hj32_residual_four_right_product_factor. pa_h_hj32_residual_four_right_product_factor + S (pa_p_hj32_residual_four_right_product) = S ((S (pa_i_hj32_residual_four_right_product)) * pa_c_hj32_residual_four_right)) /\ exists pa_q_hj32_residual_four_right_product_factor. pa_b_hj32_residual_four_right = pa_q_hj32_residual_four_right_product_factor * S ((S (pa_i_hj32_residual_four_right_product)) * pa_c_hj32_residual_four_right) + (pa_p_hj32_residual_four_right_product))) /\ ((((exists pa_h_hj32_residual_four_right_product_partial. pa_h_hj32_residual_four_right_product_partial + S (pa_r_hj32_residual_four_right_product) = S ((S (pa_i_hj32_residual_four_right_product)) * pa_v_hj32_residual_four_right_product)) /\ exists pa_q_hj32_residual_four_right_product_partial. pa_u_hj32_residual_four_right_product = pa_q_hj32_residual_four_right_product_partial * S ((S (pa_i_hj32_residual_four_right_product)) * pa_v_hj32_residual_four_right_product) + (pa_r_hj32_residual_four_right_product))) /\ ((((exists pa_h_hj32_residual_four_right_product_successor. pa_h_hj32_residual_four_right_product_successor + S (pa_s_hj32_residual_four_right_product) = S ((S (S pa_i_hj32_residual_four_right_product)) * pa_v_hj32_residual_four_right_product)) /\ exists pa_q_hj32_residual_four_right_product_successor. pa_u_hj32_residual_four_right_product = pa_q_hj32_residual_four_right_product_successor * S ((S (S pa_i_hj32_residual_four_right_product)) * pa_v_hj32_residual_four_right_product) + (pa_s_hj32_residual_four_right_product))) /\ pa_s_hj32_residual_four_right_product = pa_r_hj32_residual_four_right_product * pa_p_hj32_residual_four_right_product)))))))) -> (exists bqb_le_gap_hj32_residual_four_result. bqb_le_gap_hj32_residual_four_result + (x) = (y))Proof neighborhood
Direct theorem prerequisites
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 (7)
01Fix variables and assumptionsL1–5
02Establish rf_seedsL6–8
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two seed bundle from total.
- L6
have rf_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 - L7
apply pow_two_seed_bundle_from_total - L8
exact htotal
03Separate the logical casesL9–9
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L9
cases rf_seeds
04Establish rf_p2_fourL10–13
Establish this local claim before using it. It is not an additional assumption.
- L10
have rf_p2_four : ∃ hj32_local_value_rf_p2_four. Pow(2,4,hj32_local_value_rf_p2_four)Definitions: Pow(2,4,hj32_local_value_rf_p2_four)Original native command in the exact edition - L11
specialize htotal 2 - L12
specialize htotal 4 - L13
exact htotal
05Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
cases rf_p2_four
06Establish rf_p4_twoL15–18
Establish this local claim before using it. It is not an additional assumption.
- L15
have rf_p4_two : ∃ hj32_local_value_rf_p4_two. Pow(4,2,hj32_local_value_rf_p4_two)Definitions: Pow(4,2,hj32_local_value_rf_p4_two)Original native command in the exact edition - L16
specialize htotal 4 - L17
specialize htotal 2 - L18
exact htotal
07Separate the logical casesL19–19
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L19
cases rf_p4_two
08Establish rf_two_bridgeL20–29
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul exp from total.
- L20
have rf_two_bridge : x2 = x1 - L21
specialize pow_mul_exp_from_total 2 - L22
specialize pow_mul_exp_from_total 2 - L23
specialize pow_mul_exp_from_total 2 - L24
specialize pow_mul_exp_from_total 4 - L25
specialize pow_mul_exp_from_total 4 - L26
specialize pow_mul_exp_from_total x2 - L27
specialize pow_mul_exp_from_total x1 - L28
apply pow_mul_exp_from_total - L29
exact htotal
09Calculate and transport equalitiesL30–30
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L30
norm_num
10Use earlier factsL31–33
11Establish rf_two_boundL34–37
12Establish rf_p3_fourL38–41
Establish this local claim before using it. It is not an additional assumption.
- L38
have rf_p3_four : ∃ hj32_local_value_rf_p3_four. Pow(3,4,hj32_local_value_rf_p3_four)Definitions: Pow(3,4,hj32_local_value_rf_p3_four)Original native command in the exact edition - L39
specialize htotal 3 - L40
specialize htotal 4 - L41
exact htotal
13Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
cases rf_p3_four
14Establish rf_p4_fourL43–46
Establish this local claim before using it. It is not an additional assumption.
- L43
have rf_p4_four : ∃ hj32_local_value_rf_p4_four. Pow(4,4,hj32_local_value_rf_p4_four)Definitions: Pow(4,4,hj32_local_value_rf_p4_four)Original native command in the exact edition - L44
specialize htotal 4 - L45
specialize htotal 4 - L46
exact htotal
15Separate the logical casesL47–47
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L47
cases rf_p4_four
16Establish rf_baseL48–48
Establish this local claim before using it. It is not an additional assumption.
17Construct an explicit witnessL49–49
Supply the displayed value, then prove that it has the required property.
- L49
exists 1
18Calculate and transport equalitiesL50–50
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L50
norm_num
19Establish rf_three_boundL51–60
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow base monotone.
20Establish rf_six_product_graphL61–61
Establish this local claim before using it. It is not an additional assumption.
- L61
have rf_six_product_graph : Pow(2 · 3,4,x)Definitions: Pow(2 · 3,4,x)Original native command in the exact edition
21Establish rf_six_product_baseL62–66
22Establish rf_six_productL67–76
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul base.
23Use earlier factsL77–77
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L77
exact rf_six_product_graph
24Establish rf_six_powerL78–87
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.
25Use earlier factsL88–90
26Establish rf_resultL91–100
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.
- L91
have rf_result : Le(x1 · x3,x2 · x4)Definitions: Le(x1 · x3,x2 · x4)Original native command in the exact edition - L92
specialize mul_le_mul x1 - L93
specialize mul_le_mul x2 - L94
specialize mul_le_mul x3 - L95
specialize mul_le_mul x4 - L96
apply mul_le_mul - L97
exact rf_two_bound - L98
exact rf_three_bound - L99
rewrite <- rf_six_product at rf_result - L100
rewrite <- rf_six_power at rf_result
27Use earlier factsL101–101
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L101
exact rf_result
Original defined command ledger · 101 lines
- 0001
intro x - 0002
intro y - 0003
intro htotal - 0004
intro hx - 0005
intro hy - 0006
have rf_seeds : Pow(2,2,4) ∧ Pow(2,7,128)Exact native replay line
have rf_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)))))))) - 0007
apply pow_two_seed_bundle_from_total - 0008
exact htotal - 0009
cases rf_seeds - 0010
have rf_p2_four : ∃ hj32_local_value_rf_p2_four. Pow(2,4,hj32_local_value_rf_p2_four)Exact native replay line
have rf_p2_four : exists hj32_local_value_rf_p2_four. (exists pa_b_hj32_local_total_rf_p2_four pa_c_hj32_local_total_rf_p2_four. ((forall pa_i_hj32_local_total_rf_p2_four_repeat. (exists pa_lt_hj32_local_total_rf_p2_four_repeat_bound. pa_lt_hj32_local_total_rf_p2_four_repeat_bound + S pa_i_hj32_local_total_rf_p2_four_repeat = 4) -> (((exists pa_h_hj32_local_total_rf_p2_four_repeat_decoded. pa_h_hj32_local_total_rf_p2_four_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_rf_p2_four_repeat)) * pa_c_hj32_local_total_rf_p2_four)) /\ exists pa_q_hj32_local_total_rf_p2_four_repeat_decoded. pa_b_hj32_local_total_rf_p2_four = pa_q_hj32_local_total_rf_p2_four_repeat_decoded * S ((S (pa_i_hj32_local_total_rf_p2_four_repeat)) * pa_c_hj32_local_total_rf_p2_four) + (2)))) /\ (exists pa_u_hj32_local_total_rf_p2_four_product pa_v_hj32_local_total_rf_p2_four_product. ((((exists pa_h_hj32_local_total_rf_p2_four_product_start. pa_h_hj32_local_total_rf_p2_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rf_p2_four_product)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_start. pa_u_hj32_local_total_rf_p2_four_product = pa_q_hj32_local_total_rf_p2_four_product_start * S ((S (0)) * pa_v_hj32_local_total_rf_p2_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rf_p2_four_product_terminal. pa_h_hj32_local_total_rf_p2_four_product_terminal + S (hj32_local_value_rf_p2_four) = S ((S (4)) * pa_v_hj32_local_total_rf_p2_four_product)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_terminal. pa_u_hj32_local_total_rf_p2_four_product = pa_q_hj32_local_total_rf_p2_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_rf_p2_four_product) + (hj32_local_value_rf_p2_four))) /\ forall pa_i_hj32_local_total_rf_p2_four_product. (exists pa_lt_hj32_local_total_rf_p2_four_product_bound. pa_lt_hj32_local_total_rf_p2_four_product_bound + S pa_i_hj32_local_total_rf_p2_four_product = 4) -> exists pa_p_hj32_local_total_rf_p2_four_product pa_r_hj32_local_total_rf_p2_four_product pa_s_hj32_local_total_rf_p2_four_product. ((((exists pa_h_hj32_local_total_rf_p2_four_product_factor. pa_h_hj32_local_total_rf_p2_four_product_factor + S (pa_p_hj32_local_total_rf_p2_four_product) = S ((S (pa_i_hj32_local_total_rf_p2_four_product)) * pa_c_hj32_local_total_rf_p2_four)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_factor. pa_b_hj32_local_total_rf_p2_four = pa_q_hj32_local_total_rf_p2_four_product_factor * S ((S (pa_i_hj32_local_total_rf_p2_four_product)) * pa_c_hj32_local_total_rf_p2_four) + (pa_p_hj32_local_total_rf_p2_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p2_four_product_partial. pa_h_hj32_local_total_rf_p2_four_product_partial + S (pa_r_hj32_local_total_rf_p2_four_product) = S ((S (pa_i_hj32_local_total_rf_p2_four_product)) * pa_v_hj32_local_total_rf_p2_four_product)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_partial. pa_u_hj32_local_total_rf_p2_four_product = pa_q_hj32_local_total_rf_p2_four_product_partial * S ((S (pa_i_hj32_local_total_rf_p2_four_product)) * pa_v_hj32_local_total_rf_p2_four_product) + (pa_r_hj32_local_total_rf_p2_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p2_four_product_successor. pa_h_hj32_local_total_rf_p2_four_product_successor + S (pa_s_hj32_local_total_rf_p2_four_product) = S ((S (S pa_i_hj32_local_total_rf_p2_four_product)) * pa_v_hj32_local_total_rf_p2_four_product)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_successor. pa_u_hj32_local_total_rf_p2_four_product = pa_q_hj32_local_total_rf_p2_four_product_successor * S ((S (S pa_i_hj32_local_total_rf_p2_four_product)) * pa_v_hj32_local_total_rf_p2_four_product) + (pa_s_hj32_local_total_rf_p2_four_product))) /\ pa_s_hj32_local_total_rf_p2_four_product = pa_r_hj32_local_total_rf_p2_four_product * pa_p_hj32_local_total_rf_p2_four_product)))))))) - 0011
specialize htotal 2 - 0012
specialize htotal 4 - 0013
exact htotal - 0014
cases rf_p2_four - 0015
have rf_p4_two : ∃ hj32_local_value_rf_p4_two. Pow(4,2,hj32_local_value_rf_p4_two)Exact native replay line
have rf_p4_two : exists hj32_local_value_rf_p4_two. (exists pa_b_hj32_local_total_rf_p4_two pa_c_hj32_local_total_rf_p4_two. ((forall pa_i_hj32_local_total_rf_p4_two_repeat. (exists pa_lt_hj32_local_total_rf_p4_two_repeat_bound. pa_lt_hj32_local_total_rf_p4_two_repeat_bound + S pa_i_hj32_local_total_rf_p4_two_repeat = 2) -> (((exists pa_h_hj32_local_total_rf_p4_two_repeat_decoded. pa_h_hj32_local_total_rf_p4_two_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rf_p4_two_repeat)) * pa_c_hj32_local_total_rf_p4_two)) /\ exists pa_q_hj32_local_total_rf_p4_two_repeat_decoded. pa_b_hj32_local_total_rf_p4_two = pa_q_hj32_local_total_rf_p4_two_repeat_decoded * S ((S (pa_i_hj32_local_total_rf_p4_two_repeat)) * pa_c_hj32_local_total_rf_p4_two) + (4)))) /\ (exists pa_u_hj32_local_total_rf_p4_two_product pa_v_hj32_local_total_rf_p4_two_product. ((((exists pa_h_hj32_local_total_rf_p4_two_product_start. pa_h_hj32_local_total_rf_p4_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rf_p4_two_product)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_start. pa_u_hj32_local_total_rf_p4_two_product = pa_q_hj32_local_total_rf_p4_two_product_start * S ((S (0)) * pa_v_hj32_local_total_rf_p4_two_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rf_p4_two_product_terminal. pa_h_hj32_local_total_rf_p4_two_product_terminal + S (hj32_local_value_rf_p4_two) = S ((S (2)) * pa_v_hj32_local_total_rf_p4_two_product)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_terminal. pa_u_hj32_local_total_rf_p4_two_product = pa_q_hj32_local_total_rf_p4_two_product_terminal * S ((S (2)) * pa_v_hj32_local_total_rf_p4_two_product) + (hj32_local_value_rf_p4_two))) /\ forall pa_i_hj32_local_total_rf_p4_two_product. (exists pa_lt_hj32_local_total_rf_p4_two_product_bound. pa_lt_hj32_local_total_rf_p4_two_product_bound + S pa_i_hj32_local_total_rf_p4_two_product = 2) -> exists pa_p_hj32_local_total_rf_p4_two_product pa_r_hj32_local_total_rf_p4_two_product pa_s_hj32_local_total_rf_p4_two_product. ((((exists pa_h_hj32_local_total_rf_p4_two_product_factor. pa_h_hj32_local_total_rf_p4_two_product_factor + S (pa_p_hj32_local_total_rf_p4_two_product) = S ((S (pa_i_hj32_local_total_rf_p4_two_product)) * pa_c_hj32_local_total_rf_p4_two)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_factor. pa_b_hj32_local_total_rf_p4_two = pa_q_hj32_local_total_rf_p4_two_product_factor * S ((S (pa_i_hj32_local_total_rf_p4_two_product)) * pa_c_hj32_local_total_rf_p4_two) + (pa_p_hj32_local_total_rf_p4_two_product))) /\ ((((exists pa_h_hj32_local_total_rf_p4_two_product_partial. pa_h_hj32_local_total_rf_p4_two_product_partial + S (pa_r_hj32_local_total_rf_p4_two_product) = S ((S (pa_i_hj32_local_total_rf_p4_two_product)) * pa_v_hj32_local_total_rf_p4_two_product)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_partial. pa_u_hj32_local_total_rf_p4_two_product = pa_q_hj32_local_total_rf_p4_two_product_partial * S ((S (pa_i_hj32_local_total_rf_p4_two_product)) * pa_v_hj32_local_total_rf_p4_two_product) + (pa_r_hj32_local_total_rf_p4_two_product))) /\ ((((exists pa_h_hj32_local_total_rf_p4_two_product_successor. pa_h_hj32_local_total_rf_p4_two_product_successor + S (pa_s_hj32_local_total_rf_p4_two_product) = S ((S (S pa_i_hj32_local_total_rf_p4_two_product)) * pa_v_hj32_local_total_rf_p4_two_product)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_successor. pa_u_hj32_local_total_rf_p4_two_product = pa_q_hj32_local_total_rf_p4_two_product_successor * S ((S (S pa_i_hj32_local_total_rf_p4_two_product)) * pa_v_hj32_local_total_rf_p4_two_product) + (pa_s_hj32_local_total_rf_p4_two_product))) /\ pa_s_hj32_local_total_rf_p4_two_product = pa_r_hj32_local_total_rf_p4_two_product * pa_p_hj32_local_total_rf_p4_two_product)))))))) - 0016
specialize htotal 4 - 0017
specialize htotal 2 - 0018
exact htotal - 0019
cases rf_p4_two - 0020
have rf_two_bridge : x2 = x1 - 0021
specialize pow_mul_exp_from_total 2 - 0022
specialize pow_mul_exp_from_total 2 - 0023
specialize pow_mul_exp_from_total 2 - 0024
specialize pow_mul_exp_from_total 4 - 0025
specialize pow_mul_exp_from_total 4 - 0026
specialize pow_mul_exp_from_total x2 - 0027
specialize pow_mul_exp_from_total x1 - 0028
apply pow_mul_exp_from_total - 0029
exact htotal - 0030
norm_num - 0031
exact rf_seeds_left - 0032
exact rf_p4_two_witness - 0033
exact rf_p2_four_witness - 0034
have rf_two_bound : Le(x1,x2)Exact native replay line
have rf_two_bound : exists bqb_le_gap_hj32_rf_two_bound. bqb_le_gap_hj32_rf_two_bound + (x1) = (x2) - 0035
rewrite rf_two_bridge - 0036
specialize le_refl x1 - 0037
exact le_refl - 0038
have rf_p3_four : ∃ hj32_local_value_rf_p3_four. Pow(3,4,hj32_local_value_rf_p3_four)Exact native replay line
have rf_p3_four : exists hj32_local_value_rf_p3_four. (exists pa_b_hj32_local_total_rf_p3_four pa_c_hj32_local_total_rf_p3_four. ((forall pa_i_hj32_local_total_rf_p3_four_repeat. (exists pa_lt_hj32_local_total_rf_p3_four_repeat_bound. pa_lt_hj32_local_total_rf_p3_four_repeat_bound + S pa_i_hj32_local_total_rf_p3_four_repeat = 4) -> (((exists pa_h_hj32_local_total_rf_p3_four_repeat_decoded. pa_h_hj32_local_total_rf_p3_four_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_rf_p3_four_repeat)) * pa_c_hj32_local_total_rf_p3_four)) /\ exists pa_q_hj32_local_total_rf_p3_four_repeat_decoded. pa_b_hj32_local_total_rf_p3_four = pa_q_hj32_local_total_rf_p3_four_repeat_decoded * S ((S (pa_i_hj32_local_total_rf_p3_four_repeat)) * pa_c_hj32_local_total_rf_p3_four) + (3)))) /\ (exists pa_u_hj32_local_total_rf_p3_four_product pa_v_hj32_local_total_rf_p3_four_product. ((((exists pa_h_hj32_local_total_rf_p3_four_product_start. pa_h_hj32_local_total_rf_p3_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rf_p3_four_product)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_start. pa_u_hj32_local_total_rf_p3_four_product = pa_q_hj32_local_total_rf_p3_four_product_start * S ((S (0)) * pa_v_hj32_local_total_rf_p3_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rf_p3_four_product_terminal. pa_h_hj32_local_total_rf_p3_four_product_terminal + S (hj32_local_value_rf_p3_four) = S ((S (4)) * pa_v_hj32_local_total_rf_p3_four_product)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_terminal. pa_u_hj32_local_total_rf_p3_four_product = pa_q_hj32_local_total_rf_p3_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_rf_p3_four_product) + (hj32_local_value_rf_p3_four))) /\ forall pa_i_hj32_local_total_rf_p3_four_product. (exists pa_lt_hj32_local_total_rf_p3_four_product_bound. pa_lt_hj32_local_total_rf_p3_four_product_bound + S pa_i_hj32_local_total_rf_p3_four_product = 4) -> exists pa_p_hj32_local_total_rf_p3_four_product pa_r_hj32_local_total_rf_p3_four_product pa_s_hj32_local_total_rf_p3_four_product. ((((exists pa_h_hj32_local_total_rf_p3_four_product_factor. pa_h_hj32_local_total_rf_p3_four_product_factor + S (pa_p_hj32_local_total_rf_p3_four_product) = S ((S (pa_i_hj32_local_total_rf_p3_four_product)) * pa_c_hj32_local_total_rf_p3_four)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_factor. pa_b_hj32_local_total_rf_p3_four = pa_q_hj32_local_total_rf_p3_four_product_factor * S ((S (pa_i_hj32_local_total_rf_p3_four_product)) * pa_c_hj32_local_total_rf_p3_four) + (pa_p_hj32_local_total_rf_p3_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p3_four_product_partial. pa_h_hj32_local_total_rf_p3_four_product_partial + S (pa_r_hj32_local_total_rf_p3_four_product) = S ((S (pa_i_hj32_local_total_rf_p3_four_product)) * pa_v_hj32_local_total_rf_p3_four_product)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_partial. pa_u_hj32_local_total_rf_p3_four_product = pa_q_hj32_local_total_rf_p3_four_product_partial * S ((S (pa_i_hj32_local_total_rf_p3_four_product)) * pa_v_hj32_local_total_rf_p3_four_product) + (pa_r_hj32_local_total_rf_p3_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p3_four_product_successor. pa_h_hj32_local_total_rf_p3_four_product_successor + S (pa_s_hj32_local_total_rf_p3_four_product) = S ((S (S pa_i_hj32_local_total_rf_p3_four_product)) * pa_v_hj32_local_total_rf_p3_four_product)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_successor. pa_u_hj32_local_total_rf_p3_four_product = pa_q_hj32_local_total_rf_p3_four_product_successor * S ((S (S pa_i_hj32_local_total_rf_p3_four_product)) * pa_v_hj32_local_total_rf_p3_four_product) + (pa_s_hj32_local_total_rf_p3_four_product))) /\ pa_s_hj32_local_total_rf_p3_four_product = pa_r_hj32_local_total_rf_p3_four_product * pa_p_hj32_local_total_rf_p3_four_product)))))))) - 0039
specialize htotal 3 - 0040
specialize htotal 4 - 0041
exact htotal - 0042
cases rf_p3_four - 0043
have rf_p4_four : ∃ hj32_local_value_rf_p4_four. Pow(4,4,hj32_local_value_rf_p4_four)Exact native replay line
have rf_p4_four : exists hj32_local_value_rf_p4_four. (exists pa_b_hj32_local_total_rf_p4_four pa_c_hj32_local_total_rf_p4_four. ((forall pa_i_hj32_local_total_rf_p4_four_repeat. (exists pa_lt_hj32_local_total_rf_p4_four_repeat_bound. pa_lt_hj32_local_total_rf_p4_four_repeat_bound + S pa_i_hj32_local_total_rf_p4_four_repeat = 4) -> (((exists pa_h_hj32_local_total_rf_p4_four_repeat_decoded. pa_h_hj32_local_total_rf_p4_four_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rf_p4_four_repeat)) * pa_c_hj32_local_total_rf_p4_four)) /\ exists pa_q_hj32_local_total_rf_p4_four_repeat_decoded. pa_b_hj32_local_total_rf_p4_four = pa_q_hj32_local_total_rf_p4_four_repeat_decoded * S ((S (pa_i_hj32_local_total_rf_p4_four_repeat)) * pa_c_hj32_local_total_rf_p4_four) + (4)))) /\ (exists pa_u_hj32_local_total_rf_p4_four_product pa_v_hj32_local_total_rf_p4_four_product. ((((exists pa_h_hj32_local_total_rf_p4_four_product_start. pa_h_hj32_local_total_rf_p4_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rf_p4_four_product)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_start. pa_u_hj32_local_total_rf_p4_four_product = pa_q_hj32_local_total_rf_p4_four_product_start * S ((S (0)) * pa_v_hj32_local_total_rf_p4_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rf_p4_four_product_terminal. pa_h_hj32_local_total_rf_p4_four_product_terminal + S (hj32_local_value_rf_p4_four) = S ((S (4)) * pa_v_hj32_local_total_rf_p4_four_product)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_terminal. pa_u_hj32_local_total_rf_p4_four_product = pa_q_hj32_local_total_rf_p4_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_rf_p4_four_product) + (hj32_local_value_rf_p4_four))) /\ forall pa_i_hj32_local_total_rf_p4_four_product. (exists pa_lt_hj32_local_total_rf_p4_four_product_bound. pa_lt_hj32_local_total_rf_p4_four_product_bound + S pa_i_hj32_local_total_rf_p4_four_product = 4) -> exists pa_p_hj32_local_total_rf_p4_four_product pa_r_hj32_local_total_rf_p4_four_product pa_s_hj32_local_total_rf_p4_four_product. ((((exists pa_h_hj32_local_total_rf_p4_four_product_factor. pa_h_hj32_local_total_rf_p4_four_product_factor + S (pa_p_hj32_local_total_rf_p4_four_product) = S ((S (pa_i_hj32_local_total_rf_p4_four_product)) * pa_c_hj32_local_total_rf_p4_four)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_factor. pa_b_hj32_local_total_rf_p4_four = pa_q_hj32_local_total_rf_p4_four_product_factor * S ((S (pa_i_hj32_local_total_rf_p4_four_product)) * pa_c_hj32_local_total_rf_p4_four) + (pa_p_hj32_local_total_rf_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p4_four_product_partial. pa_h_hj32_local_total_rf_p4_four_product_partial + S (pa_r_hj32_local_total_rf_p4_four_product) = S ((S (pa_i_hj32_local_total_rf_p4_four_product)) * pa_v_hj32_local_total_rf_p4_four_product)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_partial. pa_u_hj32_local_total_rf_p4_four_product = pa_q_hj32_local_total_rf_p4_four_product_partial * S ((S (pa_i_hj32_local_total_rf_p4_four_product)) * pa_v_hj32_local_total_rf_p4_four_product) + (pa_r_hj32_local_total_rf_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p4_four_product_successor. pa_h_hj32_local_total_rf_p4_four_product_successor + S (pa_s_hj32_local_total_rf_p4_four_product) = S ((S (S pa_i_hj32_local_total_rf_p4_four_product)) * pa_v_hj32_local_total_rf_p4_four_product)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_successor. pa_u_hj32_local_total_rf_p4_four_product = pa_q_hj32_local_total_rf_p4_four_product_successor * S ((S (S pa_i_hj32_local_total_rf_p4_four_product)) * pa_v_hj32_local_total_rf_p4_four_product) + (pa_s_hj32_local_total_rf_p4_four_product))) /\ pa_s_hj32_local_total_rf_p4_four_product = pa_r_hj32_local_total_rf_p4_four_product * pa_p_hj32_local_total_rf_p4_four_product)))))))) - 0044
specialize htotal 4 - 0045
specialize htotal 4 - 0046
exact htotal - 0047
cases rf_p4_four - 0048
have rf_base : Lt(2,4)Exact native replay line
have rf_base : exists bqb_le_gap_hj32_rf_base. bqb_le_gap_hj32_rf_base + (3) = (4) - 0049
exists 1 - 0050
norm_num - 0051
have rf_three_bound : Le(x3,x4)Exact native replay line
have rf_three_bound : exists bqb_le_gap_hj32_local_base_bound_rf_three_bound. bqb_le_gap_hj32_local_base_bound_rf_three_bound + (x3) = (x4) - 0052
specialize pow_base_monotone 3 - 0053
specialize pow_base_monotone 4 - 0054
specialize pow_base_monotone 4 - 0055
specialize pow_base_monotone x3 - 0056
specialize pow_base_monotone x4 - 0057
apply pow_base_monotone - 0058
exact rf_base - 0059
exact rf_p3_four_witness - 0060
exact rf_p4_four_witness - 0061
have rf_six_product_graph : Pow(2 · 3,4,x)Exact native replay line
have rf_six_product_graph : exists pa_b_hj32_local_product_rf_six_product pa_c_hj32_local_product_rf_six_product. ((forall pa_i_hj32_local_product_rf_six_product_repeat. (exists pa_lt_hj32_local_product_rf_six_product_repeat_bound. pa_lt_hj32_local_product_rf_six_product_repeat_bound + S pa_i_hj32_local_product_rf_six_product_repeat = 4) -> (((exists pa_h_hj32_local_product_rf_six_product_repeat_decoded. pa_h_hj32_local_product_rf_six_product_repeat_decoded + S (2 * 3) = S ((S (pa_i_hj32_local_product_rf_six_product_repeat)) * pa_c_hj32_local_product_rf_six_product)) /\ exists pa_q_hj32_local_product_rf_six_product_repeat_decoded. pa_b_hj32_local_product_rf_six_product = pa_q_hj32_local_product_rf_six_product_repeat_decoded * S ((S (pa_i_hj32_local_product_rf_six_product_repeat)) * pa_c_hj32_local_product_rf_six_product) + (2 * 3)))) /\ (exists pa_u_hj32_local_product_rf_six_product_product pa_v_hj32_local_product_rf_six_product_product. ((((exists pa_h_hj32_local_product_rf_six_product_product_start. pa_h_hj32_local_product_rf_six_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_rf_six_product_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_start. pa_u_hj32_local_product_rf_six_product_product = pa_q_hj32_local_product_rf_six_product_product_start * S ((S (0)) * pa_v_hj32_local_product_rf_six_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_rf_six_product_product_terminal. pa_h_hj32_local_product_rf_six_product_product_terminal + S (x) = S ((S (4)) * pa_v_hj32_local_product_rf_six_product_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_terminal. pa_u_hj32_local_product_rf_six_product_product = pa_q_hj32_local_product_rf_six_product_product_terminal * S ((S (4)) * pa_v_hj32_local_product_rf_six_product_product) + (x))) /\ forall pa_i_hj32_local_product_rf_six_product_product. (exists pa_lt_hj32_local_product_rf_six_product_product_bound. pa_lt_hj32_local_product_rf_six_product_product_bound + S pa_i_hj32_local_product_rf_six_product_product = 4) -> exists pa_p_hj32_local_product_rf_six_product_product pa_r_hj32_local_product_rf_six_product_product pa_s_hj32_local_product_rf_six_product_product. ((((exists pa_h_hj32_local_product_rf_six_product_product_factor. pa_h_hj32_local_product_rf_six_product_product_factor + S (pa_p_hj32_local_product_rf_six_product_product) = S ((S (pa_i_hj32_local_product_rf_six_product_product)) * pa_c_hj32_local_product_rf_six_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_factor. pa_b_hj32_local_product_rf_six_product = pa_q_hj32_local_product_rf_six_product_product_factor * S ((S (pa_i_hj32_local_product_rf_six_product_product)) * pa_c_hj32_local_product_rf_six_product) + (pa_p_hj32_local_product_rf_six_product_product))) /\ ((((exists pa_h_hj32_local_product_rf_six_product_product_partial. pa_h_hj32_local_product_rf_six_product_product_partial + S (pa_r_hj32_local_product_rf_six_product_product) = S ((S (pa_i_hj32_local_product_rf_six_product_product)) * pa_v_hj32_local_product_rf_six_product_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_partial. pa_u_hj32_local_product_rf_six_product_product = pa_q_hj32_local_product_rf_six_product_product_partial * S ((S (pa_i_hj32_local_product_rf_six_product_product)) * pa_v_hj32_local_product_rf_six_product_product) + (pa_r_hj32_local_product_rf_six_product_product))) /\ ((((exists pa_h_hj32_local_product_rf_six_product_product_successor. pa_h_hj32_local_product_rf_six_product_product_successor + S (pa_s_hj32_local_product_rf_six_product_product) = S ((S (S pa_i_hj32_local_product_rf_six_product_product)) * pa_v_hj32_local_product_rf_six_product_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_successor. pa_u_hj32_local_product_rf_six_product_product = pa_q_hj32_local_product_rf_six_product_product_successor * S ((S (S pa_i_hj32_local_product_rf_six_product_product)) * pa_v_hj32_local_product_rf_six_product_product) + (pa_s_hj32_local_product_rf_six_product_product))) /\ pa_s_hj32_local_product_rf_six_product_product = pa_r_hj32_local_product_rf_six_product_product * pa_p_hj32_local_product_rf_six_product_product))))))) - 0062
have rf_six_product_base : 2 * 3 = 6 - 0063
norm_num - 0064
rewrite rf_six_product_base - 0065
rewrite rf_six_product_base - 0066
exact hx - 0067
have rf_six_product : x = x1 * x3 - 0068
specialize pow_mul_base 2 - 0069
specialize pow_mul_base 3 - 0070
specialize pow_mul_base 4 - 0071
specialize pow_mul_base x1 - 0072
specialize pow_mul_base x3 - 0073
specialize pow_mul_base x - 0074
apply pow_mul_base - 0075
exact rf_p2_four_witness - 0076
exact rf_p3_four_witness - 0077
exact rf_six_product_graph - 0078
have rf_six_power : y = x2 * x4 - 0079
specialize pow_add 4 - 0080
specialize pow_add 2 - 0081
specialize pow_add 4 - 0082
specialize pow_add 6 - 0083
specialize pow_add x2 - 0084
specialize pow_add x4 - 0085
specialize pow_add y - 0086
apply pow_add - 0087
norm_num - 0088
exact rf_p4_two_witness - 0089
exact rf_p4_four_witness - 0090
exact hy - 0091
have rf_result : Le(x1 · x3,x2 · x4)Exact native replay line
have rf_result : exists bqb_le_gap_hj32_local_product_bound_rf_result. bqb_le_gap_hj32_local_product_bound_rf_result + (x1 * x3) = (x2 * x4) - 0092
specialize mul_le_mul x1 - 0093
specialize mul_le_mul x2 - 0094
specialize mul_le_mul x3 - 0095
specialize mul_le_mul x4 - 0096
apply mul_le_mul - 0097
exact rf_two_bound - 0098
exact rf_three_bound - 0099
rewrite <- rf_six_product at rf_result - 0100
rewrite <- rf_six_power at rf_result - 0101
exact rf_result