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
∀ m. ∀ x. ∀ y. (∀ z. ∀ n. ∃ k. Pow(z,n,k)) → Pow(3,5 · m + 1,x) → Pow(4,4 · m + 1,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 m x y. (forall bpt_a_hj32_three_plus bpt_e_hj32_three_plus. exists bpt_x_hj32_three_plus. (exists ff_b_bpt_value_hj32_three_plus ff_c_bpt_value_hj32_three_plus. ((forall ff_i_bpt_value_hj32_three_plus_repeat. (exists ff_lt_bpt_value_hj32_three_plus_repeat_bound. ff_lt_bpt_value_hj32_three_plus_repeat_bound + S ff_i_bpt_value_hj32_three_plus_repeat = bpt_e_hj32_three_plus) -> (((exists ff_h_bpt_value_hj32_three_plus_repeat_decoded. ff_h_bpt_value_hj32_three_plus_repeat_decoded + S (bpt_a_hj32_three_plus) = S ((S (ff_i_bpt_value_hj32_three_plus_repeat)) * ff_c_bpt_value_hj32_three_plus)) /\ exists ff_q_bpt_value_hj32_three_plus_repeat_decoded. ff_b_bpt_value_hj32_three_plus = ff_q_bpt_value_hj32_three_plus_repeat_decoded * S ((S (ff_i_bpt_value_hj32_three_plus_repeat)) * ff_c_bpt_value_hj32_three_plus) + (bpt_a_hj32_three_plus)))) /\ (exists ff_u_bpt_value_hj32_three_plus_product ff_v_bpt_value_hj32_three_plus_product. ((((exists ff_h_bpt_value_hj32_three_plus_product_start. ff_h_bpt_value_hj32_three_plus_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_three_plus_product)) /\ exists ff_q_bpt_value_hj32_three_plus_product_start. ff_u_bpt_value_hj32_three_plus_product = ff_q_bpt_value_hj32_three_plus_product_start * S ((S (0)) * ff_v_bpt_value_hj32_three_plus_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_three_plus_product_terminal. ff_h_bpt_value_hj32_three_plus_product_terminal + S (bpt_x_hj32_three_plus) = S ((S (bpt_e_hj32_three_plus)) * ff_v_bpt_value_hj32_three_plus_product)) /\ exists ff_q_bpt_value_hj32_three_plus_product_terminal. ff_u_bpt_value_hj32_three_plus_product = ff_q_bpt_value_hj32_three_plus_product_terminal * S ((S (bpt_e_hj32_three_plus)) * ff_v_bpt_value_hj32_three_plus_product) + (bpt_x_hj32_three_plus))) /\ forall ff_i_bpt_value_hj32_three_plus_product. (exists ff_lt_bpt_value_hj32_three_plus_product_bound. ff_lt_bpt_value_hj32_three_plus_product_bound + S ff_i_bpt_value_hj32_three_plus_product = bpt_e_hj32_three_plus) -> exists ff_p_bpt_value_hj32_three_plus_product ff_r_bpt_value_hj32_three_plus_product ff_s_bpt_value_hj32_three_plus_product. ((((exists ff_h_bpt_value_hj32_three_plus_product_factor. ff_h_bpt_value_hj32_three_plus_product_factor + S (ff_p_bpt_value_hj32_three_plus_product) = S ((S (ff_i_bpt_value_hj32_three_plus_product)) * ff_c_bpt_value_hj32_three_plus)) /\ exists ff_q_bpt_value_hj32_three_plus_product_factor. ff_b_bpt_value_hj32_three_plus = ff_q_bpt_value_hj32_three_plus_product_factor * S ((S (ff_i_bpt_value_hj32_three_plus_product)) * ff_c_bpt_value_hj32_three_plus) + (ff_p_bpt_value_hj32_three_plus_product))) /\ ((((exists ff_h_bpt_value_hj32_three_plus_product_partial. ff_h_bpt_value_hj32_three_plus_product_partial + S (ff_r_bpt_value_hj32_three_plus_product) = S ((S (ff_i_bpt_value_hj32_three_plus_product)) * ff_v_bpt_value_hj32_three_plus_product)) /\ exists ff_q_bpt_value_hj32_three_plus_product_partial. ff_u_bpt_value_hj32_three_plus_product = ff_q_bpt_value_hj32_three_plus_product_partial * S ((S (ff_i_bpt_value_hj32_three_plus_product)) * ff_v_bpt_value_hj32_three_plus_product) + (ff_r_bpt_value_hj32_three_plus_product))) /\ ((((exists ff_h_bpt_value_hj32_three_plus_product_successor. ff_h_bpt_value_hj32_three_plus_product_successor + S (ff_s_bpt_value_hj32_three_plus_product) = S ((S (S ff_i_bpt_value_hj32_three_plus_product)) * ff_v_bpt_value_hj32_three_plus_product)) /\ exists ff_q_bpt_value_hj32_three_plus_product_successor. ff_u_bpt_value_hj32_three_plus_product = ff_q_bpt_value_hj32_three_plus_product_successor * S ((S (S ff_i_bpt_value_hj32_three_plus_product)) * ff_v_bpt_value_hj32_three_plus_product) + (ff_s_bpt_value_hj32_three_plus_product))) /\ ff_s_bpt_value_hj32_three_plus_product = ff_r_bpt_value_hj32_three_plus_product * ff_p_bpt_value_hj32_three_plus_product))))))))) -> (exists pa_b_hj32_three_plus_left pa_c_hj32_three_plus_left. ((forall pa_i_hj32_three_plus_left_repeat. (exists pa_lt_hj32_three_plus_left_repeat_bound. pa_lt_hj32_three_plus_left_repeat_bound + S pa_i_hj32_three_plus_left_repeat = 5 * m + 1) -> (((exists pa_h_hj32_three_plus_left_repeat_decoded. pa_h_hj32_three_plus_left_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_plus_left_repeat)) * pa_c_hj32_three_plus_left)) /\ exists pa_q_hj32_three_plus_left_repeat_decoded. pa_b_hj32_three_plus_left = pa_q_hj32_three_plus_left_repeat_decoded * S ((S (pa_i_hj32_three_plus_left_repeat)) * pa_c_hj32_three_plus_left) + (3)))) /\ (exists pa_u_hj32_three_plus_left_product pa_v_hj32_three_plus_left_product. ((((exists pa_h_hj32_three_plus_left_product_start. pa_h_hj32_three_plus_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_plus_left_product)) /\ exists pa_q_hj32_three_plus_left_product_start. pa_u_hj32_three_plus_left_product = pa_q_hj32_three_plus_left_product_start * S ((S (0)) * pa_v_hj32_three_plus_left_product) + (1))) /\ ((((exists pa_h_hj32_three_plus_left_product_terminal. pa_h_hj32_three_plus_left_product_terminal + S (x) = S ((S (5 * m + 1)) * pa_v_hj32_three_plus_left_product)) /\ exists pa_q_hj32_three_plus_left_product_terminal. pa_u_hj32_three_plus_left_product = pa_q_hj32_three_plus_left_product_terminal * S ((S (5 * m + 1)) * pa_v_hj32_three_plus_left_product) + (x))) /\ forall pa_i_hj32_three_plus_left_product. (exists pa_lt_hj32_three_plus_left_product_bound. pa_lt_hj32_three_plus_left_product_bound + S pa_i_hj32_three_plus_left_product = 5 * m + 1) -> exists pa_p_hj32_three_plus_left_product pa_r_hj32_three_plus_left_product pa_s_hj32_three_plus_left_product. ((((exists pa_h_hj32_three_plus_left_product_factor. pa_h_hj32_three_plus_left_product_factor + S (pa_p_hj32_three_plus_left_product) = S ((S (pa_i_hj32_three_plus_left_product)) * pa_c_hj32_three_plus_left)) /\ exists pa_q_hj32_three_plus_left_product_factor. pa_b_hj32_three_plus_left = pa_q_hj32_three_plus_left_product_factor * S ((S (pa_i_hj32_three_plus_left_product)) * pa_c_hj32_three_plus_left) + (pa_p_hj32_three_plus_left_product))) /\ ((((exists pa_h_hj32_three_plus_left_product_partial. pa_h_hj32_three_plus_left_product_partial + S (pa_r_hj32_three_plus_left_product) = S ((S (pa_i_hj32_three_plus_left_product)) * pa_v_hj32_three_plus_left_product)) /\ exists pa_q_hj32_three_plus_left_product_partial. pa_u_hj32_three_plus_left_product = pa_q_hj32_three_plus_left_product_partial * S ((S (pa_i_hj32_three_plus_left_product)) * pa_v_hj32_three_plus_left_product) + (pa_r_hj32_three_plus_left_product))) /\ ((((exists pa_h_hj32_three_plus_left_product_successor. pa_h_hj32_three_plus_left_product_successor + S (pa_s_hj32_three_plus_left_product) = S ((S (S pa_i_hj32_three_plus_left_product)) * pa_v_hj32_three_plus_left_product)) /\ exists pa_q_hj32_three_plus_left_product_successor. pa_u_hj32_three_plus_left_product = pa_q_hj32_three_plus_left_product_successor * S ((S (S pa_i_hj32_three_plus_left_product)) * pa_v_hj32_three_plus_left_product) + (pa_s_hj32_three_plus_left_product))) /\ pa_s_hj32_three_plus_left_product = pa_r_hj32_three_plus_left_product * pa_p_hj32_three_plus_left_product)))))))) -> (exists pa_b_hj32_three_plus_right pa_c_hj32_three_plus_right. ((forall pa_i_hj32_three_plus_right_repeat. (exists pa_lt_hj32_three_plus_right_repeat_bound. pa_lt_hj32_three_plus_right_repeat_bound + S pa_i_hj32_three_plus_right_repeat = 4 * m + 1) -> (((exists pa_h_hj32_three_plus_right_repeat_decoded. pa_h_hj32_three_plus_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_three_plus_right_repeat)) * pa_c_hj32_three_plus_right)) /\ exists pa_q_hj32_three_plus_right_repeat_decoded. pa_b_hj32_three_plus_right = pa_q_hj32_three_plus_right_repeat_decoded * S ((S (pa_i_hj32_three_plus_right_repeat)) * pa_c_hj32_three_plus_right) + (4)))) /\ (exists pa_u_hj32_three_plus_right_product pa_v_hj32_three_plus_right_product. ((((exists pa_h_hj32_three_plus_right_product_start. pa_h_hj32_three_plus_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_plus_right_product)) /\ exists pa_q_hj32_three_plus_right_product_start. pa_u_hj32_three_plus_right_product = pa_q_hj32_three_plus_right_product_start * S ((S (0)) * pa_v_hj32_three_plus_right_product) + (1))) /\ ((((exists pa_h_hj32_three_plus_right_product_terminal. pa_h_hj32_three_plus_right_product_terminal + S (y) = S ((S (4 * m + 1)) * pa_v_hj32_three_plus_right_product)) /\ exists pa_q_hj32_three_plus_right_product_terminal. pa_u_hj32_three_plus_right_product = pa_q_hj32_three_plus_right_product_terminal * S ((S (4 * m + 1)) * pa_v_hj32_three_plus_right_product) + (y))) /\ forall pa_i_hj32_three_plus_right_product. (exists pa_lt_hj32_three_plus_right_product_bound. pa_lt_hj32_three_plus_right_product_bound + S pa_i_hj32_three_plus_right_product = 4 * m + 1) -> exists pa_p_hj32_three_plus_right_product pa_r_hj32_three_plus_right_product pa_s_hj32_three_plus_right_product. ((((exists pa_h_hj32_three_plus_right_product_factor. pa_h_hj32_three_plus_right_product_factor + S (pa_p_hj32_three_plus_right_product) = S ((S (pa_i_hj32_three_plus_right_product)) * pa_c_hj32_three_plus_right)) /\ exists pa_q_hj32_three_plus_right_product_factor. pa_b_hj32_three_plus_right = pa_q_hj32_three_plus_right_product_factor * S ((S (pa_i_hj32_three_plus_right_product)) * pa_c_hj32_three_plus_right) + (pa_p_hj32_three_plus_right_product))) /\ ((((exists pa_h_hj32_three_plus_right_product_partial. pa_h_hj32_three_plus_right_product_partial + S (pa_r_hj32_three_plus_right_product) = S ((S (pa_i_hj32_three_plus_right_product)) * pa_v_hj32_three_plus_right_product)) /\ exists pa_q_hj32_three_plus_right_product_partial. pa_u_hj32_three_plus_right_product = pa_q_hj32_three_plus_right_product_partial * S ((S (pa_i_hj32_three_plus_right_product)) * pa_v_hj32_three_plus_right_product) + (pa_r_hj32_three_plus_right_product))) /\ ((((exists pa_h_hj32_three_plus_right_product_successor. pa_h_hj32_three_plus_right_product_successor + S (pa_s_hj32_three_plus_right_product) = S ((S (S pa_i_hj32_three_plus_right_product)) * pa_v_hj32_three_plus_right_product)) /\ exists pa_q_hj32_three_plus_right_product_successor. pa_u_hj32_three_plus_right_product = pa_q_hj32_three_plus_right_product_successor * S ((S (S pa_i_hj32_three_plus_right_product)) * pa_v_hj32_three_plus_right_product) + (pa_s_hj32_three_plus_right_product))) /\ pa_s_hj32_three_plus_right_product = pa_r_hj32_three_plus_right_product * pa_p_hj32_three_plus_right_product)))))))) -> (exists bqb_le_gap_hj32_three_plus_result. bqb_le_gap_hj32_three_plus_result + (x) = (y))Proof neighborhood
Direct theorem prerequisites
BT00W3 pow_block_bound_from_total BT00W4 pow_three_five_le_pow_four_four_from_total BT009X pow_add BT00PY pow_base_monotone BT00PV mul_le_mulDirect 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 (5)
01Fix variables and assumptionsL1–6
02Establish tp_p3_fiveL7–10
Establish this local claim before using it. It is not an additional assumption.
- L7
have tp_p3_five : ∃ hj32_local_value_tp_p3_five. Pow(3,5,hj32_local_value_tp_p3_five)Definitions: Pow(3,5,hj32_local_value_tp_p3_five)Original native command in the exact edition - L8
specialize htotal 3 - L9
specialize htotal 5 - L10
exact htotal
03Separate the logical casesL11–11
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L11
cases tp_p3_five
04Establish tp_p4_fourL12–15
Establish this local claim before using it. It is not an additional assumption.
- L12
have tp_p4_four : ∃ hj32_local_value_tp_p4_four. Pow(4,4,hj32_local_value_tp_p4_four)Definitions: Pow(4,4,hj32_local_value_tp_p4_four)Original native command in the exact edition - L13
specialize htotal 4 - L14
specialize htotal 4 - L15
exact htotal
05Separate the logical casesL16–16
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L16
cases tp_p4_four
06Establish tp_seedL17–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow three five le pow four four from total.
07Establish tp_p3_blockL24–27
Establish this local claim before using it. It is not an additional assumption.
- L24
have tp_p3_block : ∃ hj32_local_value_tp_p3_block. Pow(3,5 · m,hj32_local_value_tp_p3_block)Definitions: Pow(3,5 · m,hj32_local_value_tp_p3_block)Original native command in the exact edition - L25
specialize htotal 3 - L26
specialize htotal 5 * m - L27
exact htotal
08Separate the logical casesL28–28
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L28
cases tp_p3_block
09Establish tp_p4_blockL29–32
Establish this local claim before using it. It is not an additional assumption.
- L29
have tp_p4_block : ∃ hj32_local_value_tp_p4_block. Pow(4,4 · m,hj32_local_value_tp_p4_block)Definitions: Pow(4,4 · m,hj32_local_value_tp_p4_block)Original native command in the exact edition - L30
specialize htotal 4 - L31
specialize htotal 4 * m - L32
exact htotal
10Separate the logical casesL33–33
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L33
cases tp_p4_block
11Establish tp_block_boundL34–43
Establish this local claim before using it. It is not an additional assumption.
- L34
- L35
specialize pow_block_bound_from_total 3 - L36
specialize pow_block_bound_from_total 4 - L37
specialize pow_block_bound_from_total 5 - L38
specialize pow_block_bound_from_total 4 - L39
specialize pow_block_bound_from_total m - L40
specialize pow_block_bound_from_total x1 - L41
specialize pow_block_bound_from_total x2 - L42
specialize pow_block_bound_from_total x3 - L43
specialize pow_block_bound_from_total x4
12Use earlier factsL44–50
13Establish tp_p3_oneL51–54
Establish this local claim before using it. It is not an additional assumption.
- L51
have tp_p3_one : ∃ hj32_local_value_tp_p3_one. Pow(3,1,hj32_local_value_tp_p3_one)Definitions: Pow(3,1,hj32_local_value_tp_p3_one)Original native command in the exact edition - L52
specialize htotal 3 - L53
specialize htotal 1 - L54
exact htotal
14Separate the logical casesL55–55
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L55
cases tp_p3_one
15Establish tp_p4_oneL56–59
Establish this local claim before using it. It is not an additional assumption.
- L56
have tp_p4_one : ∃ hj32_local_value_tp_p4_one. Pow(4,1,hj32_local_value_tp_p4_one)Definitions: Pow(4,1,hj32_local_value_tp_p4_one)Original native command in the exact edition - L57
specialize htotal 4 - L58
specialize htotal 1 - L59
exact htotal
16Separate the logical casesL60–60
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L60
cases tp_p4_one
17Establish tp_baseL61–61
Establish this local claim before using it. It is not an additional assumption.
18Construct an explicit witnessL62–62
Supply the displayed value, then prove that it has the required property.
- L62
exists 1
19Calculate and transport equalitiesL63–63
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L63
norm_num
20Establish tp_one_boundL64–73
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow base monotone.
21Establish tp_left_productL74–83
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.
22Use earlier factsL84–86
23Establish tp_right_productL87–96
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.
24Use earlier factsL97–99
25Establish tp_resultL100–109
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.
- L100
have tp_result : Le(x3 · x5,x4 · x6)Definitions: Le(x3 · x5,x4 · x6)Original native command in the exact edition - L101
specialize mul_le_mul x3 - L102
specialize mul_le_mul x4 - L103
specialize mul_le_mul x5 - L104
specialize mul_le_mul x6 - L105
apply mul_le_mul - L106
exact tp_block_bound - L107
exact tp_one_bound - L108
rewrite <- tp_left_product at tp_result - L109
rewrite <- tp_right_product at tp_result
26Use earlier factsL110–110
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L110
exact tp_result
Original defined command ledger · 110 lines
- 0001
intro m - 0002
intro x - 0003
intro y - 0004
intro htotal - 0005
intro hx - 0006
intro hy - 0007
have tp_p3_five : ∃ hj32_local_value_tp_p3_five. Pow(3,5,hj32_local_value_tp_p3_five)Exact native replay line
have tp_p3_five : exists hj32_local_value_tp_p3_five. (exists pa_b_hj32_local_total_tp_p3_five pa_c_hj32_local_total_tp_p3_five. ((forall pa_i_hj32_local_total_tp_p3_five_repeat. (exists pa_lt_hj32_local_total_tp_p3_five_repeat_bound. pa_lt_hj32_local_total_tp_p3_five_repeat_bound + S pa_i_hj32_local_total_tp_p3_five_repeat = 5) -> (((exists pa_h_hj32_local_total_tp_p3_five_repeat_decoded. pa_h_hj32_local_total_tp_p3_five_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_tp_p3_five_repeat)) * pa_c_hj32_local_total_tp_p3_five)) /\ exists pa_q_hj32_local_total_tp_p3_five_repeat_decoded. pa_b_hj32_local_total_tp_p3_five = pa_q_hj32_local_total_tp_p3_five_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p3_five_repeat)) * pa_c_hj32_local_total_tp_p3_five) + (3)))) /\ (exists pa_u_hj32_local_total_tp_p3_five_product pa_v_hj32_local_total_tp_p3_five_product. ((((exists pa_h_hj32_local_total_tp_p3_five_product_start. pa_h_hj32_local_total_tp_p3_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p3_five_product)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_start. pa_u_hj32_local_total_tp_p3_five_product = pa_q_hj32_local_total_tp_p3_five_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p3_five_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p3_five_product_terminal. pa_h_hj32_local_total_tp_p3_five_product_terminal + S (hj32_local_value_tp_p3_five) = S ((S (5)) * pa_v_hj32_local_total_tp_p3_five_product)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_terminal. pa_u_hj32_local_total_tp_p3_five_product = pa_q_hj32_local_total_tp_p3_five_product_terminal * S ((S (5)) * pa_v_hj32_local_total_tp_p3_five_product) + (hj32_local_value_tp_p3_five))) /\ forall pa_i_hj32_local_total_tp_p3_five_product. (exists pa_lt_hj32_local_total_tp_p3_five_product_bound. pa_lt_hj32_local_total_tp_p3_five_product_bound + S pa_i_hj32_local_total_tp_p3_five_product = 5) -> exists pa_p_hj32_local_total_tp_p3_five_product pa_r_hj32_local_total_tp_p3_five_product pa_s_hj32_local_total_tp_p3_five_product. ((((exists pa_h_hj32_local_total_tp_p3_five_product_factor. pa_h_hj32_local_total_tp_p3_five_product_factor + S (pa_p_hj32_local_total_tp_p3_five_product) = S ((S (pa_i_hj32_local_total_tp_p3_five_product)) * pa_c_hj32_local_total_tp_p3_five)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_factor. pa_b_hj32_local_total_tp_p3_five = pa_q_hj32_local_total_tp_p3_five_product_factor * S ((S (pa_i_hj32_local_total_tp_p3_five_product)) * pa_c_hj32_local_total_tp_p3_five) + (pa_p_hj32_local_total_tp_p3_five_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_five_product_partial. pa_h_hj32_local_total_tp_p3_five_product_partial + S (pa_r_hj32_local_total_tp_p3_five_product) = S ((S (pa_i_hj32_local_total_tp_p3_five_product)) * pa_v_hj32_local_total_tp_p3_five_product)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_partial. pa_u_hj32_local_total_tp_p3_five_product = pa_q_hj32_local_total_tp_p3_five_product_partial * S ((S (pa_i_hj32_local_total_tp_p3_five_product)) * pa_v_hj32_local_total_tp_p3_five_product) + (pa_r_hj32_local_total_tp_p3_five_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_five_product_successor. pa_h_hj32_local_total_tp_p3_five_product_successor + S (pa_s_hj32_local_total_tp_p3_five_product) = S ((S (S pa_i_hj32_local_total_tp_p3_five_product)) * pa_v_hj32_local_total_tp_p3_five_product)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_successor. pa_u_hj32_local_total_tp_p3_five_product = pa_q_hj32_local_total_tp_p3_five_product_successor * S ((S (S pa_i_hj32_local_total_tp_p3_five_product)) * pa_v_hj32_local_total_tp_p3_five_product) + (pa_s_hj32_local_total_tp_p3_five_product))) /\ pa_s_hj32_local_total_tp_p3_five_product = pa_r_hj32_local_total_tp_p3_five_product * pa_p_hj32_local_total_tp_p3_five_product)))))))) - 0008
specialize htotal 3 - 0009
specialize htotal 5 - 0010
exact htotal - 0011
cases tp_p3_five - 0012
have tp_p4_four : ∃ hj32_local_value_tp_p4_four. Pow(4,4,hj32_local_value_tp_p4_four)Exact native replay line
have tp_p4_four : exists hj32_local_value_tp_p4_four. (exists pa_b_hj32_local_total_tp_p4_four pa_c_hj32_local_total_tp_p4_four. ((forall pa_i_hj32_local_total_tp_p4_four_repeat. (exists pa_lt_hj32_local_total_tp_p4_four_repeat_bound. pa_lt_hj32_local_total_tp_p4_four_repeat_bound + S pa_i_hj32_local_total_tp_p4_four_repeat = 4) -> (((exists pa_h_hj32_local_total_tp_p4_four_repeat_decoded. pa_h_hj32_local_total_tp_p4_four_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_tp_p4_four_repeat)) * pa_c_hj32_local_total_tp_p4_four)) /\ exists pa_q_hj32_local_total_tp_p4_four_repeat_decoded. pa_b_hj32_local_total_tp_p4_four = pa_q_hj32_local_total_tp_p4_four_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p4_four_repeat)) * pa_c_hj32_local_total_tp_p4_four) + (4)))) /\ (exists pa_u_hj32_local_total_tp_p4_four_product pa_v_hj32_local_total_tp_p4_four_product. ((((exists pa_h_hj32_local_total_tp_p4_four_product_start. pa_h_hj32_local_total_tp_p4_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p4_four_product)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_start. pa_u_hj32_local_total_tp_p4_four_product = pa_q_hj32_local_total_tp_p4_four_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p4_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p4_four_product_terminal. pa_h_hj32_local_total_tp_p4_four_product_terminal + S (hj32_local_value_tp_p4_four) = S ((S (4)) * pa_v_hj32_local_total_tp_p4_four_product)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_terminal. pa_u_hj32_local_total_tp_p4_four_product = pa_q_hj32_local_total_tp_p4_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_tp_p4_four_product) + (hj32_local_value_tp_p4_four))) /\ forall pa_i_hj32_local_total_tp_p4_four_product. (exists pa_lt_hj32_local_total_tp_p4_four_product_bound. pa_lt_hj32_local_total_tp_p4_four_product_bound + S pa_i_hj32_local_total_tp_p4_four_product = 4) -> exists pa_p_hj32_local_total_tp_p4_four_product pa_r_hj32_local_total_tp_p4_four_product pa_s_hj32_local_total_tp_p4_four_product. ((((exists pa_h_hj32_local_total_tp_p4_four_product_factor. pa_h_hj32_local_total_tp_p4_four_product_factor + S (pa_p_hj32_local_total_tp_p4_four_product) = S ((S (pa_i_hj32_local_total_tp_p4_four_product)) * pa_c_hj32_local_total_tp_p4_four)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_factor. pa_b_hj32_local_total_tp_p4_four = pa_q_hj32_local_total_tp_p4_four_product_factor * S ((S (pa_i_hj32_local_total_tp_p4_four_product)) * pa_c_hj32_local_total_tp_p4_four) + (pa_p_hj32_local_total_tp_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_four_product_partial. pa_h_hj32_local_total_tp_p4_four_product_partial + S (pa_r_hj32_local_total_tp_p4_four_product) = S ((S (pa_i_hj32_local_total_tp_p4_four_product)) * pa_v_hj32_local_total_tp_p4_four_product)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_partial. pa_u_hj32_local_total_tp_p4_four_product = pa_q_hj32_local_total_tp_p4_four_product_partial * S ((S (pa_i_hj32_local_total_tp_p4_four_product)) * pa_v_hj32_local_total_tp_p4_four_product) + (pa_r_hj32_local_total_tp_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_four_product_successor. pa_h_hj32_local_total_tp_p4_four_product_successor + S (pa_s_hj32_local_total_tp_p4_four_product) = S ((S (S pa_i_hj32_local_total_tp_p4_four_product)) * pa_v_hj32_local_total_tp_p4_four_product)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_successor. pa_u_hj32_local_total_tp_p4_four_product = pa_q_hj32_local_total_tp_p4_four_product_successor * S ((S (S pa_i_hj32_local_total_tp_p4_four_product)) * pa_v_hj32_local_total_tp_p4_four_product) + (pa_s_hj32_local_total_tp_p4_four_product))) /\ pa_s_hj32_local_total_tp_p4_four_product = pa_r_hj32_local_total_tp_p4_four_product * pa_p_hj32_local_total_tp_p4_four_product)))))))) - 0013
specialize htotal 4 - 0014
specialize htotal 4 - 0015
exact htotal - 0016
cases tp_p4_four - 0017
have tp_seed : Le(x1,x2)Exact native replay line
have tp_seed : exists bqb_le_gap_hj32_tp_seed. bqb_le_gap_hj32_tp_seed + (x1) = (x2) - 0018
specialize pow_three_five_le_pow_four_four_from_total x1 - 0019
specialize pow_three_five_le_pow_four_four_from_total x2 - 0020
apply pow_three_five_le_pow_four_four_from_total - 0021
exact htotal - 0022
exact tp_p3_five_witness - 0023
exact tp_p4_four_witness - 0024
have tp_p3_block : ∃ hj32_local_value_tp_p3_block. Pow(3,5 · m,hj32_local_value_tp_p3_block)Exact native replay line
have tp_p3_block : exists hj32_local_value_tp_p3_block. (exists pa_b_hj32_local_total_tp_p3_block pa_c_hj32_local_total_tp_p3_block. ((forall pa_i_hj32_local_total_tp_p3_block_repeat. (exists pa_lt_hj32_local_total_tp_p3_block_repeat_bound. pa_lt_hj32_local_total_tp_p3_block_repeat_bound + S pa_i_hj32_local_total_tp_p3_block_repeat = 5 * m) -> (((exists pa_h_hj32_local_total_tp_p3_block_repeat_decoded. pa_h_hj32_local_total_tp_p3_block_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_tp_p3_block_repeat)) * pa_c_hj32_local_total_tp_p3_block)) /\ exists pa_q_hj32_local_total_tp_p3_block_repeat_decoded. pa_b_hj32_local_total_tp_p3_block = pa_q_hj32_local_total_tp_p3_block_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p3_block_repeat)) * pa_c_hj32_local_total_tp_p3_block) + (3)))) /\ (exists pa_u_hj32_local_total_tp_p3_block_product pa_v_hj32_local_total_tp_p3_block_product. ((((exists pa_h_hj32_local_total_tp_p3_block_product_start. pa_h_hj32_local_total_tp_p3_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p3_block_product)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_start. pa_u_hj32_local_total_tp_p3_block_product = pa_q_hj32_local_total_tp_p3_block_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p3_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p3_block_product_terminal. pa_h_hj32_local_total_tp_p3_block_product_terminal + S (hj32_local_value_tp_p3_block) = S ((S (5 * m)) * pa_v_hj32_local_total_tp_p3_block_product)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_terminal. pa_u_hj32_local_total_tp_p3_block_product = pa_q_hj32_local_total_tp_p3_block_product_terminal * S ((S (5 * m)) * pa_v_hj32_local_total_tp_p3_block_product) + (hj32_local_value_tp_p3_block))) /\ forall pa_i_hj32_local_total_tp_p3_block_product. (exists pa_lt_hj32_local_total_tp_p3_block_product_bound. pa_lt_hj32_local_total_tp_p3_block_product_bound + S pa_i_hj32_local_total_tp_p3_block_product = 5 * m) -> exists pa_p_hj32_local_total_tp_p3_block_product pa_r_hj32_local_total_tp_p3_block_product pa_s_hj32_local_total_tp_p3_block_product. ((((exists pa_h_hj32_local_total_tp_p3_block_product_factor. pa_h_hj32_local_total_tp_p3_block_product_factor + S (pa_p_hj32_local_total_tp_p3_block_product) = S ((S (pa_i_hj32_local_total_tp_p3_block_product)) * pa_c_hj32_local_total_tp_p3_block)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_factor. pa_b_hj32_local_total_tp_p3_block = pa_q_hj32_local_total_tp_p3_block_product_factor * S ((S (pa_i_hj32_local_total_tp_p3_block_product)) * pa_c_hj32_local_total_tp_p3_block) + (pa_p_hj32_local_total_tp_p3_block_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_block_product_partial. pa_h_hj32_local_total_tp_p3_block_product_partial + S (pa_r_hj32_local_total_tp_p3_block_product) = S ((S (pa_i_hj32_local_total_tp_p3_block_product)) * pa_v_hj32_local_total_tp_p3_block_product)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_partial. pa_u_hj32_local_total_tp_p3_block_product = pa_q_hj32_local_total_tp_p3_block_product_partial * S ((S (pa_i_hj32_local_total_tp_p3_block_product)) * pa_v_hj32_local_total_tp_p3_block_product) + (pa_r_hj32_local_total_tp_p3_block_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_block_product_successor. pa_h_hj32_local_total_tp_p3_block_product_successor + S (pa_s_hj32_local_total_tp_p3_block_product) = S ((S (S pa_i_hj32_local_total_tp_p3_block_product)) * pa_v_hj32_local_total_tp_p3_block_product)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_successor. pa_u_hj32_local_total_tp_p3_block_product = pa_q_hj32_local_total_tp_p3_block_product_successor * S ((S (S pa_i_hj32_local_total_tp_p3_block_product)) * pa_v_hj32_local_total_tp_p3_block_product) + (pa_s_hj32_local_total_tp_p3_block_product))) /\ pa_s_hj32_local_total_tp_p3_block_product = pa_r_hj32_local_total_tp_p3_block_product * pa_p_hj32_local_total_tp_p3_block_product)))))))) - 0025
specialize htotal 3 - 0026
specialize htotal 5 * m - 0027
exact htotal - 0028
cases tp_p3_block - 0029
have tp_p4_block : ∃ hj32_local_value_tp_p4_block. Pow(4,4 · m,hj32_local_value_tp_p4_block)Exact native replay line
have tp_p4_block : exists hj32_local_value_tp_p4_block. (exists pa_b_hj32_local_total_tp_p4_block pa_c_hj32_local_total_tp_p4_block. ((forall pa_i_hj32_local_total_tp_p4_block_repeat. (exists pa_lt_hj32_local_total_tp_p4_block_repeat_bound. pa_lt_hj32_local_total_tp_p4_block_repeat_bound + S pa_i_hj32_local_total_tp_p4_block_repeat = 4 * m) -> (((exists pa_h_hj32_local_total_tp_p4_block_repeat_decoded. pa_h_hj32_local_total_tp_p4_block_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_tp_p4_block_repeat)) * pa_c_hj32_local_total_tp_p4_block)) /\ exists pa_q_hj32_local_total_tp_p4_block_repeat_decoded. pa_b_hj32_local_total_tp_p4_block = pa_q_hj32_local_total_tp_p4_block_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p4_block_repeat)) * pa_c_hj32_local_total_tp_p4_block) + (4)))) /\ (exists pa_u_hj32_local_total_tp_p4_block_product pa_v_hj32_local_total_tp_p4_block_product. ((((exists pa_h_hj32_local_total_tp_p4_block_product_start. pa_h_hj32_local_total_tp_p4_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p4_block_product)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_start. pa_u_hj32_local_total_tp_p4_block_product = pa_q_hj32_local_total_tp_p4_block_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p4_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p4_block_product_terminal. pa_h_hj32_local_total_tp_p4_block_product_terminal + S (hj32_local_value_tp_p4_block) = S ((S (4 * m)) * pa_v_hj32_local_total_tp_p4_block_product)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_terminal. pa_u_hj32_local_total_tp_p4_block_product = pa_q_hj32_local_total_tp_p4_block_product_terminal * S ((S (4 * m)) * pa_v_hj32_local_total_tp_p4_block_product) + (hj32_local_value_tp_p4_block))) /\ forall pa_i_hj32_local_total_tp_p4_block_product. (exists pa_lt_hj32_local_total_tp_p4_block_product_bound. pa_lt_hj32_local_total_tp_p4_block_product_bound + S pa_i_hj32_local_total_tp_p4_block_product = 4 * m) -> exists pa_p_hj32_local_total_tp_p4_block_product pa_r_hj32_local_total_tp_p4_block_product pa_s_hj32_local_total_tp_p4_block_product. ((((exists pa_h_hj32_local_total_tp_p4_block_product_factor. pa_h_hj32_local_total_tp_p4_block_product_factor + S (pa_p_hj32_local_total_tp_p4_block_product) = S ((S (pa_i_hj32_local_total_tp_p4_block_product)) * pa_c_hj32_local_total_tp_p4_block)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_factor. pa_b_hj32_local_total_tp_p4_block = pa_q_hj32_local_total_tp_p4_block_product_factor * S ((S (pa_i_hj32_local_total_tp_p4_block_product)) * pa_c_hj32_local_total_tp_p4_block) + (pa_p_hj32_local_total_tp_p4_block_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_block_product_partial. pa_h_hj32_local_total_tp_p4_block_product_partial + S (pa_r_hj32_local_total_tp_p4_block_product) = S ((S (pa_i_hj32_local_total_tp_p4_block_product)) * pa_v_hj32_local_total_tp_p4_block_product)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_partial. pa_u_hj32_local_total_tp_p4_block_product = pa_q_hj32_local_total_tp_p4_block_product_partial * S ((S (pa_i_hj32_local_total_tp_p4_block_product)) * pa_v_hj32_local_total_tp_p4_block_product) + (pa_r_hj32_local_total_tp_p4_block_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_block_product_successor. pa_h_hj32_local_total_tp_p4_block_product_successor + S (pa_s_hj32_local_total_tp_p4_block_product) = S ((S (S pa_i_hj32_local_total_tp_p4_block_product)) * pa_v_hj32_local_total_tp_p4_block_product)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_successor. pa_u_hj32_local_total_tp_p4_block_product = pa_q_hj32_local_total_tp_p4_block_product_successor * S ((S (S pa_i_hj32_local_total_tp_p4_block_product)) * pa_v_hj32_local_total_tp_p4_block_product) + (pa_s_hj32_local_total_tp_p4_block_product))) /\ pa_s_hj32_local_total_tp_p4_block_product = pa_r_hj32_local_total_tp_p4_block_product * pa_p_hj32_local_total_tp_p4_block_product)))))))) - 0030
specialize htotal 4 - 0031
specialize htotal 4 * m - 0032
exact htotal - 0033
cases tp_p4_block - 0034
have tp_block_bound : Le(x3,x4)Exact native replay line
have tp_block_bound : exists bqb_le_gap_hj32_local_block_bound_tp_block_bound. bqb_le_gap_hj32_local_block_bound_tp_block_bound + (x3) = (x4) - 0035
specialize pow_block_bound_from_total 3 - 0036
specialize pow_block_bound_from_total 4 - 0037
specialize pow_block_bound_from_total 5 - 0038
specialize pow_block_bound_from_total 4 - 0039
specialize pow_block_bound_from_total m - 0040
specialize pow_block_bound_from_total x1 - 0041
specialize pow_block_bound_from_total x2 - 0042
specialize pow_block_bound_from_total x3 - 0043
specialize pow_block_bound_from_total x4 - 0044
apply pow_block_bound_from_total - 0045
exact htotal - 0046
exact tp_p3_five_witness - 0047
exact tp_p4_four_witness - 0048
exact tp_seed - 0049
exact tp_p3_block_witness - 0050
exact tp_p4_block_witness - 0051
have tp_p3_one : ∃ hj32_local_value_tp_p3_one. Pow(3,1,hj32_local_value_tp_p3_one)Exact native replay line
have tp_p3_one : exists hj32_local_value_tp_p3_one. (exists pa_b_hj32_local_total_tp_p3_one pa_c_hj32_local_total_tp_p3_one. ((forall pa_i_hj32_local_total_tp_p3_one_repeat. (exists pa_lt_hj32_local_total_tp_p3_one_repeat_bound. pa_lt_hj32_local_total_tp_p3_one_repeat_bound + S pa_i_hj32_local_total_tp_p3_one_repeat = 1) -> (((exists pa_h_hj32_local_total_tp_p3_one_repeat_decoded. pa_h_hj32_local_total_tp_p3_one_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_tp_p3_one_repeat)) * pa_c_hj32_local_total_tp_p3_one)) /\ exists pa_q_hj32_local_total_tp_p3_one_repeat_decoded. pa_b_hj32_local_total_tp_p3_one = pa_q_hj32_local_total_tp_p3_one_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p3_one_repeat)) * pa_c_hj32_local_total_tp_p3_one) + (3)))) /\ (exists pa_u_hj32_local_total_tp_p3_one_product pa_v_hj32_local_total_tp_p3_one_product. ((((exists pa_h_hj32_local_total_tp_p3_one_product_start. pa_h_hj32_local_total_tp_p3_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p3_one_product)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_start. pa_u_hj32_local_total_tp_p3_one_product = pa_q_hj32_local_total_tp_p3_one_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p3_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p3_one_product_terminal. pa_h_hj32_local_total_tp_p3_one_product_terminal + S (hj32_local_value_tp_p3_one) = S ((S (1)) * pa_v_hj32_local_total_tp_p3_one_product)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_terminal. pa_u_hj32_local_total_tp_p3_one_product = pa_q_hj32_local_total_tp_p3_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_tp_p3_one_product) + (hj32_local_value_tp_p3_one))) /\ forall pa_i_hj32_local_total_tp_p3_one_product. (exists pa_lt_hj32_local_total_tp_p3_one_product_bound. pa_lt_hj32_local_total_tp_p3_one_product_bound + S pa_i_hj32_local_total_tp_p3_one_product = 1) -> exists pa_p_hj32_local_total_tp_p3_one_product pa_r_hj32_local_total_tp_p3_one_product pa_s_hj32_local_total_tp_p3_one_product. ((((exists pa_h_hj32_local_total_tp_p3_one_product_factor. pa_h_hj32_local_total_tp_p3_one_product_factor + S (pa_p_hj32_local_total_tp_p3_one_product) = S ((S (pa_i_hj32_local_total_tp_p3_one_product)) * pa_c_hj32_local_total_tp_p3_one)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_factor. pa_b_hj32_local_total_tp_p3_one = pa_q_hj32_local_total_tp_p3_one_product_factor * S ((S (pa_i_hj32_local_total_tp_p3_one_product)) * pa_c_hj32_local_total_tp_p3_one) + (pa_p_hj32_local_total_tp_p3_one_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_one_product_partial. pa_h_hj32_local_total_tp_p3_one_product_partial + S (pa_r_hj32_local_total_tp_p3_one_product) = S ((S (pa_i_hj32_local_total_tp_p3_one_product)) * pa_v_hj32_local_total_tp_p3_one_product)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_partial. pa_u_hj32_local_total_tp_p3_one_product = pa_q_hj32_local_total_tp_p3_one_product_partial * S ((S (pa_i_hj32_local_total_tp_p3_one_product)) * pa_v_hj32_local_total_tp_p3_one_product) + (pa_r_hj32_local_total_tp_p3_one_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_one_product_successor. pa_h_hj32_local_total_tp_p3_one_product_successor + S (pa_s_hj32_local_total_tp_p3_one_product) = S ((S (S pa_i_hj32_local_total_tp_p3_one_product)) * pa_v_hj32_local_total_tp_p3_one_product)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_successor. pa_u_hj32_local_total_tp_p3_one_product = pa_q_hj32_local_total_tp_p3_one_product_successor * S ((S (S pa_i_hj32_local_total_tp_p3_one_product)) * pa_v_hj32_local_total_tp_p3_one_product) + (pa_s_hj32_local_total_tp_p3_one_product))) /\ pa_s_hj32_local_total_tp_p3_one_product = pa_r_hj32_local_total_tp_p3_one_product * pa_p_hj32_local_total_tp_p3_one_product)))))))) - 0052
specialize htotal 3 - 0053
specialize htotal 1 - 0054
exact htotal - 0055
cases tp_p3_one - 0056
have tp_p4_one : ∃ hj32_local_value_tp_p4_one. Pow(4,1,hj32_local_value_tp_p4_one)Exact native replay line
have tp_p4_one : exists hj32_local_value_tp_p4_one. (exists pa_b_hj32_local_total_tp_p4_one pa_c_hj32_local_total_tp_p4_one. ((forall pa_i_hj32_local_total_tp_p4_one_repeat. (exists pa_lt_hj32_local_total_tp_p4_one_repeat_bound. pa_lt_hj32_local_total_tp_p4_one_repeat_bound + S pa_i_hj32_local_total_tp_p4_one_repeat = 1) -> (((exists pa_h_hj32_local_total_tp_p4_one_repeat_decoded. pa_h_hj32_local_total_tp_p4_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_tp_p4_one_repeat)) * pa_c_hj32_local_total_tp_p4_one)) /\ exists pa_q_hj32_local_total_tp_p4_one_repeat_decoded. pa_b_hj32_local_total_tp_p4_one = pa_q_hj32_local_total_tp_p4_one_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p4_one_repeat)) * pa_c_hj32_local_total_tp_p4_one) + (4)))) /\ (exists pa_u_hj32_local_total_tp_p4_one_product pa_v_hj32_local_total_tp_p4_one_product. ((((exists pa_h_hj32_local_total_tp_p4_one_product_start. pa_h_hj32_local_total_tp_p4_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p4_one_product)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_start. pa_u_hj32_local_total_tp_p4_one_product = pa_q_hj32_local_total_tp_p4_one_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p4_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p4_one_product_terminal. pa_h_hj32_local_total_tp_p4_one_product_terminal + S (hj32_local_value_tp_p4_one) = S ((S (1)) * pa_v_hj32_local_total_tp_p4_one_product)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_terminal. pa_u_hj32_local_total_tp_p4_one_product = pa_q_hj32_local_total_tp_p4_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_tp_p4_one_product) + (hj32_local_value_tp_p4_one))) /\ forall pa_i_hj32_local_total_tp_p4_one_product. (exists pa_lt_hj32_local_total_tp_p4_one_product_bound. pa_lt_hj32_local_total_tp_p4_one_product_bound + S pa_i_hj32_local_total_tp_p4_one_product = 1) -> exists pa_p_hj32_local_total_tp_p4_one_product pa_r_hj32_local_total_tp_p4_one_product pa_s_hj32_local_total_tp_p4_one_product. ((((exists pa_h_hj32_local_total_tp_p4_one_product_factor. pa_h_hj32_local_total_tp_p4_one_product_factor + S (pa_p_hj32_local_total_tp_p4_one_product) = S ((S (pa_i_hj32_local_total_tp_p4_one_product)) * pa_c_hj32_local_total_tp_p4_one)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_factor. pa_b_hj32_local_total_tp_p4_one = pa_q_hj32_local_total_tp_p4_one_product_factor * S ((S (pa_i_hj32_local_total_tp_p4_one_product)) * pa_c_hj32_local_total_tp_p4_one) + (pa_p_hj32_local_total_tp_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_one_product_partial. pa_h_hj32_local_total_tp_p4_one_product_partial + S (pa_r_hj32_local_total_tp_p4_one_product) = S ((S (pa_i_hj32_local_total_tp_p4_one_product)) * pa_v_hj32_local_total_tp_p4_one_product)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_partial. pa_u_hj32_local_total_tp_p4_one_product = pa_q_hj32_local_total_tp_p4_one_product_partial * S ((S (pa_i_hj32_local_total_tp_p4_one_product)) * pa_v_hj32_local_total_tp_p4_one_product) + (pa_r_hj32_local_total_tp_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_one_product_successor. pa_h_hj32_local_total_tp_p4_one_product_successor + S (pa_s_hj32_local_total_tp_p4_one_product) = S ((S (S pa_i_hj32_local_total_tp_p4_one_product)) * pa_v_hj32_local_total_tp_p4_one_product)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_successor. pa_u_hj32_local_total_tp_p4_one_product = pa_q_hj32_local_total_tp_p4_one_product_successor * S ((S (S pa_i_hj32_local_total_tp_p4_one_product)) * pa_v_hj32_local_total_tp_p4_one_product) + (pa_s_hj32_local_total_tp_p4_one_product))) /\ pa_s_hj32_local_total_tp_p4_one_product = pa_r_hj32_local_total_tp_p4_one_product * pa_p_hj32_local_total_tp_p4_one_product)))))))) - 0057
specialize htotal 4 - 0058
specialize htotal 1 - 0059
exact htotal - 0060
cases tp_p4_one - 0061
have tp_base : Lt(2,4)Exact native replay line
have tp_base : exists bqb_le_gap_hj32_tp_base. bqb_le_gap_hj32_tp_base + (3) = (4) - 0062
exists 1 - 0063
norm_num - 0064
have tp_one_bound : Le(x5,x6)Exact native replay line
have tp_one_bound : exists bqb_le_gap_hj32_local_base_bound_tp_one_bound. bqb_le_gap_hj32_local_base_bound_tp_one_bound + (x5) = (x6) - 0065
specialize pow_base_monotone 3 - 0066
specialize pow_base_monotone 4 - 0067
specialize pow_base_monotone 1 - 0068
specialize pow_base_monotone x5 - 0069
specialize pow_base_monotone x6 - 0070
apply pow_base_monotone - 0071
exact tp_base - 0072
exact tp_p3_one_witness - 0073
exact tp_p4_one_witness - 0074
have tp_left_product : x = x3 * x5 - 0075
specialize pow_add 3 - 0076
specialize pow_add 5 * m - 0077
specialize pow_add 1 - 0078
specialize pow_add 5 * m + 1 - 0079
specialize pow_add x3 - 0080
specialize pow_add x5 - 0081
specialize pow_add x - 0082
apply pow_add - 0083
refl - 0084
exact tp_p3_block_witness - 0085
exact tp_p3_one_witness - 0086
exact hx - 0087
have tp_right_product : y = x4 * x6 - 0088
specialize pow_add 4 - 0089
specialize pow_add 4 * m - 0090
specialize pow_add 1 - 0091
specialize pow_add 4 * m + 1 - 0092
specialize pow_add x4 - 0093
specialize pow_add x6 - 0094
specialize pow_add y - 0095
apply pow_add - 0096
refl - 0097
exact tp_p4_block_witness - 0098
exact tp_p4_one_witness - 0099
exact hy - 0100
have tp_result : Le(x3 · x5,x4 · x6)Exact native replay line
have tp_result : exists bqb_le_gap_hj32_local_product_bound_tp_result. bqb_le_gap_hj32_local_product_bound_tp_result + (x3 * x5) = (x4 * x6) - 0101
specialize mul_le_mul x3 - 0102
specialize mul_le_mul x4 - 0103
specialize mul_le_mul x5 - 0104
specialize mul_le_mul x6 - 0105
apply mul_le_mul - 0106
exact tp_block_bound - 0107
exact tp_one_bound - 0108
rewrite <- tp_left_product at tp_result - 0109
rewrite <- tp_right_product at tp_result - 0110
exact tp_result