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.
Exact expanded PA statement
forall sb sc fb fc r l e F R. (((exists ff_u_sign_product_count_sum ff_v_sign_product_count_sum. ((((exists ff_h_sign_product_count_sum_start. ff_h_sign_product_count_sum_start + S (0) = S ((S (0)) * ff_v_sign_product_count_sum)) /\ exists ff_q_sign_product_count_sum_start. ff_u_sign_product_count_sum = ff_q_sign_product_count_sum_start * S ((S (0)) * ff_v_sign_product_count_sum) + (0))) /\ ((((exists ff_h_sign_product_count_sum_terminal. ff_h_sign_product_count_sum_terminal + S (e) = S ((S (l)) * ff_v_sign_product_count_sum)) /\ exists ff_q_sign_product_count_sum_terminal. ff_u_sign_product_count_sum = ff_q_sign_product_count_sum_terminal * S ((S (l)) * ff_v_sign_product_count_sum) + (e))) /\ forall ff_i_sign_product_count_sum. (exists ff_lt_sign_product_count_sum_bound. ff_lt_sign_product_count_sum_bound + S ff_i_sign_product_count_sum = l) -> exists ff_a_sign_product_count_sum ff_r_sign_product_count_sum ff_s_sign_product_count_sum. ((((exists ff_h_sign_product_count_sum_summand. ff_h_sign_product_count_sum_summand + S (ff_a_sign_product_count_sum) = S ((S (ff_i_sign_product_count_sum)) * sc)) /\ exists ff_q_sign_product_count_sum_summand. sb = ff_q_sign_product_count_sum_summand * S ((S (ff_i_sign_product_count_sum)) * sc) + (ff_a_sign_product_count_sum))) /\ ((((exists ff_h_sign_product_count_sum_partial. ff_h_sign_product_count_sum_partial + S (ff_r_sign_product_count_sum) = S ((S (ff_i_sign_product_count_sum)) * ff_v_sign_product_count_sum)) /\ exists ff_q_sign_product_count_sum_partial. ff_u_sign_product_count_sum = ff_q_sign_product_count_sum_partial * S ((S (ff_i_sign_product_count_sum)) * ff_v_sign_product_count_sum) + (ff_r_sign_product_count_sum))) /\ ((((exists ff_h_sign_product_count_sum_successor. ff_h_sign_product_count_sum_successor + S (ff_s_sign_product_count_sum) = S ((S (S ff_i_sign_product_count_sum)) * ff_v_sign_product_count_sum)) /\ exists ff_q_sign_product_count_sum_successor. ff_u_sign_product_count_sum = ff_q_sign_product_count_sum_successor * S ((S (S ff_i_sign_product_count_sum)) * ff_v_sign_product_count_sum) + (ff_s_sign_product_count_sum))) /\ ff_s_sign_product_count_sum = ff_r_sign_product_count_sum + ff_a_sign_product_count_sum)))))) /\ (forall ff_i_sign_product_count_bits. (exists ff_lt_sign_product_count_bits_bound. ff_lt_sign_product_count_bits_bound + S ff_i_sign_product_count_bits = l) -> exists ff_bit_sign_product_count_bits. ((((exists ff_h_sign_product_count_bits_decoded. ff_h_sign_product_count_bits_decoded + S (ff_bit_sign_product_count_bits) = S ((S (ff_i_sign_product_count_bits)) * sc)) /\ exists ff_q_sign_product_count_bits_decoded. sb = ff_q_sign_product_count_bits_decoded * S ((S (ff_i_sign_product_count_bits)) * sc) + (ff_bit_sign_product_count_bits))) /\ (ff_bit_sign_product_count_bits = 0 \/ ff_bit_sign_product_count_bits = 1))))) -> (forall gspf_index_sign_product_signs gspf_bit_sign_product_signs. (exists gsp_lt_gap_sign_product_signs_bound. gsp_lt_gap_sign_product_signs_bound + S gspf_index_sign_product_signs = l) -> (((exists ff_h_gspf_sign_product_signs_bit. ff_h_gspf_sign_product_signs_bit + S (gspf_bit_sign_product_signs) = S ((S (gspf_index_sign_product_signs)) * sc)) /\ exists ff_q_gspf_sign_product_signs_bit. sb = ff_q_gspf_sign_product_signs_bit * S ((S (gspf_index_sign_product_signs)) * sc) + (gspf_bit_sign_product_signs))) -> (((gspf_bit_sign_product_signs = 0) /\ (((exists gsp_beta_height_gspf_sign_product_signs_one. gsp_beta_height_gspf_sign_product_signs_one + S (1) = S ((S (gspf_index_sign_product_signs)) * fc)) /\ exists gsp_beta_quotient_gspf_sign_product_signs_one. fb = gsp_beta_quotient_gspf_sign_product_signs_one * S ((S (gspf_index_sign_product_signs)) * fc) + (1)))) \/ ((gspf_bit_sign_product_signs = 1) /\ (((exists ff_h_gspf_sign_product_signs_predecessor. ff_h_gspf_sign_product_signs_predecessor + S (r) = S ((S (gspf_index_sign_product_signs)) * fc)) /\ exists ff_q_gspf_sign_product_signs_predecessor. fb = ff_q_gspf_sign_product_signs_predecessor * S ((S (gspf_index_sign_product_signs)) * fc) + (r)))))) -> (exists ff_u_sign_product_product ff_v_sign_product_product. ((((exists ff_h_sign_product_product_start. ff_h_sign_product_product_start + S (1) = S ((S (0)) * ff_v_sign_product_product)) /\ exists ff_q_sign_product_product_start. ff_u_sign_product_product = ff_q_sign_product_product_start * S ((S (0)) * ff_v_sign_product_product) + (1))) /\ ((((exists ff_h_sign_product_product_terminal. ff_h_sign_product_product_terminal + S (F) = S ((S (l)) * ff_v_sign_product_product)) /\ exists ff_q_sign_product_product_terminal. ff_u_sign_product_product = ff_q_sign_product_product_terminal * S ((S (l)) * ff_v_sign_product_product) + (F))) /\ forall ff_i_sign_product_product. (exists ff_lt_sign_product_product_bound. ff_lt_sign_product_product_bound + S ff_i_sign_product_product = l) -> exists ff_p_sign_product_product ff_r_sign_product_product ff_s_sign_product_product. ((((exists ff_h_sign_product_product_factor. ff_h_sign_product_product_factor + S (ff_p_sign_product_product) = S ((S (ff_i_sign_product_product)) * fc)) /\ exists ff_q_sign_product_product_factor. fb = ff_q_sign_product_product_factor * S ((S (ff_i_sign_product_product)) * fc) + (ff_p_sign_product_product))) /\ ((((exists ff_h_sign_product_product_partial. ff_h_sign_product_product_partial + S (ff_r_sign_product_product) = S ((S (ff_i_sign_product_product)) * ff_v_sign_product_product)) /\ exists ff_q_sign_product_product_partial. ff_u_sign_product_product = ff_q_sign_product_product_partial * S ((S (ff_i_sign_product_product)) * ff_v_sign_product_product) + (ff_r_sign_product_product))) /\ ((((exists ff_h_sign_product_product_successor. ff_h_sign_product_product_successor + S (ff_s_sign_product_product) = S ((S (S ff_i_sign_product_product)) * ff_v_sign_product_product)) /\ exists ff_q_sign_product_product_successor. ff_u_sign_product_product = ff_q_sign_product_product_successor * S ((S (S ff_i_sign_product_product)) * ff_v_sign_product_product) + (ff_s_sign_product_product))) /\ ff_s_sign_product_product = ff_r_sign_product_product * ff_p_sign_product_product)))))) -> (exists ff_b_sign_product_power ff_c_sign_product_power. ((forall ff_i_sign_product_power_repeat. (exists ff_lt_sign_product_power_repeat_bound. ff_lt_sign_product_power_repeat_bound + S ff_i_sign_product_power_repeat = e) -> (((exists ff_h_sign_product_power_repeat_decoded. ff_h_sign_product_power_repeat_decoded + S (r) = S ((S (ff_i_sign_product_power_repeat)) * ff_c_sign_product_power)) /\ exists ff_q_sign_product_power_repeat_decoded. ff_b_sign_product_power = ff_q_sign_product_power_repeat_decoded * S ((S (ff_i_sign_product_power_repeat)) * ff_c_sign_product_power) + (r)))) /\ (exists ff_u_sign_product_power_product ff_v_sign_product_power_product. ((((exists ff_h_sign_product_power_product_start. ff_h_sign_product_power_product_start + S (1) = S ((S (0)) * ff_v_sign_product_power_product)) /\ exists ff_q_sign_product_power_product_start. ff_u_sign_product_power_product = ff_q_sign_product_power_product_start * S ((S (0)) * ff_v_sign_product_power_product) + (1))) /\ ((((exists ff_h_sign_product_power_product_terminal. ff_h_sign_product_power_product_terminal + S (R) = S ((S (e)) * ff_v_sign_product_power_product)) /\ exists ff_q_sign_product_power_product_terminal. ff_u_sign_product_power_product = ff_q_sign_product_power_product_terminal * S ((S (e)) * ff_v_sign_product_power_product) + (R))) /\ forall ff_i_sign_product_power_product. (exists ff_lt_sign_product_power_product_bound. ff_lt_sign_product_power_product_bound + S ff_i_sign_product_power_product = e) -> exists ff_p_sign_product_power_product ff_r_sign_product_power_product ff_s_sign_product_power_product. ((((exists ff_h_sign_product_power_product_factor. ff_h_sign_product_power_product_factor + S (ff_p_sign_product_power_product) = S ((S (ff_i_sign_product_power_product)) * ff_c_sign_product_power)) /\ exists ff_q_sign_product_power_product_factor. ff_b_sign_product_power = ff_q_sign_product_power_product_factor * S ((S (ff_i_sign_product_power_product)) * ff_c_sign_product_power) + (ff_p_sign_product_power_product))) /\ ((((exists ff_h_sign_product_power_product_partial. ff_h_sign_product_power_product_partial + S (ff_r_sign_product_power_product) = S ((S (ff_i_sign_product_power_product)) * ff_v_sign_product_power_product)) /\ exists ff_q_sign_product_power_product_partial. ff_u_sign_product_power_product = ff_q_sign_product_power_product_partial * S ((S (ff_i_sign_product_power_product)) * ff_v_sign_product_power_product) + (ff_r_sign_product_power_product))) /\ ((((exists ff_h_sign_product_power_product_successor. ff_h_sign_product_power_product_successor + S (ff_s_sign_product_power_product) = S ((S (S ff_i_sign_product_power_product)) * ff_v_sign_product_power_product)) /\ exists ff_q_sign_product_power_product_successor. ff_u_sign_product_power_product = ff_q_sign_product_power_product_successor * S ((S (S ff_i_sign_product_power_product)) * ff_v_sign_product_power_product) + (ff_s_sign_product_power_product))) /\ ff_s_sign_product_power_product = ff_r_sign_product_power_product * ff_p_sign_product_power_product)))))))) -> F = RStructural proof guide
Generated structural guide
The product of 1/r sign factors is exactly r to the number of one bits.
Use the direct prerequisites bit_count_zero, bit_count_succ_decompose, beta_product_zero, beta_product_succ_decompose, pow_zero, pow_successor_decompose, beta_sign_factor_prefix_drop_last, beta_at_unique, le_refl, mul_one as previously established PA formulas.
The proof proceeds by structural induction (1), case analysis (14), intermediate claims (16), equality transport (11).
Referenced ingredients
Proof neighborhood
Direct dependencies
PA0048 bit_count_zero PA0042 bit_count_succ_decompose PA0049 beta_product_zero PA004A beta_product_succ_decompose PA004B pow_zero PA004D pow_successor_decompose PA007H beta_sign_factor_prefix_drop_last PA002F beta_at_unique PA001A le_refl PA0002 mul_oneDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.
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 (10)
01Fix variables and assumptionsL1–5
02Induction on lL6–13
03Establish he0L14–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bit count zero.
04Establish hF1L22–27
05Establish hR1L28–37
06Use earlier factsL38–38
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L38
exact hR1
07Fix variables and assumptionsL39–45
08Establish hcount_decompL46–54
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bit count succ decompose.
09Separate the logical casesL55–59
10Establish hproduct_decompL60–66
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.
11Separate the logical casesL67–70
12Establish hprefix_signsL71–79
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sign factor prefix drop last.
- L71
have hprefix_signs : ∀ gspf_index_sign_product_restricted_signs. ∀ gspf_bit_sign_product_restricted_signs. Lt(gspf_index_sign_product_restricted_signs,l) → BetaAt(sb,sc,gspf_index_sign_product_restricted_signs,gspf_bit_sign_product_restricted_signs) → gspf_bit_sign_product_restricted_signs = 0 ∧ BetaAt(fb,fc,gspf_index_sign_product_restricted_signs,1) ∨ gspf_bit_sign_product_restricted_signs = 1 ∧ BetaAt(fb,fc,gspf_index_sign_product_restricted_signs,r)Definitions: LtBetaAt - L72
specialize beta_sign_factor_prefix_drop_last sb - L73
specialize beta_sign_factor_prefix_drop_last sc - L74
specialize beta_sign_factor_prefix_drop_last fb - L75
specialize beta_sign_factor_prefix_drop_last fc - L76
specialize beta_sign_factor_prefix_drop_last r - L77
specialize beta_sign_factor_prefix_drop_last l - L78
apply beta_sign_factor_prefix_drop_last - L79
exact hsigns
13Establish hlast_caseL80–86
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hsigns.
- L80
have hlast_case : ((x = 0) /\ (((exists gsp_beta_height_sign_product_last_one. gsp_beta_height_sign_product_last_one + S (1) = S ((S (l)) * fc)) /\ exists gsp_beta_quotient_sign_product_last_one. fb = gsp_beta_quotient_sign_product_last_one * S ((S (l)) * fc) + (1)))) \/ ((x = 1) /\ (((exists ff_h_sign_product_last_predecessor. ff_h_sign_product_last_predecessor + S (r) = S ((S (l)) * fc)) /\ exists ff_q_sign_product_last_predecessor. fb = ff_q_sign_product_last_predecessor * S ((S (l)) * fc) + (r)))) - L81
specialize hsigns l - L82
specialize hsigns x - L83
apply hsigns - L84
specialize le_refl (S l) - L85
exact le_refl - L86
exact hcount_decomp_witness_witness_left
14Separate the logical casesL87–88
15Establish hfactor_oneL89–97
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
16Establish heqkL98–106
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA3.
17Establish hprefix_equalL107–116
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
18Calculate and transport equalitiesL117–117
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L117
rewrite hfactor_one
19Use earlier factsL118–118
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L118
specialize mul_one x3
20Calculate and transport equalitiesL119–119
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L119
rewrite mul_one
21Use earlier factsL120–120
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L120
exact hprefix_equal
22Separate the logical casesL121–121
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L121
cases hlast_case_right
23Establish hfactor_rL122–130
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
24Establish hsumL131–136
25Establish hsuccL137–141
26Establish heqsuccL142–145
27Establish hpower_decompL146–153
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor decompose.
28Separate the logical casesL154–155
29Establish hprefix_equalL156–165
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
- L156
have hprefix_equal : x3 = x4 - L157
specialize IH x1 - L158
specialize IH x3 - L159
specialize IH x4 - L160
apply IH - L161
exact hcount_decomp_witness_witness_right_left - L162
exact hprefix_signs - L163
exact hproduct_decomp_witness_witness_right_left - L164
exact hpower_decomp_witness_left - L165
rewrite hproduct_decomp_witness_witness_right_right
30Calculate and transport equalitiesL166–168
31Use earlier factsL169–169
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L169
exact hpower_decomp_witness_right
Original exact command ledger · 169 lines
- 0001
intro sb - 0002
intro sc - 0003
intro fb - 0004
intro fc - 0005
intro r - 0006
induction l - 0007
intro e - 0008
intro F - 0009
intro R - 0010
intro hcount - 0011
intro hsigns - 0012
intro hproduct - 0013
intro hpower - 0014
have he0 : e = 0 - 0015
specialize bit_count_zero sb - 0016
specialize bit_count_zero sc - 0017
specialize bit_count_zero 0 - 0018
specialize bit_count_zero e - 0019
apply bit_count_zero - 0020
refl - 0021
exact hcount - 0022
have hF1 : F = 1 - 0023
specialize beta_product_zero fb - 0024
specialize beta_product_zero fc - 0025
specialize beta_product_zero F - 0026
apply beta_product_zero - 0027
exact hproduct - 0028
have hR1 : R = 1 - 0029
specialize pow_zero r - 0030
specialize pow_zero e - 0031
specialize pow_zero R - 0032
apply pow_zero - 0033
exact he0 - 0034
exact hpower - 0035
trans 1 - 0036
exact hF1 - 0037
symm - 0038
exact hR1 - 0039
intro e - 0040
intro F - 0041
intro R - 0042
intro hcount - 0043
intro hsigns - 0044
intro hproduct - 0045
intro hpower - 0046
have hcount_decomp : exists a k. (((exists ff_h_sign_product_last_bit. ff_h_sign_product_last_bit + S (a) = S ((S (l)) * sc)) /\ exists ff_q_sign_product_last_bit. sb = ff_q_sign_product_last_bit * S ((S (l)) * sc) + (a))) /\ ((((exists ff_u_sign_product_prefix_count_sum ff_v_sign_product_prefix_count_sum. ((((exists ff_h_sign_product_prefix_count_sum_start. ff_h_sign_product_prefix_count_sum_start + S (0) = S ((S (0)) * ff_v_sign_product_prefix_count_sum)) /\ exists ff_q_sign_product_prefix_count_sum_start. ff_u_sign_product_prefix_count_sum = ff_q_sign_product_prefix_count_sum_start * S ((S (0)) * ff_v_sign_product_prefix_count_sum) + (0))) /\ ((((exists ff_h_sign_product_prefix_count_sum_terminal. ff_h_sign_product_prefix_count_sum_terminal + S (k) = S ((S (l)) * ff_v_sign_product_prefix_count_sum)) /\ exists ff_q_sign_product_prefix_count_sum_terminal. ff_u_sign_product_prefix_count_sum = ff_q_sign_product_prefix_count_sum_terminal * S ((S (l)) * ff_v_sign_product_prefix_count_sum) + (k))) /\ forall ff_i_sign_product_prefix_count_sum. (exists ff_lt_sign_product_prefix_count_sum_bound. ff_lt_sign_product_prefix_count_sum_bound + S ff_i_sign_product_prefix_count_sum = l) -> exists ff_a_sign_product_prefix_count_sum ff_r_sign_product_prefix_count_sum ff_s_sign_product_prefix_count_sum. ((((exists ff_h_sign_product_prefix_count_sum_summand. ff_h_sign_product_prefix_count_sum_summand + S (ff_a_sign_product_prefix_count_sum) = S ((S (ff_i_sign_product_prefix_count_sum)) * sc)) /\ exists ff_q_sign_product_prefix_count_sum_summand. sb = ff_q_sign_product_prefix_count_sum_summand * S ((S (ff_i_sign_product_prefix_count_sum)) * sc) + (ff_a_sign_product_prefix_count_sum))) /\ ((((exists ff_h_sign_product_prefix_count_sum_partial. ff_h_sign_product_prefix_count_sum_partial + S (ff_r_sign_product_prefix_count_sum) = S ((S (ff_i_sign_product_prefix_count_sum)) * ff_v_sign_product_prefix_count_sum)) /\ exists ff_q_sign_product_prefix_count_sum_partial. ff_u_sign_product_prefix_count_sum = ff_q_sign_product_prefix_count_sum_partial * S ((S (ff_i_sign_product_prefix_count_sum)) * ff_v_sign_product_prefix_count_sum) + (ff_r_sign_product_prefix_count_sum))) /\ ((((exists ff_h_sign_product_prefix_count_sum_successor. ff_h_sign_product_prefix_count_sum_successor + S (ff_s_sign_product_prefix_count_sum) = S ((S (S ff_i_sign_product_prefix_count_sum)) * ff_v_sign_product_prefix_count_sum)) /\ exists ff_q_sign_product_prefix_count_sum_successor. ff_u_sign_product_prefix_count_sum = ff_q_sign_product_prefix_count_sum_successor * S ((S (S ff_i_sign_product_prefix_count_sum)) * ff_v_sign_product_prefix_count_sum) + (ff_s_sign_product_prefix_count_sum))) /\ ff_s_sign_product_prefix_count_sum = ff_r_sign_product_prefix_count_sum + ff_a_sign_product_prefix_count_sum)))))) /\ (forall ff_i_sign_product_prefix_count_bits. (exists ff_lt_sign_product_prefix_count_bits_bound. ff_lt_sign_product_prefix_count_bits_bound + S ff_i_sign_product_prefix_count_bits = l) -> exists ff_bit_sign_product_prefix_count_bits. ((((exists ff_h_sign_product_prefix_count_bits_decoded. ff_h_sign_product_prefix_count_bits_decoded + S (ff_bit_sign_product_prefix_count_bits) = S ((S (ff_i_sign_product_prefix_count_bits)) * sc)) /\ exists ff_q_sign_product_prefix_count_bits_decoded. sb = ff_q_sign_product_prefix_count_bits_decoded * S ((S (ff_i_sign_product_prefix_count_bits)) * sc) + (ff_bit_sign_product_prefix_count_bits))) /\ (ff_bit_sign_product_prefix_count_bits = 0 \/ ff_bit_sign_product_prefix_count_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ e = k + a)) - 0047
specialize bit_count_succ_decompose sb - 0048
specialize bit_count_succ_decompose sc - 0049
specialize bit_count_succ_decompose l - 0050
specialize bit_count_succ_decompose (S l) - 0051
specialize bit_count_succ_decompose e - 0052
apply bit_count_succ_decompose - 0053
refl - 0054
exact hcount - 0055
cases hcount_decomp - 0056
cases hcount_decomp_witness - 0057
cases hcount_decomp_witness_witness - 0058
cases hcount_decomp_witness_witness_right - 0059
cases hcount_decomp_witness_witness_right_right - 0060
have hproduct_decomp : exists f G. (((exists ff_h_sign_product_last_factor. ff_h_sign_product_last_factor + S (f) = S ((S (l)) * fc)) /\ exists ff_q_sign_product_last_factor. fb = ff_q_sign_product_last_factor * S ((S (l)) * fc) + (f))) /\ ((exists ff_u_sign_product_prefix_product ff_v_sign_product_prefix_product. ((((exists ff_h_sign_product_prefix_product_start. ff_h_sign_product_prefix_product_start + S (1) = S ((S (0)) * ff_v_sign_product_prefix_product)) /\ exists ff_q_sign_product_prefix_product_start. ff_u_sign_product_prefix_product = ff_q_sign_product_prefix_product_start * S ((S (0)) * ff_v_sign_product_prefix_product) + (1))) /\ ((((exists ff_h_sign_product_prefix_product_terminal. ff_h_sign_product_prefix_product_terminal + S (G) = S ((S (l)) * ff_v_sign_product_prefix_product)) /\ exists ff_q_sign_product_prefix_product_terminal. ff_u_sign_product_prefix_product = ff_q_sign_product_prefix_product_terminal * S ((S (l)) * ff_v_sign_product_prefix_product) + (G))) /\ forall ff_i_sign_product_prefix_product. (exists ff_lt_sign_product_prefix_product_bound. ff_lt_sign_product_prefix_product_bound + S ff_i_sign_product_prefix_product = l) -> exists ff_p_sign_product_prefix_product ff_r_sign_product_prefix_product ff_s_sign_product_prefix_product. ((((exists ff_h_sign_product_prefix_product_factor. ff_h_sign_product_prefix_product_factor + S (ff_p_sign_product_prefix_product) = S ((S (ff_i_sign_product_prefix_product)) * fc)) /\ exists ff_q_sign_product_prefix_product_factor. fb = ff_q_sign_product_prefix_product_factor * S ((S (ff_i_sign_product_prefix_product)) * fc) + (ff_p_sign_product_prefix_product))) /\ ((((exists ff_h_sign_product_prefix_product_partial. ff_h_sign_product_prefix_product_partial + S (ff_r_sign_product_prefix_product) = S ((S (ff_i_sign_product_prefix_product)) * ff_v_sign_product_prefix_product)) /\ exists ff_q_sign_product_prefix_product_partial. ff_u_sign_product_prefix_product = ff_q_sign_product_prefix_product_partial * S ((S (ff_i_sign_product_prefix_product)) * ff_v_sign_product_prefix_product) + (ff_r_sign_product_prefix_product))) /\ ((((exists ff_h_sign_product_prefix_product_successor. ff_h_sign_product_prefix_product_successor + S (ff_s_sign_product_prefix_product) = S ((S (S ff_i_sign_product_prefix_product)) * ff_v_sign_product_prefix_product)) /\ exists ff_q_sign_product_prefix_product_successor. ff_u_sign_product_prefix_product = ff_q_sign_product_prefix_product_successor * S ((S (S ff_i_sign_product_prefix_product)) * ff_v_sign_product_prefix_product) + (ff_s_sign_product_prefix_product))) /\ ff_s_sign_product_prefix_product = ff_r_sign_product_prefix_product * ff_p_sign_product_prefix_product)))))) /\ F = G * f) - 0061
specialize beta_product_succ_decompose fb - 0062
specialize beta_product_succ_decompose fc - 0063
specialize beta_product_succ_decompose l - 0064
specialize beta_product_succ_decompose F - 0065
apply beta_product_succ_decompose - 0066
exact hproduct - 0067
cases hproduct_decomp - 0068
cases hproduct_decomp_witness - 0069
cases hproduct_decomp_witness_witness - 0070
cases hproduct_decomp_witness_witness_right - 0071
have hprefix_signs : forall gspf_index_sign_product_restricted_signs gspf_bit_sign_product_restricted_signs. (exists gsp_lt_gap_sign_product_restricted_signs_bound. gsp_lt_gap_sign_product_restricted_signs_bound + S gspf_index_sign_product_restricted_signs = l) -> (((exists ff_h_gspf_sign_product_restricted_signs_bit. ff_h_gspf_sign_product_restricted_signs_bit + S (gspf_bit_sign_product_restricted_signs) = S ((S (gspf_index_sign_product_restricted_signs)) * sc)) /\ exists ff_q_gspf_sign_product_restricted_signs_bit. sb = ff_q_gspf_sign_product_restricted_signs_bit * S ((S (gspf_index_sign_product_restricted_signs)) * sc) + (gspf_bit_sign_product_restricted_signs))) -> (((gspf_bit_sign_product_restricted_signs = 0) /\ (((exists gsp_beta_height_gspf_sign_product_restricted_signs_one. gsp_beta_height_gspf_sign_product_restricted_signs_one + S (1) = S ((S (gspf_index_sign_product_restricted_signs)) * fc)) /\ exists gsp_beta_quotient_gspf_sign_product_restricted_signs_one. fb = gsp_beta_quotient_gspf_sign_product_restricted_signs_one * S ((S (gspf_index_sign_product_restricted_signs)) * fc) + (1)))) \/ ((gspf_bit_sign_product_restricted_signs = 1) /\ (((exists ff_h_gspf_sign_product_restricted_signs_predecessor. ff_h_gspf_sign_product_restricted_signs_predecessor + S (r) = S ((S (gspf_index_sign_product_restricted_signs)) * fc)) /\ exists ff_q_gspf_sign_product_restricted_signs_predecessor. fb = ff_q_gspf_sign_product_restricted_signs_predecessor * S ((S (gspf_index_sign_product_restricted_signs)) * fc) + (r))))) - 0072
specialize beta_sign_factor_prefix_drop_last sb - 0073
specialize beta_sign_factor_prefix_drop_last sc - 0074
specialize beta_sign_factor_prefix_drop_last fb - 0075
specialize beta_sign_factor_prefix_drop_last fc - 0076
specialize beta_sign_factor_prefix_drop_last r - 0077
specialize beta_sign_factor_prefix_drop_last l - 0078
apply beta_sign_factor_prefix_drop_last - 0079
exact hsigns - 0080
have hlast_case : ((x = 0) /\ (((exists gsp_beta_height_sign_product_last_one. gsp_beta_height_sign_product_last_one + S (1) = S ((S (l)) * fc)) /\ exists gsp_beta_quotient_sign_product_last_one. fb = gsp_beta_quotient_sign_product_last_one * S ((S (l)) * fc) + (1)))) \/ ((x = 1) /\ (((exists ff_h_sign_product_last_predecessor. ff_h_sign_product_last_predecessor + S (r) = S ((S (l)) * fc)) /\ exists ff_q_sign_product_last_predecessor. fb = ff_q_sign_product_last_predecessor * S ((S (l)) * fc) + (r)))) - 0081
specialize hsigns l - 0082
specialize hsigns x - 0083
apply hsigns - 0084
specialize le_refl (S l) - 0085
exact le_refl - 0086
exact hcount_decomp_witness_witness_left - 0087
cases hlast_case - 0088
cases hlast_case_left - 0089
have hfactor_one : x2 = 1 - 0090
specialize beta_at_unique fb - 0091
specialize beta_at_unique fc - 0092
specialize beta_at_unique l - 0093
specialize beta_at_unique x2 - 0094
specialize beta_at_unique 1 - 0095
apply beta_at_unique - 0096
exact hproduct_decomp_witness_witness_left - 0097
exact hlast_case_left_right - 0098
have heqk : e = x1 - 0099
trans x1 + x - 0100
exact hcount_decomp_witness_witness_right_right_right - 0101
rewrite hlast_case_left_left - 0102
apply PA3 - 0103
rewrite heqk at hpower - 0104
rewrite heqk at hpower - 0105
rewrite heqk at hpower - 0106
rewrite heqk at hpower - 0107
have hprefix_equal : x3 = R - 0108
specialize IH x1 - 0109
specialize IH x3 - 0110
specialize IH R - 0111
apply IH - 0112
exact hcount_decomp_witness_witness_right_left - 0113
exact hprefix_signs - 0114
exact hproduct_decomp_witness_witness_right_left - 0115
exact hpower - 0116
rewrite hproduct_decomp_witness_witness_right_right - 0117
rewrite hfactor_one - 0118
specialize mul_one x3 - 0119
rewrite mul_one - 0120
exact hprefix_equal - 0121
cases hlast_case_right - 0122
have hfactor_r : x2 = r - 0123
specialize beta_at_unique fb - 0124
specialize beta_at_unique fc - 0125
specialize beta_at_unique l - 0126
specialize beta_at_unique x2 - 0127
specialize beta_at_unique r - 0128
apply beta_at_unique - 0129
exact hproduct_decomp_witness_witness_left - 0130
exact hlast_case_right_right - 0131
have hsum : e = x1 + 1 - 0132
trans x1 + x - 0133
exact hcount_decomp_witness_witness_right_right_right - 0134
congr - 0135
refl - 0136
exact hlast_case_right_left - 0137
have hsucc : x1 + 1 = S x1 - 0138
trans S (x1 + 0) - 0139
apply PA4 - 0140
congr - 0141
apply PA3 - 0142
have heqsucc : e = S x1 - 0143
trans x1 + 1 - 0144
exact hsum - 0145
exact hsucc - 0146
have hpower_decomp : exists W. (exists ff_b_sign_product_predecessor_power ff_c_sign_product_predecessor_power. ((forall ff_i_sign_product_predecessor_power_repeat. (exists ff_lt_sign_product_predecessor_power_repeat_bound. ff_lt_sign_product_predecessor_power_repeat_bound + S ff_i_sign_product_predecessor_power_repeat = x1) -> (((exists ff_h_sign_product_predecessor_power_repeat_decoded. ff_h_sign_product_predecessor_power_repeat_decoded + S (r) = S ((S (ff_i_sign_product_predecessor_power_repeat)) * ff_c_sign_product_predecessor_power)) /\ exists ff_q_sign_product_predecessor_power_repeat_decoded. ff_b_sign_product_predecessor_power = ff_q_sign_product_predecessor_power_repeat_decoded * S ((S (ff_i_sign_product_predecessor_power_repeat)) * ff_c_sign_product_predecessor_power) + (r)))) /\ (exists ff_u_sign_product_predecessor_power_product ff_v_sign_product_predecessor_power_product. ((((exists ff_h_sign_product_predecessor_power_product_start. ff_h_sign_product_predecessor_power_product_start + S (1) = S ((S (0)) * ff_v_sign_product_predecessor_power_product)) /\ exists ff_q_sign_product_predecessor_power_product_start. ff_u_sign_product_predecessor_power_product = ff_q_sign_product_predecessor_power_product_start * S ((S (0)) * ff_v_sign_product_predecessor_power_product) + (1))) /\ ((((exists ff_h_sign_product_predecessor_power_product_terminal. ff_h_sign_product_predecessor_power_product_terminal + S (W) = S ((S (x1)) * ff_v_sign_product_predecessor_power_product)) /\ exists ff_q_sign_product_predecessor_power_product_terminal. ff_u_sign_product_predecessor_power_product = ff_q_sign_product_predecessor_power_product_terminal * S ((S (x1)) * ff_v_sign_product_predecessor_power_product) + (W))) /\ forall ff_i_sign_product_predecessor_power_product. (exists ff_lt_sign_product_predecessor_power_product_bound. ff_lt_sign_product_predecessor_power_product_bound + S ff_i_sign_product_predecessor_power_product = x1) -> exists ff_p_sign_product_predecessor_power_product ff_r_sign_product_predecessor_power_product ff_s_sign_product_predecessor_power_product. ((((exists ff_h_sign_product_predecessor_power_product_factor. ff_h_sign_product_predecessor_power_product_factor + S (ff_p_sign_product_predecessor_power_product) = S ((S (ff_i_sign_product_predecessor_power_product)) * ff_c_sign_product_predecessor_power)) /\ exists ff_q_sign_product_predecessor_power_product_factor. ff_b_sign_product_predecessor_power = ff_q_sign_product_predecessor_power_product_factor * S ((S (ff_i_sign_product_predecessor_power_product)) * ff_c_sign_product_predecessor_power) + (ff_p_sign_product_predecessor_power_product))) /\ ((((exists ff_h_sign_product_predecessor_power_product_partial. ff_h_sign_product_predecessor_power_product_partial + S (ff_r_sign_product_predecessor_power_product) = S ((S (ff_i_sign_product_predecessor_power_product)) * ff_v_sign_product_predecessor_power_product)) /\ exists ff_q_sign_product_predecessor_power_product_partial. ff_u_sign_product_predecessor_power_product = ff_q_sign_product_predecessor_power_product_partial * S ((S (ff_i_sign_product_predecessor_power_product)) * ff_v_sign_product_predecessor_power_product) + (ff_r_sign_product_predecessor_power_product))) /\ ((((exists ff_h_sign_product_predecessor_power_product_successor. ff_h_sign_product_predecessor_power_product_successor + S (ff_s_sign_product_predecessor_power_product) = S ((S (S ff_i_sign_product_predecessor_power_product)) * ff_v_sign_product_predecessor_power_product)) /\ exists ff_q_sign_product_predecessor_power_product_successor. ff_u_sign_product_predecessor_power_product = ff_q_sign_product_predecessor_power_product_successor * S ((S (S ff_i_sign_product_predecessor_power_product)) * ff_v_sign_product_predecessor_power_product) + (ff_s_sign_product_predecessor_power_product))) /\ ff_s_sign_product_predecessor_power_product = ff_r_sign_product_predecessor_power_product * ff_p_sign_product_predecessor_power_product)))))))) /\ R = W * r - 0147
specialize pow_successor_decompose r - 0148
specialize pow_successor_decompose x1 - 0149
specialize pow_successor_decompose e - 0150
specialize pow_successor_decompose R - 0151
apply pow_successor_decompose - 0152
exact heqsucc - 0153
exact hpower - 0154
cases hpower_decomp - 0155
cases hpower_decomp_witness - 0156
have hprefix_equal : x3 = x4 - 0157
specialize IH x1 - 0158
specialize IH x3 - 0159
specialize IH x4 - 0160
apply IH - 0161
exact hcount_decomp_witness_witness_right_left - 0162
exact hprefix_signs - 0163
exact hproduct_decomp_witness_witness_right_left - 0164
exact hpower_decomp_witness_left - 0165
rewrite hproduct_decomp_witness_witness_right_right - 0166
rewrite hfactor_r - 0167
rewrite hprefix_equal - 0168
symm - 0169
exact hpower_decomp_witness_right