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
∀ s. ∀ j. ∀ g. (∀ x. ∀ y. ∃ z. Pow(x,y,z)) → Lt(31,s) → Le(s,37) → Pow(s + 7,12,j) → Pow(4,s + 5,g) → Le(j,g)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
6 occurrences
In local proof propositions
20 occurrences
Exact expanded native-PA statement
forall s j g. (forall bpt_a_hj32_base bpt_e_hj32_base. exists bpt_x_hj32_base. (exists ff_b_bpt_value_hj32_base ff_c_bpt_value_hj32_base. ((forall ff_i_bpt_value_hj32_base_repeat. (exists ff_lt_bpt_value_hj32_base_repeat_bound. ff_lt_bpt_value_hj32_base_repeat_bound + S ff_i_bpt_value_hj32_base_repeat = bpt_e_hj32_base) -> (((exists ff_h_bpt_value_hj32_base_repeat_decoded. ff_h_bpt_value_hj32_base_repeat_decoded + S (bpt_a_hj32_base) = S ((S (ff_i_bpt_value_hj32_base_repeat)) * ff_c_bpt_value_hj32_base)) /\ exists ff_q_bpt_value_hj32_base_repeat_decoded. ff_b_bpt_value_hj32_base = ff_q_bpt_value_hj32_base_repeat_decoded * S ((S (ff_i_bpt_value_hj32_base_repeat)) * ff_c_bpt_value_hj32_base) + (bpt_a_hj32_base)))) /\ (exists ff_u_bpt_value_hj32_base_product ff_v_bpt_value_hj32_base_product. ((((exists ff_h_bpt_value_hj32_base_product_start. ff_h_bpt_value_hj32_base_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_start. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_start * S ((S (0)) * ff_v_bpt_value_hj32_base_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_base_product_terminal. ff_h_bpt_value_hj32_base_product_terminal + S (bpt_x_hj32_base) = S ((S (bpt_e_hj32_base)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_terminal. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_terminal * S ((S (bpt_e_hj32_base)) * ff_v_bpt_value_hj32_base_product) + (bpt_x_hj32_base))) /\ forall ff_i_bpt_value_hj32_base_product. (exists ff_lt_bpt_value_hj32_base_product_bound. ff_lt_bpt_value_hj32_base_product_bound + S ff_i_bpt_value_hj32_base_product = bpt_e_hj32_base) -> exists ff_p_bpt_value_hj32_base_product ff_r_bpt_value_hj32_base_product ff_s_bpt_value_hj32_base_product. ((((exists ff_h_bpt_value_hj32_base_product_factor. ff_h_bpt_value_hj32_base_product_factor + S (ff_p_bpt_value_hj32_base_product) = S ((S (ff_i_bpt_value_hj32_base_product)) * ff_c_bpt_value_hj32_base)) /\ exists ff_q_bpt_value_hj32_base_product_factor. ff_b_bpt_value_hj32_base = ff_q_bpt_value_hj32_base_product_factor * S ((S (ff_i_bpt_value_hj32_base_product)) * ff_c_bpt_value_hj32_base) + (ff_p_bpt_value_hj32_base_product))) /\ ((((exists ff_h_bpt_value_hj32_base_product_partial. ff_h_bpt_value_hj32_base_product_partial + S (ff_r_bpt_value_hj32_base_product) = S ((S (ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_partial. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_partial * S ((S (ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product) + (ff_r_bpt_value_hj32_base_product))) /\ ((((exists ff_h_bpt_value_hj32_base_product_successor. ff_h_bpt_value_hj32_base_product_successor + S (ff_s_bpt_value_hj32_base_product) = S ((S (S ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_successor. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_successor * S ((S (S ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product) + (ff_s_bpt_value_hj32_base_product))) /\ ff_s_bpt_value_hj32_base_product = ff_r_bpt_value_hj32_base_product * ff_p_bpt_value_hj32_base_product))))))))) -> (exists bqb_le_gap_hj32_base_lower. bqb_le_gap_hj32_base_lower + (32) = (s)) -> (exists bqb_le_gap_hj32_base_upper. bqb_le_gap_hj32_base_upper + (s) = (37)) -> (exists pa_b_hj32_base_j pa_c_hj32_base_j. ((forall pa_i_hj32_base_j_repeat. (exists pa_lt_hj32_base_j_repeat_bound. pa_lt_hj32_base_j_repeat_bound + S pa_i_hj32_base_j_repeat = 12) -> (((exists pa_h_hj32_base_j_repeat_decoded. pa_h_hj32_base_j_repeat_decoded + S (s + 7) = S ((S (pa_i_hj32_base_j_repeat)) * pa_c_hj32_base_j)) /\ exists pa_q_hj32_base_j_repeat_decoded. pa_b_hj32_base_j = pa_q_hj32_base_j_repeat_decoded * S ((S (pa_i_hj32_base_j_repeat)) * pa_c_hj32_base_j) + (s + 7)))) /\ (exists pa_u_hj32_base_j_product pa_v_hj32_base_j_product. ((((exists pa_h_hj32_base_j_product_start. pa_h_hj32_base_j_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_start. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_start * S ((S (0)) * pa_v_hj32_base_j_product) + (1))) /\ ((((exists pa_h_hj32_base_j_product_terminal. pa_h_hj32_base_j_product_terminal + S (j) = S ((S (12)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_terminal. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_terminal * S ((S (12)) * pa_v_hj32_base_j_product) + (j))) /\ forall pa_i_hj32_base_j_product. (exists pa_lt_hj32_base_j_product_bound. pa_lt_hj32_base_j_product_bound + S pa_i_hj32_base_j_product = 12) -> exists pa_p_hj32_base_j_product pa_r_hj32_base_j_product pa_s_hj32_base_j_product. ((((exists pa_h_hj32_base_j_product_factor. pa_h_hj32_base_j_product_factor + S (pa_p_hj32_base_j_product) = S ((S (pa_i_hj32_base_j_product)) * pa_c_hj32_base_j)) /\ exists pa_q_hj32_base_j_product_factor. pa_b_hj32_base_j = pa_q_hj32_base_j_product_factor * S ((S (pa_i_hj32_base_j_product)) * pa_c_hj32_base_j) + (pa_p_hj32_base_j_product))) /\ ((((exists pa_h_hj32_base_j_product_partial. pa_h_hj32_base_j_product_partial + S (pa_r_hj32_base_j_product) = S ((S (pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_partial. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_partial * S ((S (pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product) + (pa_r_hj32_base_j_product))) /\ ((((exists pa_h_hj32_base_j_product_successor. pa_h_hj32_base_j_product_successor + S (pa_s_hj32_base_j_product) = S ((S (S pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_successor. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_successor * S ((S (S pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product) + (pa_s_hj32_base_j_product))) /\ pa_s_hj32_base_j_product = pa_r_hj32_base_j_product * pa_p_hj32_base_j_product)))))))) -> (exists pa_b_hj32_base_j_bound pa_c_hj32_base_j_bound. ((forall pa_i_hj32_base_j_bound_repeat. (exists pa_lt_hj32_base_j_bound_repeat_bound. pa_lt_hj32_base_j_bound_repeat_bound + S pa_i_hj32_base_j_bound_repeat = s + 5) -> (((exists pa_h_hj32_base_j_bound_repeat_decoded. pa_h_hj32_base_j_bound_repeat_decoded + S (4) = S ((S (pa_i_hj32_base_j_bound_repeat)) * pa_c_hj32_base_j_bound)) /\ exists pa_q_hj32_base_j_bound_repeat_decoded. pa_b_hj32_base_j_bound = pa_q_hj32_base_j_bound_repeat_decoded * S ((S (pa_i_hj32_base_j_bound_repeat)) * pa_c_hj32_base_j_bound) + (4)))) /\ (exists pa_u_hj32_base_j_bound_product pa_v_hj32_base_j_bound_product. ((((exists pa_h_hj32_base_j_bound_product_start. pa_h_hj32_base_j_bound_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_start. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_start * S ((S (0)) * pa_v_hj32_base_j_bound_product) + (1))) /\ ((((exists pa_h_hj32_base_j_bound_product_terminal. pa_h_hj32_base_j_bound_product_terminal + S (g) = S ((S (s + 5)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_terminal. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_terminal * S ((S (s + 5)) * pa_v_hj32_base_j_bound_product) + (g))) /\ forall pa_i_hj32_base_j_bound_product. (exists pa_lt_hj32_base_j_bound_product_bound. pa_lt_hj32_base_j_bound_product_bound + S pa_i_hj32_base_j_bound_product = s + 5) -> exists pa_p_hj32_base_j_bound_product pa_r_hj32_base_j_bound_product pa_s_hj32_base_j_bound_product. ((((exists pa_h_hj32_base_j_bound_product_factor. pa_h_hj32_base_j_bound_product_factor + S (pa_p_hj32_base_j_bound_product) = S ((S (pa_i_hj32_base_j_bound_product)) * pa_c_hj32_base_j_bound)) /\ exists pa_q_hj32_base_j_bound_product_factor. pa_b_hj32_base_j_bound = pa_q_hj32_base_j_bound_product_factor * S ((S (pa_i_hj32_base_j_bound_product)) * pa_c_hj32_base_j_bound) + (pa_p_hj32_base_j_bound_product))) /\ ((((exists pa_h_hj32_base_j_bound_product_partial. pa_h_hj32_base_j_bound_product_partial + S (pa_r_hj32_base_j_bound_product) = S ((S (pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_partial. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_partial * S ((S (pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product) + (pa_r_hj32_base_j_bound_product))) /\ ((((exists pa_h_hj32_base_j_bound_product_successor. pa_h_hj32_base_j_bound_product_successor + S (pa_s_hj32_base_j_bound_product) = S ((S (S pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_successor. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_successor * S ((S (S pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product) + (pa_s_hj32_base_j_bound_product))) /\ pa_s_hj32_base_j_bound_product = pa_r_hj32_base_j_bound_product * pa_p_hj32_base_j_bound_product)))))))) -> (exists bqb_le_gap_hj32_base_j_result. bqb_le_gap_hj32_base_j_result + (j) = (g))Proof neighborhood
Direct theorem prerequisites
BT00WL pow_eleven_double_block_le_pow_four_even_from_total BT00QV pow_mul_base BT009X pow_add BT00PY pow_base_monotone BT00SN pow_exponent_monotone_from_total BT00PV mul_le_mul BT000E le_refl BT000F le_trans BT0014 add_le_add_rightDirect 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 (9)
01Fix variables and assumptionsL1–8
02Establish j_p11_blockL9–12
Establish this local claim before using it. It is not an additional assumption.
- L9
have j_p11_block : ∃ hj32_local_value_j_p11_block. Pow(11,2 · 6,hj32_local_value_j_p11_block)Definitions: Pow(11,2 · 6,hj32_local_value_j_p11_block)Original native command in the exact edition - L10
specialize htotal 11 - L11
specialize htotal 2 * 6 - L12
exact htotal
03Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
cases j_p11_block
04Establish j_p4_twenty_oneL14–17
Establish this local claim before using it. It is not an additional assumption.
- L14
have j_p4_twenty_one : ∃ hj32_local_value_j_p4_twenty_one. Pow(4,21,hj32_local_value_j_p4_twenty_one)Definitions: Pow(4,21,hj32_local_value_j_p4_twenty_one)Original native command in the exact edition - L15
specialize htotal 4 - L16
specialize htotal 21 - L17
exact htotal
05Separate the logical casesL18–18
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L18
cases j_p4_twenty_one
06Establish j_parityL19–20
07Establish j_eleven_boundL21–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow eleven double block le pow four even from total.
- L21
- L22
specialize pow_eleven_double_block_le_pow_four_even_from_total 6 - L23
specialize pow_eleven_double_block_le_pow_four_even_from_total 21 - L24
specialize pow_eleven_double_block_le_pow_four_even_from_total x - L25
specialize pow_eleven_double_block_le_pow_four_even_from_total x1 - L26
apply pow_eleven_double_block_le_pow_four_even_from_total - L27
exact htotal - L28
exact j_parity - L29
exact j_p11_block_witness - L30
exact j_p4_twenty_one_witness
08Establish j_twelveL31–32
09Establish j_h_blockL33–38
Establish this local claim before using it. It is not an additional assumption.
- L33
have j_h_block : Pow(s + 7,2 · 6,j)Definitions: Pow(s + 7,2 · 6,j)Original native command in the exact edition - L34
rewrite j_twelve - L35
rewrite j_twelve - L36
rewrite j_twelve - L37
rewrite j_twelve - L38
exact hj
10Establish j_p4_blockL39–42
Establish this local claim before using it. It is not an additional assumption.
- L39
have j_p4_block : ∃ hj32_local_value_j_p4_block. Pow(4,2 · 6,hj32_local_value_j_p4_block)Definitions: Pow(4,2 · 6,hj32_local_value_j_p4_block)Original native command in the exact edition - L40
specialize htotal 4 - L41
specialize htotal 2 * 6 - L42
exact htotal
11Separate the logical casesL43–43
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L43
cases j_p4_block
12Establish j_p44_blockL44–47
Establish this local claim before using it. It is not an additional assumption.
- L44
have j_p44_block : ∃ hj32_local_value_j_p44_block. Pow(44,2 · 6,hj32_local_value_j_p44_block)Definitions: Pow(44,2 · 6,hj32_local_value_j_p44_block)Original native command in the exact edition - L45
specialize htotal 44 - L46
specialize htotal 2 * 6 - L47
exact htotal
13Separate the logical casesL48–48
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L48
cases j_p44_block
14Establish j_p4_thirty_threeL49–52
Establish this local claim before using it. It is not an additional assumption.
- L49
have j_p4_thirty_three : ∃ hj32_local_value_j_p4_thirty_three. Pow(4,33,hj32_local_value_j_p4_thirty_three)Definitions: Pow(4,33,hj32_local_value_j_p4_thirty_three)Original native command in the exact edition - L50
specialize htotal 4 - L51
specialize htotal 33 - L52
exact htotal
15Separate the logical casesL53–53
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L53
cases j_p4_thirty_three
16Establish j_product_44_graphL54–54
Establish this local claim before using it. It is not an additional assumption.
- L54
have j_product_44_graph : Pow(4 · 11,2 · 6,x3)Definitions: Pow(4 · 11,2 · 6,x3)Original native command in the exact edition
17Establish j_product_44_baseL55–59
18Establish j_product_44L60–69
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul base.
19Use earlier factsL70–70
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L70
exact j_product_44_graph
20Establish j_product_33L71–80
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.
21Use earlier factsL81–83
22Establish j_four_reflL84–86
Establish this local claim before using it. It is not an additional assumption.
23Establish j_product_boundL87–96
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.
- L87
have j_product_bound : Le(x2 · x,x2 · x1)Definitions: Le(x2 · x,x2 · x1)Original native command in the exact edition - L88
specialize mul_le_mul x2 - L89
specialize mul_le_mul x2 - L90
specialize mul_le_mul x - L91
specialize mul_le_mul x1 - L92
apply mul_le_mul - L93
exact j_four_refl - L94
exact j_eleven_bound - L95
rewrite <- j_product_44 at j_product_bound - L96
rewrite <- j_product_33 at j_product_bound
24Establish j_base_to_upperL97–102
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add le add right.
- L97
have j_base_to_upper : Le(s + 7,37 + 7)Definitions: Le(s + 7,37 + 7)Original native command in the exact edition - L98
specialize add_le_add_right s - L99
specialize add_le_add_right 37 - L100
specialize add_le_add_right 7 - L101
apply add_le_add_right - L102
exact hupper
25Establish j_upper_valueL103–104
26Establish j_base_boundL105–107
Establish this local claim before using it. It is not an additional assumption.
- L105
have j_base_bound : Le(s + 7,44)Definitions: Le(s + 7,44)Original native command in the exact edition - L106
rewrite j_upper_value at j_base_to_upper - L107
exact j_base_to_upper
27Establish j_to_44L108–117
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow base monotone.
28Establish j_to_thirty_threeL118–124
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
29Establish j_exponent_from_lowerL125–130
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add le add right.
- L125
have j_exponent_from_lower : Le(32 + 5,s + 5)Definitions: Le(32 + 5,s + 5)Original native command in the exact edition - L126
specialize add_le_add_right 32 - L127
specialize add_le_add_right s - L128
specialize add_le_add_right 5 - L129
apply add_le_add_right - L130
exact hlower
30Establish j_lower_valueL131–132
31Establish j_thirty_seven_to_targetL133–135
Establish this local claim before using it. It is not an additional assumption.
- L133
have j_thirty_seven_to_target : Lt(36,s + 5)Definitions: Lt(36,s + 5)Original native command in the exact edition - L134
rewrite j_lower_value at j_exponent_from_lower - L135
exact j_exponent_from_lower
32Establish j_seedL136–136
Establish this local claim before using it. It is not an additional assumption.
33Construct an explicit witnessL137–137
Supply the displayed value, then prove that it has the required property.
- L137
exists 4
34Calculate and transport equalitiesL138–138
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L138
norm_num
35Establish j_exponent_boundL139–145
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
- L139
have j_exponent_bound : Lt(32,s + 5)Definitions: Lt(32,s + 5)Original native command in the exact edition - L140
specialize le_trans 33 - L141
specialize le_trans 37 - L142
specialize le_trans s + 5 - L143
apply le_trans - L144
exact j_seed - L145
exact j_thirty_seven_to_target
36Establish j_growthL146–153
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow exponent monotone from total.
- L146
- L147
specialize pow_exponent_monotone_from_total 4 - L148
specialize pow_exponent_monotone_from_total 33 - L149
specialize pow_exponent_monotone_from_total s + 5 - L150
specialize pow_exponent_monotone_from_total x4 - L151
specialize pow_exponent_monotone_from_total g - L152
apply pow_exponent_monotone_from_total - L153
exact htotal
37Construct an explicit witnessL154–154
Supply the displayed value, then prove that it has the required property.
- L154
exists 3
38Calculate and transport equalitiesL155–155
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L155
norm_num
39Use earlier factsL156–158
40Establish j_resultL159–166
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
Original defined command ledger · 166 lines
- 0001
intro s - 0002
intro j - 0003
intro g - 0004
intro htotal - 0005
intro hlower - 0006
intro hupper - 0007
intro hj - 0008
intro hg - 0009
have j_p11_block : ∃ hj32_local_value_j_p11_block. Pow(11,2 · 6,hj32_local_value_j_p11_block)Exact native replay line
have j_p11_block : exists hj32_local_value_j_p11_block. (exists pa_b_hj32_local_total_j_p11_block pa_c_hj32_local_total_j_p11_block. ((forall pa_i_hj32_local_total_j_p11_block_repeat. (exists pa_lt_hj32_local_total_j_p11_block_repeat_bound. pa_lt_hj32_local_total_j_p11_block_repeat_bound + S pa_i_hj32_local_total_j_p11_block_repeat = 2 * 6) -> (((exists pa_h_hj32_local_total_j_p11_block_repeat_decoded. pa_h_hj32_local_total_j_p11_block_repeat_decoded + S (11) = S ((S (pa_i_hj32_local_total_j_p11_block_repeat)) * pa_c_hj32_local_total_j_p11_block)) /\ exists pa_q_hj32_local_total_j_p11_block_repeat_decoded. pa_b_hj32_local_total_j_p11_block = pa_q_hj32_local_total_j_p11_block_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p11_block_repeat)) * pa_c_hj32_local_total_j_p11_block) + (11)))) /\ (exists pa_u_hj32_local_total_j_p11_block_product pa_v_hj32_local_total_j_p11_block_product. ((((exists pa_h_hj32_local_total_j_p11_block_product_start. pa_h_hj32_local_total_j_p11_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p11_block_product)) /\ exists pa_q_hj32_local_total_j_p11_block_product_start. pa_u_hj32_local_total_j_p11_block_product = pa_q_hj32_local_total_j_p11_block_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p11_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p11_block_product_terminal. pa_h_hj32_local_total_j_p11_block_product_terminal + S (hj32_local_value_j_p11_block) = S ((S (2 * 6)) * pa_v_hj32_local_total_j_p11_block_product)) /\ exists pa_q_hj32_local_total_j_p11_block_product_terminal. pa_u_hj32_local_total_j_p11_block_product = pa_q_hj32_local_total_j_p11_block_product_terminal * S ((S (2 * 6)) * pa_v_hj32_local_total_j_p11_block_product) + (hj32_local_value_j_p11_block))) /\ forall pa_i_hj32_local_total_j_p11_block_product. (exists pa_lt_hj32_local_total_j_p11_block_product_bound. pa_lt_hj32_local_total_j_p11_block_product_bound + S pa_i_hj32_local_total_j_p11_block_product = 2 * 6) -> exists pa_p_hj32_local_total_j_p11_block_product pa_r_hj32_local_total_j_p11_block_product pa_s_hj32_local_total_j_p11_block_product. ((((exists pa_h_hj32_local_total_j_p11_block_product_factor. pa_h_hj32_local_total_j_p11_block_product_factor + S (pa_p_hj32_local_total_j_p11_block_product) = S ((S (pa_i_hj32_local_total_j_p11_block_product)) * pa_c_hj32_local_total_j_p11_block)) /\ exists pa_q_hj32_local_total_j_p11_block_product_factor. pa_b_hj32_local_total_j_p11_block = pa_q_hj32_local_total_j_p11_block_product_factor * S ((S (pa_i_hj32_local_total_j_p11_block_product)) * pa_c_hj32_local_total_j_p11_block) + (pa_p_hj32_local_total_j_p11_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p11_block_product_partial. pa_h_hj32_local_total_j_p11_block_product_partial + S (pa_r_hj32_local_total_j_p11_block_product) = S ((S (pa_i_hj32_local_total_j_p11_block_product)) * pa_v_hj32_local_total_j_p11_block_product)) /\ exists pa_q_hj32_local_total_j_p11_block_product_partial. pa_u_hj32_local_total_j_p11_block_product = pa_q_hj32_local_total_j_p11_block_product_partial * S ((S (pa_i_hj32_local_total_j_p11_block_product)) * pa_v_hj32_local_total_j_p11_block_product) + (pa_r_hj32_local_total_j_p11_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p11_block_product_successor. pa_h_hj32_local_total_j_p11_block_product_successor + S (pa_s_hj32_local_total_j_p11_block_product) = S ((S (S pa_i_hj32_local_total_j_p11_block_product)) * pa_v_hj32_local_total_j_p11_block_product)) /\ exists pa_q_hj32_local_total_j_p11_block_product_successor. pa_u_hj32_local_total_j_p11_block_product = pa_q_hj32_local_total_j_p11_block_product_successor * S ((S (S pa_i_hj32_local_total_j_p11_block_product)) * pa_v_hj32_local_total_j_p11_block_product) + (pa_s_hj32_local_total_j_p11_block_product))) /\ pa_s_hj32_local_total_j_p11_block_product = pa_r_hj32_local_total_j_p11_block_product * pa_p_hj32_local_total_j_p11_block_product)))))))) - 0010
specialize htotal 11 - 0011
specialize htotal 2 * 6 - 0012
exact htotal - 0013
cases j_p11_block - 0014
have j_p4_twenty_one : ∃ hj32_local_value_j_p4_twenty_one. Pow(4,21,hj32_local_value_j_p4_twenty_one)Exact native replay line
have j_p4_twenty_one : exists hj32_local_value_j_p4_twenty_one. (exists pa_b_hj32_local_total_j_p4_twenty_one pa_c_hj32_local_total_j_p4_twenty_one. ((forall pa_i_hj32_local_total_j_p4_twenty_one_repeat. (exists pa_lt_hj32_local_total_j_p4_twenty_one_repeat_bound. pa_lt_hj32_local_total_j_p4_twenty_one_repeat_bound + S pa_i_hj32_local_total_j_p4_twenty_one_repeat = 21) -> (((exists pa_h_hj32_local_total_j_p4_twenty_one_repeat_decoded. pa_h_hj32_local_total_j_p4_twenty_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_j_p4_twenty_one_repeat)) * pa_c_hj32_local_total_j_p4_twenty_one)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_repeat_decoded. pa_b_hj32_local_total_j_p4_twenty_one = pa_q_hj32_local_total_j_p4_twenty_one_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p4_twenty_one_repeat)) * pa_c_hj32_local_total_j_p4_twenty_one) + (4)))) /\ (exists pa_u_hj32_local_total_j_p4_twenty_one_product pa_v_hj32_local_total_j_p4_twenty_one_product. ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_start. pa_h_hj32_local_total_j_p4_twenty_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p4_twenty_one_product)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_start. pa_u_hj32_local_total_j_p4_twenty_one_product = pa_q_hj32_local_total_j_p4_twenty_one_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p4_twenty_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_terminal. pa_h_hj32_local_total_j_p4_twenty_one_product_terminal + S (hj32_local_value_j_p4_twenty_one) = S ((S (21)) * pa_v_hj32_local_total_j_p4_twenty_one_product)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_terminal. pa_u_hj32_local_total_j_p4_twenty_one_product = pa_q_hj32_local_total_j_p4_twenty_one_product_terminal * S ((S (21)) * pa_v_hj32_local_total_j_p4_twenty_one_product) + (hj32_local_value_j_p4_twenty_one))) /\ forall pa_i_hj32_local_total_j_p4_twenty_one_product. (exists pa_lt_hj32_local_total_j_p4_twenty_one_product_bound. pa_lt_hj32_local_total_j_p4_twenty_one_product_bound + S pa_i_hj32_local_total_j_p4_twenty_one_product = 21) -> exists pa_p_hj32_local_total_j_p4_twenty_one_product pa_r_hj32_local_total_j_p4_twenty_one_product pa_s_hj32_local_total_j_p4_twenty_one_product. ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_factor. pa_h_hj32_local_total_j_p4_twenty_one_product_factor + S (pa_p_hj32_local_total_j_p4_twenty_one_product) = S ((S (pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_c_hj32_local_total_j_p4_twenty_one)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_factor. pa_b_hj32_local_total_j_p4_twenty_one = pa_q_hj32_local_total_j_p4_twenty_one_product_factor * S ((S (pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_c_hj32_local_total_j_p4_twenty_one) + (pa_p_hj32_local_total_j_p4_twenty_one_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_partial. pa_h_hj32_local_total_j_p4_twenty_one_product_partial + S (pa_r_hj32_local_total_j_p4_twenty_one_product) = S ((S (pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_v_hj32_local_total_j_p4_twenty_one_product)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_partial. pa_u_hj32_local_total_j_p4_twenty_one_product = pa_q_hj32_local_total_j_p4_twenty_one_product_partial * S ((S (pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_v_hj32_local_total_j_p4_twenty_one_product) + (pa_r_hj32_local_total_j_p4_twenty_one_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_successor. pa_h_hj32_local_total_j_p4_twenty_one_product_successor + S (pa_s_hj32_local_total_j_p4_twenty_one_product) = S ((S (S pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_v_hj32_local_total_j_p4_twenty_one_product)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_successor. pa_u_hj32_local_total_j_p4_twenty_one_product = pa_q_hj32_local_total_j_p4_twenty_one_product_successor * S ((S (S pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_v_hj32_local_total_j_p4_twenty_one_product) + (pa_s_hj32_local_total_j_p4_twenty_one_product))) /\ pa_s_hj32_local_total_j_p4_twenty_one_product = pa_r_hj32_local_total_j_p4_twenty_one_product * pa_p_hj32_local_total_j_p4_twenty_one_product)))))))) - 0015
specialize htotal 4 - 0016
specialize htotal 21 - 0017
exact htotal - 0018
cases j_p4_twenty_one - 0019
have j_parity : 7 * 6 = 2 * 21 - 0020
norm_num - 0021
have j_eleven_bound : Le(x,x1)Exact native replay line
have j_eleven_bound : exists bqb_le_gap_hj32_j_eleven_bound. bqb_le_gap_hj32_j_eleven_bound + (x) = (x1) - 0022
specialize pow_eleven_double_block_le_pow_four_even_from_total 6 - 0023
specialize pow_eleven_double_block_le_pow_four_even_from_total 21 - 0024
specialize pow_eleven_double_block_le_pow_four_even_from_total x - 0025
specialize pow_eleven_double_block_le_pow_four_even_from_total x1 - 0026
apply pow_eleven_double_block_le_pow_four_even_from_total - 0027
exact htotal - 0028
exact j_parity - 0029
exact j_p11_block_witness - 0030
exact j_p4_twenty_one_witness - 0031
have j_twelve : 2 * 6 = 12 - 0032
norm_num - 0033
have j_h_block : Pow(s + 7,2 · 6,j)Exact native replay line
have j_h_block : exists pa_b_hj32_j_h_block pa_c_hj32_j_h_block. ((forall pa_i_hj32_j_h_block_repeat. (exists pa_lt_hj32_j_h_block_repeat_bound. pa_lt_hj32_j_h_block_repeat_bound + S pa_i_hj32_j_h_block_repeat = 2 * 6) -> (((exists pa_h_hj32_j_h_block_repeat_decoded. pa_h_hj32_j_h_block_repeat_decoded + S (s + 7) = S ((S (pa_i_hj32_j_h_block_repeat)) * pa_c_hj32_j_h_block)) /\ exists pa_q_hj32_j_h_block_repeat_decoded. pa_b_hj32_j_h_block = pa_q_hj32_j_h_block_repeat_decoded * S ((S (pa_i_hj32_j_h_block_repeat)) * pa_c_hj32_j_h_block) + (s + 7)))) /\ (exists pa_u_hj32_j_h_block_product pa_v_hj32_j_h_block_product. ((((exists pa_h_hj32_j_h_block_product_start. pa_h_hj32_j_h_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_j_h_block_product)) /\ exists pa_q_hj32_j_h_block_product_start. pa_u_hj32_j_h_block_product = pa_q_hj32_j_h_block_product_start * S ((S (0)) * pa_v_hj32_j_h_block_product) + (1))) /\ ((((exists pa_h_hj32_j_h_block_product_terminal. pa_h_hj32_j_h_block_product_terminal + S (j) = S ((S (2 * 6)) * pa_v_hj32_j_h_block_product)) /\ exists pa_q_hj32_j_h_block_product_terminal. pa_u_hj32_j_h_block_product = pa_q_hj32_j_h_block_product_terminal * S ((S (2 * 6)) * pa_v_hj32_j_h_block_product) + (j))) /\ forall pa_i_hj32_j_h_block_product. (exists pa_lt_hj32_j_h_block_product_bound. pa_lt_hj32_j_h_block_product_bound + S pa_i_hj32_j_h_block_product = 2 * 6) -> exists pa_p_hj32_j_h_block_product pa_r_hj32_j_h_block_product pa_s_hj32_j_h_block_product. ((((exists pa_h_hj32_j_h_block_product_factor. pa_h_hj32_j_h_block_product_factor + S (pa_p_hj32_j_h_block_product) = S ((S (pa_i_hj32_j_h_block_product)) * pa_c_hj32_j_h_block)) /\ exists pa_q_hj32_j_h_block_product_factor. pa_b_hj32_j_h_block = pa_q_hj32_j_h_block_product_factor * S ((S (pa_i_hj32_j_h_block_product)) * pa_c_hj32_j_h_block) + (pa_p_hj32_j_h_block_product))) /\ ((((exists pa_h_hj32_j_h_block_product_partial. pa_h_hj32_j_h_block_product_partial + S (pa_r_hj32_j_h_block_product) = S ((S (pa_i_hj32_j_h_block_product)) * pa_v_hj32_j_h_block_product)) /\ exists pa_q_hj32_j_h_block_product_partial. pa_u_hj32_j_h_block_product = pa_q_hj32_j_h_block_product_partial * S ((S (pa_i_hj32_j_h_block_product)) * pa_v_hj32_j_h_block_product) + (pa_r_hj32_j_h_block_product))) /\ ((((exists pa_h_hj32_j_h_block_product_successor. pa_h_hj32_j_h_block_product_successor + S (pa_s_hj32_j_h_block_product) = S ((S (S pa_i_hj32_j_h_block_product)) * pa_v_hj32_j_h_block_product)) /\ exists pa_q_hj32_j_h_block_product_successor. pa_u_hj32_j_h_block_product = pa_q_hj32_j_h_block_product_successor * S ((S (S pa_i_hj32_j_h_block_product)) * pa_v_hj32_j_h_block_product) + (pa_s_hj32_j_h_block_product))) /\ pa_s_hj32_j_h_block_product = pa_r_hj32_j_h_block_product * pa_p_hj32_j_h_block_product))))))) - 0034
rewrite j_twelve - 0035
rewrite j_twelve - 0036
rewrite j_twelve - 0037
rewrite j_twelve - 0038
exact hj - 0039
have j_p4_block : ∃ hj32_local_value_j_p4_block. Pow(4,2 · 6,hj32_local_value_j_p4_block)Exact native replay line
have j_p4_block : exists hj32_local_value_j_p4_block. (exists pa_b_hj32_local_total_j_p4_block pa_c_hj32_local_total_j_p4_block. ((forall pa_i_hj32_local_total_j_p4_block_repeat. (exists pa_lt_hj32_local_total_j_p4_block_repeat_bound. pa_lt_hj32_local_total_j_p4_block_repeat_bound + S pa_i_hj32_local_total_j_p4_block_repeat = 2 * 6) -> (((exists pa_h_hj32_local_total_j_p4_block_repeat_decoded. pa_h_hj32_local_total_j_p4_block_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_j_p4_block_repeat)) * pa_c_hj32_local_total_j_p4_block)) /\ exists pa_q_hj32_local_total_j_p4_block_repeat_decoded. pa_b_hj32_local_total_j_p4_block = pa_q_hj32_local_total_j_p4_block_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p4_block_repeat)) * pa_c_hj32_local_total_j_p4_block) + (4)))) /\ (exists pa_u_hj32_local_total_j_p4_block_product pa_v_hj32_local_total_j_p4_block_product. ((((exists pa_h_hj32_local_total_j_p4_block_product_start. pa_h_hj32_local_total_j_p4_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p4_block_product)) /\ exists pa_q_hj32_local_total_j_p4_block_product_start. pa_u_hj32_local_total_j_p4_block_product = pa_q_hj32_local_total_j_p4_block_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p4_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p4_block_product_terminal. pa_h_hj32_local_total_j_p4_block_product_terminal + S (hj32_local_value_j_p4_block) = S ((S (2 * 6)) * pa_v_hj32_local_total_j_p4_block_product)) /\ exists pa_q_hj32_local_total_j_p4_block_product_terminal. pa_u_hj32_local_total_j_p4_block_product = pa_q_hj32_local_total_j_p4_block_product_terminal * S ((S (2 * 6)) * pa_v_hj32_local_total_j_p4_block_product) + (hj32_local_value_j_p4_block))) /\ forall pa_i_hj32_local_total_j_p4_block_product. (exists pa_lt_hj32_local_total_j_p4_block_product_bound. pa_lt_hj32_local_total_j_p4_block_product_bound + S pa_i_hj32_local_total_j_p4_block_product = 2 * 6) -> exists pa_p_hj32_local_total_j_p4_block_product pa_r_hj32_local_total_j_p4_block_product pa_s_hj32_local_total_j_p4_block_product. ((((exists pa_h_hj32_local_total_j_p4_block_product_factor. pa_h_hj32_local_total_j_p4_block_product_factor + S (pa_p_hj32_local_total_j_p4_block_product) = S ((S (pa_i_hj32_local_total_j_p4_block_product)) * pa_c_hj32_local_total_j_p4_block)) /\ exists pa_q_hj32_local_total_j_p4_block_product_factor. pa_b_hj32_local_total_j_p4_block = pa_q_hj32_local_total_j_p4_block_product_factor * S ((S (pa_i_hj32_local_total_j_p4_block_product)) * pa_c_hj32_local_total_j_p4_block) + (pa_p_hj32_local_total_j_p4_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_block_product_partial. pa_h_hj32_local_total_j_p4_block_product_partial + S (pa_r_hj32_local_total_j_p4_block_product) = S ((S (pa_i_hj32_local_total_j_p4_block_product)) * pa_v_hj32_local_total_j_p4_block_product)) /\ exists pa_q_hj32_local_total_j_p4_block_product_partial. pa_u_hj32_local_total_j_p4_block_product = pa_q_hj32_local_total_j_p4_block_product_partial * S ((S (pa_i_hj32_local_total_j_p4_block_product)) * pa_v_hj32_local_total_j_p4_block_product) + (pa_r_hj32_local_total_j_p4_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_block_product_successor. pa_h_hj32_local_total_j_p4_block_product_successor + S (pa_s_hj32_local_total_j_p4_block_product) = S ((S (S pa_i_hj32_local_total_j_p4_block_product)) * pa_v_hj32_local_total_j_p4_block_product)) /\ exists pa_q_hj32_local_total_j_p4_block_product_successor. pa_u_hj32_local_total_j_p4_block_product = pa_q_hj32_local_total_j_p4_block_product_successor * S ((S (S pa_i_hj32_local_total_j_p4_block_product)) * pa_v_hj32_local_total_j_p4_block_product) + (pa_s_hj32_local_total_j_p4_block_product))) /\ pa_s_hj32_local_total_j_p4_block_product = pa_r_hj32_local_total_j_p4_block_product * pa_p_hj32_local_total_j_p4_block_product)))))))) - 0040
specialize htotal 4 - 0041
specialize htotal 2 * 6 - 0042
exact htotal - 0043
cases j_p4_block - 0044
have j_p44_block : ∃ hj32_local_value_j_p44_block. Pow(44,2 · 6,hj32_local_value_j_p44_block)Exact native replay line
have j_p44_block : exists hj32_local_value_j_p44_block. (exists pa_b_hj32_local_total_j_p44_block pa_c_hj32_local_total_j_p44_block. ((forall pa_i_hj32_local_total_j_p44_block_repeat. (exists pa_lt_hj32_local_total_j_p44_block_repeat_bound. pa_lt_hj32_local_total_j_p44_block_repeat_bound + S pa_i_hj32_local_total_j_p44_block_repeat = 2 * 6) -> (((exists pa_h_hj32_local_total_j_p44_block_repeat_decoded. pa_h_hj32_local_total_j_p44_block_repeat_decoded + S (44) = S ((S (pa_i_hj32_local_total_j_p44_block_repeat)) * pa_c_hj32_local_total_j_p44_block)) /\ exists pa_q_hj32_local_total_j_p44_block_repeat_decoded. pa_b_hj32_local_total_j_p44_block = pa_q_hj32_local_total_j_p44_block_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p44_block_repeat)) * pa_c_hj32_local_total_j_p44_block) + (44)))) /\ (exists pa_u_hj32_local_total_j_p44_block_product pa_v_hj32_local_total_j_p44_block_product. ((((exists pa_h_hj32_local_total_j_p44_block_product_start. pa_h_hj32_local_total_j_p44_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p44_block_product)) /\ exists pa_q_hj32_local_total_j_p44_block_product_start. pa_u_hj32_local_total_j_p44_block_product = pa_q_hj32_local_total_j_p44_block_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p44_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p44_block_product_terminal. pa_h_hj32_local_total_j_p44_block_product_terminal + S (hj32_local_value_j_p44_block) = S ((S (2 * 6)) * pa_v_hj32_local_total_j_p44_block_product)) /\ exists pa_q_hj32_local_total_j_p44_block_product_terminal. pa_u_hj32_local_total_j_p44_block_product = pa_q_hj32_local_total_j_p44_block_product_terminal * S ((S (2 * 6)) * pa_v_hj32_local_total_j_p44_block_product) + (hj32_local_value_j_p44_block))) /\ forall pa_i_hj32_local_total_j_p44_block_product. (exists pa_lt_hj32_local_total_j_p44_block_product_bound. pa_lt_hj32_local_total_j_p44_block_product_bound + S pa_i_hj32_local_total_j_p44_block_product = 2 * 6) -> exists pa_p_hj32_local_total_j_p44_block_product pa_r_hj32_local_total_j_p44_block_product pa_s_hj32_local_total_j_p44_block_product. ((((exists pa_h_hj32_local_total_j_p44_block_product_factor. pa_h_hj32_local_total_j_p44_block_product_factor + S (pa_p_hj32_local_total_j_p44_block_product) = S ((S (pa_i_hj32_local_total_j_p44_block_product)) * pa_c_hj32_local_total_j_p44_block)) /\ exists pa_q_hj32_local_total_j_p44_block_product_factor. pa_b_hj32_local_total_j_p44_block = pa_q_hj32_local_total_j_p44_block_product_factor * S ((S (pa_i_hj32_local_total_j_p44_block_product)) * pa_c_hj32_local_total_j_p44_block) + (pa_p_hj32_local_total_j_p44_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p44_block_product_partial. pa_h_hj32_local_total_j_p44_block_product_partial + S (pa_r_hj32_local_total_j_p44_block_product) = S ((S (pa_i_hj32_local_total_j_p44_block_product)) * pa_v_hj32_local_total_j_p44_block_product)) /\ exists pa_q_hj32_local_total_j_p44_block_product_partial. pa_u_hj32_local_total_j_p44_block_product = pa_q_hj32_local_total_j_p44_block_product_partial * S ((S (pa_i_hj32_local_total_j_p44_block_product)) * pa_v_hj32_local_total_j_p44_block_product) + (pa_r_hj32_local_total_j_p44_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p44_block_product_successor. pa_h_hj32_local_total_j_p44_block_product_successor + S (pa_s_hj32_local_total_j_p44_block_product) = S ((S (S pa_i_hj32_local_total_j_p44_block_product)) * pa_v_hj32_local_total_j_p44_block_product)) /\ exists pa_q_hj32_local_total_j_p44_block_product_successor. pa_u_hj32_local_total_j_p44_block_product = pa_q_hj32_local_total_j_p44_block_product_successor * S ((S (S pa_i_hj32_local_total_j_p44_block_product)) * pa_v_hj32_local_total_j_p44_block_product) + (pa_s_hj32_local_total_j_p44_block_product))) /\ pa_s_hj32_local_total_j_p44_block_product = pa_r_hj32_local_total_j_p44_block_product * pa_p_hj32_local_total_j_p44_block_product)))))))) - 0045
specialize htotal 44 - 0046
specialize htotal 2 * 6 - 0047
exact htotal - 0048
cases j_p44_block - 0049
have j_p4_thirty_three : ∃ hj32_local_value_j_p4_thirty_three. Pow(4,33,hj32_local_value_j_p4_thirty_three)Exact native replay line
have j_p4_thirty_three : exists hj32_local_value_j_p4_thirty_three. (exists pa_b_hj32_local_total_j_p4_thirty_three pa_c_hj32_local_total_j_p4_thirty_three. ((forall pa_i_hj32_local_total_j_p4_thirty_three_repeat. (exists pa_lt_hj32_local_total_j_p4_thirty_three_repeat_bound. pa_lt_hj32_local_total_j_p4_thirty_three_repeat_bound + S pa_i_hj32_local_total_j_p4_thirty_three_repeat = 33) -> (((exists pa_h_hj32_local_total_j_p4_thirty_three_repeat_decoded. pa_h_hj32_local_total_j_p4_thirty_three_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_j_p4_thirty_three_repeat)) * pa_c_hj32_local_total_j_p4_thirty_three)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_repeat_decoded. pa_b_hj32_local_total_j_p4_thirty_three = pa_q_hj32_local_total_j_p4_thirty_three_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p4_thirty_three_repeat)) * pa_c_hj32_local_total_j_p4_thirty_three) + (4)))) /\ (exists pa_u_hj32_local_total_j_p4_thirty_three_product pa_v_hj32_local_total_j_p4_thirty_three_product. ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_start. pa_h_hj32_local_total_j_p4_thirty_three_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p4_thirty_three_product)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_start. pa_u_hj32_local_total_j_p4_thirty_three_product = pa_q_hj32_local_total_j_p4_thirty_three_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p4_thirty_three_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_terminal. pa_h_hj32_local_total_j_p4_thirty_three_product_terminal + S (hj32_local_value_j_p4_thirty_three) = S ((S (33)) * pa_v_hj32_local_total_j_p4_thirty_three_product)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_terminal. pa_u_hj32_local_total_j_p4_thirty_three_product = pa_q_hj32_local_total_j_p4_thirty_three_product_terminal * S ((S (33)) * pa_v_hj32_local_total_j_p4_thirty_three_product) + (hj32_local_value_j_p4_thirty_three))) /\ forall pa_i_hj32_local_total_j_p4_thirty_three_product. (exists pa_lt_hj32_local_total_j_p4_thirty_three_product_bound. pa_lt_hj32_local_total_j_p4_thirty_three_product_bound + S pa_i_hj32_local_total_j_p4_thirty_three_product = 33) -> exists pa_p_hj32_local_total_j_p4_thirty_three_product pa_r_hj32_local_total_j_p4_thirty_three_product pa_s_hj32_local_total_j_p4_thirty_three_product. ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_factor. pa_h_hj32_local_total_j_p4_thirty_three_product_factor + S (pa_p_hj32_local_total_j_p4_thirty_three_product) = S ((S (pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_c_hj32_local_total_j_p4_thirty_three)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_factor. pa_b_hj32_local_total_j_p4_thirty_three = pa_q_hj32_local_total_j_p4_thirty_three_product_factor * S ((S (pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_c_hj32_local_total_j_p4_thirty_three) + (pa_p_hj32_local_total_j_p4_thirty_three_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_partial. pa_h_hj32_local_total_j_p4_thirty_three_product_partial + S (pa_r_hj32_local_total_j_p4_thirty_three_product) = S ((S (pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_v_hj32_local_total_j_p4_thirty_three_product)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_partial. pa_u_hj32_local_total_j_p4_thirty_three_product = pa_q_hj32_local_total_j_p4_thirty_three_product_partial * S ((S (pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_v_hj32_local_total_j_p4_thirty_three_product) + (pa_r_hj32_local_total_j_p4_thirty_three_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_successor. pa_h_hj32_local_total_j_p4_thirty_three_product_successor + S (pa_s_hj32_local_total_j_p4_thirty_three_product) = S ((S (S pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_v_hj32_local_total_j_p4_thirty_three_product)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_successor. pa_u_hj32_local_total_j_p4_thirty_three_product = pa_q_hj32_local_total_j_p4_thirty_three_product_successor * S ((S (S pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_v_hj32_local_total_j_p4_thirty_three_product) + (pa_s_hj32_local_total_j_p4_thirty_three_product))) /\ pa_s_hj32_local_total_j_p4_thirty_three_product = pa_r_hj32_local_total_j_p4_thirty_three_product * pa_p_hj32_local_total_j_p4_thirty_three_product)))))))) - 0050
specialize htotal 4 - 0051
specialize htotal 33 - 0052
exact htotal - 0053
cases j_p4_thirty_three - 0054
have j_product_44_graph : Pow(4 · 11,2 · 6,x3)Exact native replay line
have j_product_44_graph : exists pa_b_hj32_local_product_j_product_44 pa_c_hj32_local_product_j_product_44. ((forall pa_i_hj32_local_product_j_product_44_repeat. (exists pa_lt_hj32_local_product_j_product_44_repeat_bound. pa_lt_hj32_local_product_j_product_44_repeat_bound + S pa_i_hj32_local_product_j_product_44_repeat = 2 * 6) -> (((exists pa_h_hj32_local_product_j_product_44_repeat_decoded. pa_h_hj32_local_product_j_product_44_repeat_decoded + S (4 * 11) = S ((S (pa_i_hj32_local_product_j_product_44_repeat)) * pa_c_hj32_local_product_j_product_44)) /\ exists pa_q_hj32_local_product_j_product_44_repeat_decoded. pa_b_hj32_local_product_j_product_44 = pa_q_hj32_local_product_j_product_44_repeat_decoded * S ((S (pa_i_hj32_local_product_j_product_44_repeat)) * pa_c_hj32_local_product_j_product_44) + (4 * 11)))) /\ (exists pa_u_hj32_local_product_j_product_44_product pa_v_hj32_local_product_j_product_44_product. ((((exists pa_h_hj32_local_product_j_product_44_product_start. pa_h_hj32_local_product_j_product_44_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_j_product_44_product)) /\ exists pa_q_hj32_local_product_j_product_44_product_start. pa_u_hj32_local_product_j_product_44_product = pa_q_hj32_local_product_j_product_44_product_start * S ((S (0)) * pa_v_hj32_local_product_j_product_44_product) + (1))) /\ ((((exists pa_h_hj32_local_product_j_product_44_product_terminal. pa_h_hj32_local_product_j_product_44_product_terminal + S (x3) = S ((S (2 * 6)) * pa_v_hj32_local_product_j_product_44_product)) /\ exists pa_q_hj32_local_product_j_product_44_product_terminal. pa_u_hj32_local_product_j_product_44_product = pa_q_hj32_local_product_j_product_44_product_terminal * S ((S (2 * 6)) * pa_v_hj32_local_product_j_product_44_product) + (x3))) /\ forall pa_i_hj32_local_product_j_product_44_product. (exists pa_lt_hj32_local_product_j_product_44_product_bound. pa_lt_hj32_local_product_j_product_44_product_bound + S pa_i_hj32_local_product_j_product_44_product = 2 * 6) -> exists pa_p_hj32_local_product_j_product_44_product pa_r_hj32_local_product_j_product_44_product pa_s_hj32_local_product_j_product_44_product. ((((exists pa_h_hj32_local_product_j_product_44_product_factor. pa_h_hj32_local_product_j_product_44_product_factor + S (pa_p_hj32_local_product_j_product_44_product) = S ((S (pa_i_hj32_local_product_j_product_44_product)) * pa_c_hj32_local_product_j_product_44)) /\ exists pa_q_hj32_local_product_j_product_44_product_factor. pa_b_hj32_local_product_j_product_44 = pa_q_hj32_local_product_j_product_44_product_factor * S ((S (pa_i_hj32_local_product_j_product_44_product)) * pa_c_hj32_local_product_j_product_44) + (pa_p_hj32_local_product_j_product_44_product))) /\ ((((exists pa_h_hj32_local_product_j_product_44_product_partial. pa_h_hj32_local_product_j_product_44_product_partial + S (pa_r_hj32_local_product_j_product_44_product) = S ((S (pa_i_hj32_local_product_j_product_44_product)) * pa_v_hj32_local_product_j_product_44_product)) /\ exists pa_q_hj32_local_product_j_product_44_product_partial. pa_u_hj32_local_product_j_product_44_product = pa_q_hj32_local_product_j_product_44_product_partial * S ((S (pa_i_hj32_local_product_j_product_44_product)) * pa_v_hj32_local_product_j_product_44_product) + (pa_r_hj32_local_product_j_product_44_product))) /\ ((((exists pa_h_hj32_local_product_j_product_44_product_successor. pa_h_hj32_local_product_j_product_44_product_successor + S (pa_s_hj32_local_product_j_product_44_product) = S ((S (S pa_i_hj32_local_product_j_product_44_product)) * pa_v_hj32_local_product_j_product_44_product)) /\ exists pa_q_hj32_local_product_j_product_44_product_successor. pa_u_hj32_local_product_j_product_44_product = pa_q_hj32_local_product_j_product_44_product_successor * S ((S (S pa_i_hj32_local_product_j_product_44_product)) * pa_v_hj32_local_product_j_product_44_product) + (pa_s_hj32_local_product_j_product_44_product))) /\ pa_s_hj32_local_product_j_product_44_product = pa_r_hj32_local_product_j_product_44_product * pa_p_hj32_local_product_j_product_44_product))))))) - 0055
have j_product_44_base : 4 * 11 = 44 - 0056
norm_num - 0057
rewrite j_product_44_base - 0058
rewrite j_product_44_base - 0059
exact j_p44_block_witness - 0060
have j_product_44 : x3 = x2 * x - 0061
specialize pow_mul_base 4 - 0062
specialize pow_mul_base 11 - 0063
specialize pow_mul_base 2 * 6 - 0064
specialize pow_mul_base x2 - 0065
specialize pow_mul_base x - 0066
specialize pow_mul_base x3 - 0067
apply pow_mul_base - 0068
exact j_p4_block_witness - 0069
exact j_p11_block_witness - 0070
exact j_product_44_graph - 0071
have j_product_33 : x4 = x2 * x1 - 0072
specialize pow_add 4 - 0073
specialize pow_add 2 * 6 - 0074
specialize pow_add 21 - 0075
specialize pow_add 33 - 0076
specialize pow_add x2 - 0077
specialize pow_add x1 - 0078
specialize pow_add x4 - 0079
apply pow_add - 0080
norm_num - 0081
exact j_p4_block_witness - 0082
exact j_p4_twenty_one_witness - 0083
exact j_p4_thirty_three_witness - 0084
have j_four_refl : Le(x2,x2)Exact native replay line
have j_four_refl : exists bqb_le_gap_hj32_j_four_refl. bqb_le_gap_hj32_j_four_refl + (x2) = (x2) - 0085
specialize le_refl x2 - 0086
exact le_refl - 0087
have j_product_bound : Le(x2 · x,x2 · x1)Exact native replay line
have j_product_bound : exists bqb_le_gap_hj32_local_product_bound_j_product_bound. bqb_le_gap_hj32_local_product_bound_j_product_bound + (x2 * x) = (x2 * x1) - 0088
specialize mul_le_mul x2 - 0089
specialize mul_le_mul x2 - 0090
specialize mul_le_mul x - 0091
specialize mul_le_mul x1 - 0092
apply mul_le_mul - 0093
exact j_four_refl - 0094
exact j_eleven_bound - 0095
rewrite <- j_product_44 at j_product_bound - 0096
rewrite <- j_product_33 at j_product_bound - 0097
have j_base_to_upper : Le(s + 7,37 + 7)Exact native replay line
have j_base_to_upper : exists bqb_le_gap_hj32_j_base_to_upper. bqb_le_gap_hj32_j_base_to_upper + (s + 7) = (37 + 7) - 0098
specialize add_le_add_right s - 0099
specialize add_le_add_right 37 - 0100
specialize add_le_add_right 7 - 0101
apply add_le_add_right - 0102
exact hupper - 0103
have j_upper_value : 37 + 7 = 44 - 0104
norm_num - 0105
have j_base_bound : Le(s + 7,44)Exact native replay line
have j_base_bound : exists bqb_le_gap_hj32_j_base_bound. bqb_le_gap_hj32_j_base_bound + (s + 7) = (44) - 0106
rewrite j_upper_value at j_base_to_upper - 0107
exact j_base_to_upper - 0108
have j_to_44 : Le(j,x3)Exact native replay line
have j_to_44 : exists bqb_le_gap_hj32_local_base_bound_j_to_44. bqb_le_gap_hj32_local_base_bound_j_to_44 + (j) = (x3) - 0109
specialize pow_base_monotone s + 7 - 0110
specialize pow_base_monotone 44 - 0111
specialize pow_base_monotone 2 * 6 - 0112
specialize pow_base_monotone j - 0113
specialize pow_base_monotone x3 - 0114
apply pow_base_monotone - 0115
exact j_base_bound - 0116
exact j_h_block - 0117
exact j_p44_block_witness - 0118
have j_to_thirty_three : Le(j,x4)Exact native replay line
have j_to_thirty_three : exists bqb_le_gap_hj32_local_trans_bound_j_to_thirty_three. bqb_le_gap_hj32_local_trans_bound_j_to_thirty_three + (j) = (x4) - 0119
specialize le_trans j - 0120
specialize le_trans x3 - 0121
specialize le_trans x4 - 0122
apply le_trans - 0123
exact j_to_44 - 0124
exact j_product_bound - 0125
have j_exponent_from_lower : Le(32 + 5,s + 5)Exact native replay line
have j_exponent_from_lower : exists bqb_le_gap_hj32_j_exponent_from_lower. bqb_le_gap_hj32_j_exponent_from_lower + (32 + 5) = (s + 5) - 0126
specialize add_le_add_right 32 - 0127
specialize add_le_add_right s - 0128
specialize add_le_add_right 5 - 0129
apply add_le_add_right - 0130
exact hlower - 0131
have j_lower_value : 32 + 5 = 37 - 0132
norm_num - 0133
have j_thirty_seven_to_target : Lt(36,s + 5)Exact native replay line
have j_thirty_seven_to_target : exists bqb_le_gap_hj32_j_thirty_seven_to_target. bqb_le_gap_hj32_j_thirty_seven_to_target + (37) = (s + 5) - 0134
rewrite j_lower_value at j_exponent_from_lower - 0135
exact j_exponent_from_lower - 0136
have j_seed : Lt(32,37)Exact native replay line
have j_seed : exists bqb_le_gap_hj32_j_exponent_seed. bqb_le_gap_hj32_j_exponent_seed + (33) = (37) - 0137
exists 4 - 0138
norm_num - 0139
have j_exponent_bound : Lt(32,s + 5)Exact native replay line
have j_exponent_bound : exists bqb_le_gap_hj32_local_trans_bound_j_exponent_bound. bqb_le_gap_hj32_local_trans_bound_j_exponent_bound + (33) = (s + 5) - 0140
specialize le_trans 33 - 0141
specialize le_trans 37 - 0142
specialize le_trans s + 5 - 0143
apply le_trans - 0144
exact j_seed - 0145
exact j_thirty_seven_to_target - 0146
have j_growth : Le(x4,g)Exact native replay line
have j_growth : exists bqb_le_gap_hj32_local_exponent_bound_j_growth. bqb_le_gap_hj32_local_exponent_bound_j_growth + (x4) = (g) - 0147
specialize pow_exponent_monotone_from_total 4 - 0148
specialize pow_exponent_monotone_from_total 33 - 0149
specialize pow_exponent_monotone_from_total s + 5 - 0150
specialize pow_exponent_monotone_from_total x4 - 0151
specialize pow_exponent_monotone_from_total g - 0152
apply pow_exponent_monotone_from_total - 0153
exact htotal - 0154
exists 3 - 0155
norm_num - 0156
exact j_exponent_bound - 0157
exact j_p4_thirty_three_witness - 0158
exact hg - 0159
have j_result : Le(j,g)Exact native replay line
have j_result : exists bqb_le_gap_hj32_local_trans_bound_j_result. bqb_le_gap_hj32_local_trans_bound_j_result + (j) = (g) - 0160
specialize le_trans j - 0161
specialize le_trans x4 - 0162
specialize le_trans g - 0163
apply le_trans - 0164
exact j_to_thirty_three - 0165
exact j_growth - 0166
exact j_result