Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ F. ∀ G. ∀ n. ∀ L. ∀ M. ∀ z. ¬n = 0 → Le(n,L) → DirichletPrefix(F,G,n,L,M) → (SignedPrefixSum(M,S L,z) → DirichletSum(F,G,n,z)) ∧ (DirichletSum(F,G,n,z) → SignedPrefixSum(M,S L,z))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall F G n L M z. ~(n=0) -> (exists pvs_le_gap_padded_iff_bound. pvs_le_gap_padded_iff_bound + (n) = (L)) -> (((exists dst_positive_code_padded_iff_prefixtable dst_positive_scale_padded_iff_prefixtable dst_negative_code_padded_iff_prefixtable dst_negative_scale_padded_iff_prefixtable. (((M) = (((((dst_positive_code_padded_iff_prefixtable) + (dst_positive_scale_padded_iff_prefixtable)) * S ((dst_positive_code_padded_iff_prefixtable) + (dst_positive_scale_padded_iff_prefixtable)) + ((dst_positive_scale_padded_iff_prefixtable) + (dst_positive_scale_padded_iff_prefixtable))) + (((dst_negative_code_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)) * S ((dst_negative_code_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)) + ((dst_negative_scale_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)))) * S ((((dst_positive_code_padded_iff_prefixtable) + (dst_positive_scale_padded_iff_prefixtable)) * S ((dst_positive_code_padded_iff_prefixtable) + (dst_positive_scale_padded_iff_prefixtable)) + ((dst_positive_scale_padded_iff_prefixtable) + (dst_positive_scale_padded_iff_prefixtable))) + (((dst_negative_code_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)) * S ((dst_negative_code_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)) + ((dst_negative_scale_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)))) + ((((dst_negative_code_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)) * S ((dst_negative_code_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)) + ((dst_negative_scale_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable))) + (((dst_negative_code_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)) * S ((dst_negative_code_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)) + ((dst_negative_scale_padded_iff_prefixtable) + (dst_negative_scale_padded_iff_prefixtable)))))) /\ (forall dst_index_padded_iff_prefixtable. (exists pvs_le_gap_padded_iff_prefixtabledomain. pvs_le_gap_padded_iff_prefixtabledomain + (dst_index_padded_iff_prefixtable) = (L)) -> exists dst_positive_padded_iff_prefixtable dst_negative_padded_iff_prefixtable dst_value_padded_iff_prefixtable. ((((exists ff_h_pvs_padded_iff_prefixtableentrypositive. ff_h_pvs_padded_iff_prefixtableentrypositive + S (dst_positive_padded_iff_prefixtable) = S ((S (dst_index_padded_iff_prefixtable)) * dst_positive_scale_padded_iff_prefixtable)) /\ exists ff_q_pvs_padded_iff_prefixtableentrypositive. dst_positive_code_padded_iff_prefixtable = ff_q_pvs_padded_iff_prefixtableentrypositive * S ((S (dst_index_padded_iff_prefixtable)) * dst_positive_scale_padded_iff_prefixtable) + (dst_positive_padded_iff_prefixtable))) /\ (((((exists ff_h_pvs_padded_iff_prefixtableentrynegative. ff_h_pvs_padded_iff_prefixtableentrynegative + S (dst_negative_padded_iff_prefixtable) = S ((S (dst_index_padded_iff_prefixtable)) * dst_negative_scale_padded_iff_prefixtable)) /\ exists ff_q_pvs_padded_iff_prefixtableentrynegative. dst_negative_code_padded_iff_prefixtable = ff_q_pvs_padded_iff_prefixtableentrynegative * S ((S (dst_index_padded_iff_prefixtable)) * dst_negative_scale_padded_iff_prefixtable) + (dst_negative_padded_iff_prefixtable))) /\ (exists ge_balance_positive_padded_iff_prefixtableentryvalue ge_balance_negative_padded_iff_prefixtableentryvalue. (((((dst_value_padded_iff_prefixtable) = 2 * (ge_balance_positive_padded_iff_prefixtableentryvalue) /\ (ge_balance_negative_padded_iff_prefixtableentryvalue) = 0) \/ exists ge_signed_half_padded_iff_prefixtableentryvaluedecode. (((dst_value_padded_iff_prefixtable) = 2 * ge_signed_half_padded_iff_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_padded_iff_prefixtableentryvalue) = 0) /\ (ge_balance_negative_padded_iff_prefixtableentryvalue) = S ge_signed_half_padded_iff_prefixtableentryvaluedecode))) /\ ((dst_positive_padded_iff_prefixtable) + ge_balance_negative_padded_iff_prefixtableentryvalue = (dst_negative_padded_iff_prefixtable) + ge_balance_positive_padded_iff_prefixtableentryvalue))))))))) /\ (forall dc_index_padded_iff_prefix dc_value_padded_iff_prefix. (exists pvs_le_gap_padded_iff_prefixdomain. pvs_le_gap_padded_iff_prefixdomain + (dc_index_padded_iff_prefix) = (L)) -> (exists dst_positive_code_padded_iff_prefixlookup dst_positive_scale_padded_iff_prefixlookup dst_negative_code_padded_iff_prefixlookup dst_negative_scale_padded_iff_prefixlookup dst_positive_padded_iff_prefixlookup dst_negative_padded_iff_prefixlookup. (((M) = (((((dst_positive_code_padded_iff_prefixlookup) + (dst_positive_scale_padded_iff_prefixlookup)) * S ((dst_positive_code_padded_iff_prefixlookup) + (dst_positive_scale_padded_iff_prefixlookup)) + ((dst_positive_scale_padded_iff_prefixlookup) + (dst_positive_scale_padded_iff_prefixlookup))) + (((dst_negative_code_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)) * S ((dst_negative_code_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)) + ((dst_negative_scale_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)))) * S ((((dst_positive_code_padded_iff_prefixlookup) + (dst_positive_scale_padded_iff_prefixlookup)) * S ((dst_positive_code_padded_iff_prefixlookup) + (dst_positive_scale_padded_iff_prefixlookup)) + ((dst_positive_scale_padded_iff_prefixlookup) + (dst_positive_scale_padded_iff_prefixlookup))) + (((dst_negative_code_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)) * S ((dst_negative_code_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)) + ((dst_negative_scale_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)))) + ((((dst_negative_code_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)) * S ((dst_negative_code_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)) + ((dst_negative_scale_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup))) + (((dst_negative_code_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)) * S ((dst_negative_code_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)) + ((dst_negative_scale_padded_iff_prefixlookup) + (dst_negative_scale_padded_iff_prefixlookup)))))) /\ (((((exists ff_h_pvs_padded_iff_prefixlookuppositive. ff_h_pvs_padded_iff_prefixlookuppositive + S (dst_positive_padded_iff_prefixlookup) = S ((S (dc_index_padded_iff_prefix)) * dst_positive_scale_padded_iff_prefixlookup)) /\ exists ff_q_pvs_padded_iff_prefixlookuppositive. dst_positive_code_padded_iff_prefixlookup = ff_q_pvs_padded_iff_prefixlookuppositive * S ((S (dc_index_padded_iff_prefix)) * dst_positive_scale_padded_iff_prefixlookup) + (dst_positive_padded_iff_prefixlookup))) /\ (((((exists ff_h_pvs_padded_iff_prefixlookupnegative. ff_h_pvs_padded_iff_prefixlookupnegative + S (dst_negative_padded_iff_prefixlookup) = S ((S (dc_index_padded_iff_prefix)) * dst_negative_scale_padded_iff_prefixlookup)) /\ exists ff_q_pvs_padded_iff_prefixlookupnegative. dst_negative_code_padded_iff_prefixlookup = ff_q_pvs_padded_iff_prefixlookupnegative * S ((S (dc_index_padded_iff_prefix)) * dst_negative_scale_padded_iff_prefixlookup) + (dst_negative_padded_iff_prefixlookup))) /\ (exists ge_balance_positive_padded_iff_prefixlookupvalue ge_balance_negative_padded_iff_prefixlookupvalue. (((((dc_value_padded_iff_prefix) = 2 * (ge_balance_positive_padded_iff_prefixlookupvalue) /\ (ge_balance_negative_padded_iff_prefixlookupvalue) = 0) \/ exists ge_signed_half_padded_iff_prefixlookupvaluedecode. (((dc_value_padded_iff_prefix) = 2 * ge_signed_half_padded_iff_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_padded_iff_prefixlookupvalue) = 0) /\ (ge_balance_negative_padded_iff_prefixlookupvalue) = S ge_signed_half_padded_iff_prefixlookupvaluedecode))) /\ ((dst_positive_padded_iff_prefixlookup) + ge_balance_negative_padded_iff_prefixlookupvalue = (dst_negative_padded_iff_prefixlookup) + ge_balance_positive_padded_iff_prefixlookupvalue))))))))) -> ((((~((dc_index_padded_iff_prefix)=0)) /\ (exists dc_quotient_padded_iff_prefixentry dc_left_padded_iff_prefixentry dc_right_padded_iff_prefixentry. (((n)=(dc_index_padded_iff_prefix)*dc_quotient_padded_iff_prefixentry) /\ (((exists dst_positive_code_padded_iff_prefixentryleft dst_positive_scale_padded_iff_prefixentryleft dst_negative_code_padded_iff_prefixentryleft dst_negative_scale_padded_iff_prefixentryleft dst_positive_padded_iff_prefixentryleft dst_negative_padded_iff_prefixentryleft. (((F) = (((((dst_positive_code_padded_iff_prefixentryleft) + (dst_positive_scale_padded_iff_prefixentryleft)) * S ((dst_positive_code_padded_iff_prefixentryleft) + (dst_positive_scale_padded_iff_prefixentryleft)) + ((dst_positive_scale_padded_iff_prefixentryleft) + (dst_positive_scale_padded_iff_prefixentryleft))) + (((dst_negative_code_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)) * S ((dst_negative_code_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)) + ((dst_negative_scale_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)))) * S ((((dst_positive_code_padded_iff_prefixentryleft) + (dst_positive_scale_padded_iff_prefixentryleft)) * S ((dst_positive_code_padded_iff_prefixentryleft) + (dst_positive_scale_padded_iff_prefixentryleft)) + ((dst_positive_scale_padded_iff_prefixentryleft) + (dst_positive_scale_padded_iff_prefixentryleft))) + (((dst_negative_code_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)) * S ((dst_negative_code_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)) + ((dst_negative_scale_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)))) + ((((dst_negative_code_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)) * S ((dst_negative_code_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)) + ((dst_negative_scale_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft))) + (((dst_negative_code_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)) * S ((dst_negative_code_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)) + ((dst_negative_scale_padded_iff_prefixentryleft) + (dst_negative_scale_padded_iff_prefixentryleft)))))) /\ (((((exists ff_h_pvs_padded_iff_prefixentryleftpositive. ff_h_pvs_padded_iff_prefixentryleftpositive + S (dst_positive_padded_iff_prefixentryleft) = S ((S (dc_index_padded_iff_prefix)) * dst_positive_scale_padded_iff_prefixentryleft)) /\ exists ff_q_pvs_padded_iff_prefixentryleftpositive. dst_positive_code_padded_iff_prefixentryleft = ff_q_pvs_padded_iff_prefixentryleftpositive * S ((S (dc_index_padded_iff_prefix)) * dst_positive_scale_padded_iff_prefixentryleft) + (dst_positive_padded_iff_prefixentryleft))) /\ (((((exists ff_h_pvs_padded_iff_prefixentryleftnegative. ff_h_pvs_padded_iff_prefixentryleftnegative + S (dst_negative_padded_iff_prefixentryleft) = S ((S (dc_index_padded_iff_prefix)) * dst_negative_scale_padded_iff_prefixentryleft)) /\ exists ff_q_pvs_padded_iff_prefixentryleftnegative. dst_negative_code_padded_iff_prefixentryleft = ff_q_pvs_padded_iff_prefixentryleftnegative * S ((S (dc_index_padded_iff_prefix)) * dst_negative_scale_padded_iff_prefixentryleft) + (dst_negative_padded_iff_prefixentryleft))) /\ (exists ge_balance_positive_padded_iff_prefixentryleftvalue ge_balance_negative_padded_iff_prefixentryleftvalue. (((((dc_left_padded_iff_prefixentry) = 2 * (ge_balance_positive_padded_iff_prefixentryleftvalue) /\ (ge_balance_negative_padded_iff_prefixentryleftvalue) = 0) \/ exists ge_signed_half_padded_iff_prefixentryleftvaluedecode. (((dc_left_padded_iff_prefixentry) = 2 * ge_signed_half_padded_iff_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_padded_iff_prefixentryleftvalue) = 0) /\ (ge_balance_negative_padded_iff_prefixentryleftvalue) = S ge_signed_half_padded_iff_prefixentryleftvaluedecode))) /\ ((dst_positive_padded_iff_prefixentryleft) + ge_balance_negative_padded_iff_prefixentryleftvalue = (dst_negative_padded_iff_prefixentryleft) + ge_balance_positive_padded_iff_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_padded_iff_prefixentryright dst_positive_scale_padded_iff_prefixentryright dst_negative_code_padded_iff_prefixentryright dst_negative_scale_padded_iff_prefixentryright dst_positive_padded_iff_prefixentryright dst_negative_padded_iff_prefixentryright. (((G) = (((((dst_positive_code_padded_iff_prefixentryright) + (dst_positive_scale_padded_iff_prefixentryright)) * S ((dst_positive_code_padded_iff_prefixentryright) + (dst_positive_scale_padded_iff_prefixentryright)) + ((dst_positive_scale_padded_iff_prefixentryright) + (dst_positive_scale_padded_iff_prefixentryright))) + (((dst_negative_code_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)) * S ((dst_negative_code_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)) + ((dst_negative_scale_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)))) * S ((((dst_positive_code_padded_iff_prefixentryright) + (dst_positive_scale_padded_iff_prefixentryright)) * S ((dst_positive_code_padded_iff_prefixentryright) + (dst_positive_scale_padded_iff_prefixentryright)) + ((dst_positive_scale_padded_iff_prefixentryright) + (dst_positive_scale_padded_iff_prefixentryright))) + (((dst_negative_code_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)) * S ((dst_negative_code_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)) + ((dst_negative_scale_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)))) + ((((dst_negative_code_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)) * S ((dst_negative_code_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)) + ((dst_negative_scale_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright))) + (((dst_negative_code_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)) * S ((dst_negative_code_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)) + ((dst_negative_scale_padded_iff_prefixentryright) + (dst_negative_scale_padded_iff_prefixentryright)))))) /\ (((((exists ff_h_pvs_padded_iff_prefixentryrightpositive. ff_h_pvs_padded_iff_prefixentryrightpositive + S (dst_positive_padded_iff_prefixentryright) = S ((S (dc_quotient_padded_iff_prefixentry)) * dst_positive_scale_padded_iff_prefixentryright)) /\ exists ff_q_pvs_padded_iff_prefixentryrightpositive. dst_positive_code_padded_iff_prefixentryright = ff_q_pvs_padded_iff_prefixentryrightpositive * S ((S (dc_quotient_padded_iff_prefixentry)) * dst_positive_scale_padded_iff_prefixentryright) + (dst_positive_padded_iff_prefixentryright))) /\ (((((exists ff_h_pvs_padded_iff_prefixentryrightnegative. ff_h_pvs_padded_iff_prefixentryrightnegative + S (dst_negative_padded_iff_prefixentryright) = S ((S (dc_quotient_padded_iff_prefixentry)) * dst_negative_scale_padded_iff_prefixentryright)) /\ exists ff_q_pvs_padded_iff_prefixentryrightnegative. dst_negative_code_padded_iff_prefixentryright = ff_q_pvs_padded_iff_prefixentryrightnegative * S ((S (dc_quotient_padded_iff_prefixentry)) * dst_negative_scale_padded_iff_prefixentryright) + (dst_negative_padded_iff_prefixentryright))) /\ (exists ge_balance_positive_padded_iff_prefixentryrightvalue ge_balance_negative_padded_iff_prefixentryrightvalue. (((((dc_right_padded_iff_prefixentry) = 2 * (ge_balance_positive_padded_iff_prefixentryrightvalue) /\ (ge_balance_negative_padded_iff_prefixentryrightvalue) = 0) \/ exists ge_signed_half_padded_iff_prefixentryrightvaluedecode. (((dc_right_padded_iff_prefixentry) = 2 * ge_signed_half_padded_iff_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_padded_iff_prefixentryrightvalue) = 0) /\ (ge_balance_negative_padded_iff_prefixentryrightvalue) = S ge_signed_half_padded_iff_prefixentryrightvaluedecode))) /\ ((dst_positive_padded_iff_prefixentryright) + ge_balance_negative_padded_iff_prefixentryrightvalue = (dst_negative_padded_iff_prefixentryright) + ge_balance_positive_padded_iff_prefixentryrightvalue))))))))) /\ (exists sto_ap_padded_iff_prefixentryproduct sto_an_padded_iff_prefixentryproduct sto_bp_padded_iff_prefixentryproduct sto_bn_padded_iff_prefixentryproduct sto_cp_padded_iff_prefixentryproduct sto_cn_padded_iff_prefixentryproduct. (((((dc_left_padded_iff_prefixentry) = 2 * (sto_ap_padded_iff_prefixentryproduct) /\ (sto_an_padded_iff_prefixentryproduct) = 0) \/ exists ge_signed_half_padded_iff_prefixentryproductleft. (((dc_left_padded_iff_prefixentry) = 2 * ge_signed_half_padded_iff_prefixentryproductleft + 1 /\ (sto_ap_padded_iff_prefixentryproduct) = 0) /\ (sto_an_padded_iff_prefixentryproduct) = S ge_signed_half_padded_iff_prefixentryproductleft))) /\ ((((((dc_right_padded_iff_prefixentry) = 2 * (sto_bp_padded_iff_prefixentryproduct) /\ (sto_bn_padded_iff_prefixentryproduct) = 0) \/ exists ge_signed_half_padded_iff_prefixentryproductright. (((dc_right_padded_iff_prefixentry) = 2 * ge_signed_half_padded_iff_prefixentryproductright + 1 /\ (sto_bp_padded_iff_prefixentryproduct) = 0) /\ (sto_bn_padded_iff_prefixentryproduct) = S ge_signed_half_padded_iff_prefixentryproductright))) /\ ((((((dc_value_padded_iff_prefix) = 2 * (sto_cp_padded_iff_prefixentryproduct) /\ (sto_cn_padded_iff_prefixentryproduct) = 0) \/ exists ge_signed_half_padded_iff_prefixentryproductoutput. (((dc_value_padded_iff_prefix) = 2 * ge_signed_half_padded_iff_prefixentryproductoutput + 1 /\ (sto_cp_padded_iff_prefixentryproduct) = 0) /\ (sto_cn_padded_iff_prefixentryproduct) = S ge_signed_half_padded_iff_prefixentryproductoutput))) /\ ((sto_ap_padded_iff_prefixentryproduct * sto_bp_padded_iff_prefixentryproduct + sto_an_padded_iff_prefixentryproduct * sto_bn_padded_iff_prefixentryproduct) + sto_cn_padded_iff_prefixentryproduct = (sto_ap_padded_iff_prefixentryproduct * sto_bn_padded_iff_prefixentryproduct + sto_an_padded_iff_prefixentryproduct * sto_bp_padded_iff_prefixentryproduct) + sto_cp_padded_iff_prefixentryproduct))))))))))))))) \/ ((((dc_index_padded_iff_prefix)=0 \/ ~(exists pvs_factor_padded_iff_prefixentrynondivisor. (n) = (dc_index_padded_iff_prefix) * pvs_factor_padded_iff_prefixentrynondivisor)) /\ ((dc_value_padded_iff_prefix)=0))))))) -> (((exists dst_positive_code_padded_iff_fold dst_positive_scale_padded_iff_fold dst_negative_code_padded_iff_fold dst_negative_scale_padded_iff_fold dst_positive_sum_padded_iff_fold dst_negative_sum_padded_iff_fold. (((M) = (((((dst_positive_code_padded_iff_fold) + (dst_positive_scale_padded_iff_fold)) * S ((dst_positive_code_padded_iff_fold) + (dst_positive_scale_padded_iff_fold)) + ((dst_positive_scale_padded_iff_fold) + (dst_positive_scale_padded_iff_fold))) + (((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) * S ((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) + ((dst_negative_scale_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)))) * S ((((dst_positive_code_padded_iff_fold) + (dst_positive_scale_padded_iff_fold)) * S ((dst_positive_code_padded_iff_fold) + (dst_positive_scale_padded_iff_fold)) + ((dst_positive_scale_padded_iff_fold) + (dst_positive_scale_padded_iff_fold))) + (((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) * S ((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) + ((dst_negative_scale_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)))) + ((((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) * S ((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) + ((dst_negative_scale_padded_iff_fold) + (dst_negative_scale_padded_iff_fold))) + (((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) * S ((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) + ((dst_negative_scale_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)))))) /\ (((exists fs_u_dst_padded_iff_foldpositive fs_v_dst_padded_iff_foldpositive. ((((exists fs_h_dst_padded_iff_foldpositive_body_start. fs_h_dst_padded_iff_foldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_iff_foldpositive)) /\ exists fs_q_dst_padded_iff_foldpositive_body_start. fs_u_dst_padded_iff_foldpositive = fs_q_dst_padded_iff_foldpositive_body_start * S ((S (0)) * fs_v_dst_padded_iff_foldpositive) + (0))) /\ ((((exists fs_h_dst_padded_iff_foldpositive_body_terminal. fs_h_dst_padded_iff_foldpositive_body_terminal + S (dst_positive_sum_padded_iff_fold) = S ((S (S L)) * fs_v_dst_padded_iff_foldpositive)) /\ exists fs_q_dst_padded_iff_foldpositive_body_terminal. fs_u_dst_padded_iff_foldpositive = fs_q_dst_padded_iff_foldpositive_body_terminal * S ((S (S L)) * fs_v_dst_padded_iff_foldpositive) + (dst_positive_sum_padded_iff_fold))) /\ forall fs_i_dst_padded_iff_foldpositive_body_steps. (exists fs_lt_dst_padded_iff_foldpositive_body_steps_bound. fs_lt_dst_padded_iff_foldpositive_body_steps_bound + S fs_i_dst_padded_iff_foldpositive_body_steps = S L) -> exists fs_a_dst_padded_iff_foldpositive_body_steps fs_r_dst_padded_iff_foldpositive_body_steps fs_s_dst_padded_iff_foldpositive_body_steps. ((((exists fs_h_dst_padded_iff_foldpositive_body_steps_summand. fs_h_dst_padded_iff_foldpositive_body_steps_summand + S (fs_a_dst_padded_iff_foldpositive_body_steps) = S ((S (fs_i_dst_padded_iff_foldpositive_body_steps)) * dst_positive_scale_padded_iff_fold)) /\ exists fs_q_dst_padded_iff_foldpositive_body_steps_summand. dst_positive_code_padded_iff_fold = fs_q_dst_padded_iff_foldpositive_body_steps_summand * S ((S (fs_i_dst_padded_iff_foldpositive_body_steps)) * dst_positive_scale_padded_iff_fold) + (fs_a_dst_padded_iff_foldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_iff_foldpositive_body_steps_partial. fs_h_dst_padded_iff_foldpositive_body_steps_partial + S (fs_r_dst_padded_iff_foldpositive_body_steps) = S ((S (fs_i_dst_padded_iff_foldpositive_body_steps)) * fs_v_dst_padded_iff_foldpositive)) /\ exists fs_q_dst_padded_iff_foldpositive_body_steps_partial. fs_u_dst_padded_iff_foldpositive = fs_q_dst_padded_iff_foldpositive_body_steps_partial * S ((S (fs_i_dst_padded_iff_foldpositive_body_steps)) * fs_v_dst_padded_iff_foldpositive) + (fs_r_dst_padded_iff_foldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_iff_foldpositive_body_steps_successor. fs_h_dst_padded_iff_foldpositive_body_steps_successor + S (fs_s_dst_padded_iff_foldpositive_body_steps) = S ((S (S fs_i_dst_padded_iff_foldpositive_body_steps)) * fs_v_dst_padded_iff_foldpositive)) /\ exists fs_q_dst_padded_iff_foldpositive_body_steps_successor. fs_u_dst_padded_iff_foldpositive = fs_q_dst_padded_iff_foldpositive_body_steps_successor * S ((S (S fs_i_dst_padded_iff_foldpositive_body_steps)) * fs_v_dst_padded_iff_foldpositive) + (fs_s_dst_padded_iff_foldpositive_body_steps))) /\ fs_s_dst_padded_iff_foldpositive_body_steps = fs_r_dst_padded_iff_foldpositive_body_steps + fs_a_dst_padded_iff_foldpositive_body_steps)))))) /\ (((exists fs_u_dst_padded_iff_foldnegative fs_v_dst_padded_iff_foldnegative. ((((exists fs_h_dst_padded_iff_foldnegative_body_start. fs_h_dst_padded_iff_foldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_iff_foldnegative)) /\ exists fs_q_dst_padded_iff_foldnegative_body_start. fs_u_dst_padded_iff_foldnegative = fs_q_dst_padded_iff_foldnegative_body_start * S ((S (0)) * fs_v_dst_padded_iff_foldnegative) + (0))) /\ ((((exists fs_h_dst_padded_iff_foldnegative_body_terminal. fs_h_dst_padded_iff_foldnegative_body_terminal + S (dst_negative_sum_padded_iff_fold) = S ((S (S L)) * fs_v_dst_padded_iff_foldnegative)) /\ exists fs_q_dst_padded_iff_foldnegative_body_terminal. fs_u_dst_padded_iff_foldnegative = fs_q_dst_padded_iff_foldnegative_body_terminal * S ((S (S L)) * fs_v_dst_padded_iff_foldnegative) + (dst_negative_sum_padded_iff_fold))) /\ forall fs_i_dst_padded_iff_foldnegative_body_steps. (exists fs_lt_dst_padded_iff_foldnegative_body_steps_bound. fs_lt_dst_padded_iff_foldnegative_body_steps_bound + S fs_i_dst_padded_iff_foldnegative_body_steps = S L) -> exists fs_a_dst_padded_iff_foldnegative_body_steps fs_r_dst_padded_iff_foldnegative_body_steps fs_s_dst_padded_iff_foldnegative_body_steps. ((((exists fs_h_dst_padded_iff_foldnegative_body_steps_summand. fs_h_dst_padded_iff_foldnegative_body_steps_summand + S (fs_a_dst_padded_iff_foldnegative_body_steps) = S ((S (fs_i_dst_padded_iff_foldnegative_body_steps)) * dst_negative_scale_padded_iff_fold)) /\ exists fs_q_dst_padded_iff_foldnegative_body_steps_summand. dst_negative_code_padded_iff_fold = fs_q_dst_padded_iff_foldnegative_body_steps_summand * S ((S (fs_i_dst_padded_iff_foldnegative_body_steps)) * dst_negative_scale_padded_iff_fold) + (fs_a_dst_padded_iff_foldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_iff_foldnegative_body_steps_partial. fs_h_dst_padded_iff_foldnegative_body_steps_partial + S (fs_r_dst_padded_iff_foldnegative_body_steps) = S ((S (fs_i_dst_padded_iff_foldnegative_body_steps)) * fs_v_dst_padded_iff_foldnegative)) /\ exists fs_q_dst_padded_iff_foldnegative_body_steps_partial. fs_u_dst_padded_iff_foldnegative = fs_q_dst_padded_iff_foldnegative_body_steps_partial * S ((S (fs_i_dst_padded_iff_foldnegative_body_steps)) * fs_v_dst_padded_iff_foldnegative) + (fs_r_dst_padded_iff_foldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_iff_foldnegative_body_steps_successor. fs_h_dst_padded_iff_foldnegative_body_steps_successor + S (fs_s_dst_padded_iff_foldnegative_body_steps) = S ((S (S fs_i_dst_padded_iff_foldnegative_body_steps)) * fs_v_dst_padded_iff_foldnegative)) /\ exists fs_q_dst_padded_iff_foldnegative_body_steps_successor. fs_u_dst_padded_iff_foldnegative = fs_q_dst_padded_iff_foldnegative_body_steps_successor * S ((S (S fs_i_dst_padded_iff_foldnegative_body_steps)) * fs_v_dst_padded_iff_foldnegative) + (fs_s_dst_padded_iff_foldnegative_body_steps))) /\ fs_s_dst_padded_iff_foldnegative_body_steps = fs_r_dst_padded_iff_foldnegative_body_steps + fs_a_dst_padded_iff_foldnegative_body_steps)))))) /\ (exists ge_balance_positive_padded_iff_foldresult ge_balance_negative_padded_iff_foldresult. (((((z) = 2 * (ge_balance_positive_padded_iff_foldresult) /\ (ge_balance_negative_padded_iff_foldresult) = 0) \/ exists ge_signed_half_padded_iff_foldresultdecode. (((z) = 2 * ge_signed_half_padded_iff_foldresultdecode + 1 /\ (ge_balance_positive_padded_iff_foldresult) = 0) /\ (ge_balance_negative_padded_iff_foldresult) = S ge_signed_half_padded_iff_foldresultdecode))) /\ ((dst_positive_sum_padded_iff_fold) + ge_balance_negative_padded_iff_foldresult = (dst_negative_sum_padded_iff_fold) + ge_balance_positive_padded_iff_foldresult))))))))) -> (((~((n)=0)) /\ (exists dc_mask_padded_iff_value. ((((exists dst_positive_code_padded_iff_valuemasktable dst_positive_scale_padded_iff_valuemasktable dst_negative_code_padded_iff_valuemasktable dst_negative_scale_padded_iff_valuemasktable. (((dc_mask_padded_iff_value) = (((((dst_positive_code_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable)) * S ((dst_positive_code_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable)) + ((dst_positive_scale_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable))) + (((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) * S ((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) + ((dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)))) * S ((((dst_positive_code_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable)) * S ((dst_positive_code_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable)) + ((dst_positive_scale_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable))) + (((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) * S ((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) + ((dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)))) + ((((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) * S ((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) + ((dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable))) + (((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) * S ((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) + ((dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)))))) /\ (forall dst_index_padded_iff_valuemasktable. (exists pvs_le_gap_padded_iff_valuemasktabledomain. pvs_le_gap_padded_iff_valuemasktabledomain + (dst_index_padded_iff_valuemasktable) = (n)) -> exists dst_positive_padded_iff_valuemasktable dst_negative_padded_iff_valuemasktable dst_value_padded_iff_valuemasktable. ((((exists ff_h_pvs_padded_iff_valuemasktableentrypositive. ff_h_pvs_padded_iff_valuemasktableentrypositive + S (dst_positive_padded_iff_valuemasktable) = S ((S (dst_index_padded_iff_valuemasktable)) * dst_positive_scale_padded_iff_valuemasktable)) /\ exists ff_q_pvs_padded_iff_valuemasktableentrypositive. dst_positive_code_padded_iff_valuemasktable = ff_q_pvs_padded_iff_valuemasktableentrypositive * S ((S (dst_index_padded_iff_valuemasktable)) * dst_positive_scale_padded_iff_valuemasktable) + (dst_positive_padded_iff_valuemasktable))) /\ (((((exists ff_h_pvs_padded_iff_valuemasktableentrynegative. ff_h_pvs_padded_iff_valuemasktableentrynegative + S (dst_negative_padded_iff_valuemasktable) = S ((S (dst_index_padded_iff_valuemasktable)) * dst_negative_scale_padded_iff_valuemasktable)) /\ exists ff_q_pvs_padded_iff_valuemasktableentrynegative. dst_negative_code_padded_iff_valuemasktable = ff_q_pvs_padded_iff_valuemasktableentrynegative * S ((S (dst_index_padded_iff_valuemasktable)) * dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_padded_iff_valuemasktable))) /\ (exists ge_balance_positive_padded_iff_valuemasktableentryvalue ge_balance_negative_padded_iff_valuemasktableentryvalue. (((((dst_value_padded_iff_valuemasktable) = 2 * (ge_balance_positive_padded_iff_valuemasktableentryvalue) /\ (ge_balance_negative_padded_iff_valuemasktableentryvalue) = 0) \/ exists ge_signed_half_padded_iff_valuemasktableentryvaluedecode. (((dst_value_padded_iff_valuemasktable) = 2 * ge_signed_half_padded_iff_valuemasktableentryvaluedecode + 1 /\ (ge_balance_positive_padded_iff_valuemasktableentryvalue) = 0) /\ (ge_balance_negative_padded_iff_valuemasktableentryvalue) = S ge_signed_half_padded_iff_valuemasktableentryvaluedecode))) /\ ((dst_positive_padded_iff_valuemasktable) + ge_balance_negative_padded_iff_valuemasktableentryvalue = (dst_negative_padded_iff_valuemasktable) + ge_balance_positive_padded_iff_valuemasktableentryvalue))))))))) /\ (forall dc_index_padded_iff_valuemask dc_value_padded_iff_valuemask. (exists pvs_le_gap_padded_iff_valuemaskdomain. pvs_le_gap_padded_iff_valuemaskdomain + (dc_index_padded_iff_valuemask) = (n)) -> (exists dst_positive_code_padded_iff_valuemasklookup dst_positive_scale_padded_iff_valuemasklookup dst_negative_code_padded_iff_valuemasklookup dst_negative_scale_padded_iff_valuemasklookup dst_positive_padded_iff_valuemasklookup dst_negative_padded_iff_valuemasklookup. (((dc_mask_padded_iff_value) = (((((dst_positive_code_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup)) * S ((dst_positive_code_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup)) + ((dst_positive_scale_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup))) + (((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) * S ((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) + ((dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)))) * S ((((dst_positive_code_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup)) * S ((dst_positive_code_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup)) + ((dst_positive_scale_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup))) + (((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) * S ((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) + ((dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)))) + ((((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) * S ((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) + ((dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup))) + (((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) * S ((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) + ((dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)))))) /\ (((((exists ff_h_pvs_padded_iff_valuemasklookuppositive. ff_h_pvs_padded_iff_valuemasklookuppositive + S (dst_positive_padded_iff_valuemasklookup) = S ((S (dc_index_padded_iff_valuemask)) * dst_positive_scale_padded_iff_valuemasklookup)) /\ exists ff_q_pvs_padded_iff_valuemasklookuppositive. dst_positive_code_padded_iff_valuemasklookup = ff_q_pvs_padded_iff_valuemasklookuppositive * S ((S (dc_index_padded_iff_valuemask)) * dst_positive_scale_padded_iff_valuemasklookup) + (dst_positive_padded_iff_valuemasklookup))) /\ (((((exists ff_h_pvs_padded_iff_valuemasklookupnegative. ff_h_pvs_padded_iff_valuemasklookupnegative + S (dst_negative_padded_iff_valuemasklookup) = S ((S (dc_index_padded_iff_valuemask)) * dst_negative_scale_padded_iff_valuemasklookup)) /\ exists ff_q_pvs_padded_iff_valuemasklookupnegative. dst_negative_code_padded_iff_valuemasklookup = ff_q_pvs_padded_iff_valuemasklookupnegative * S ((S (dc_index_padded_iff_valuemask)) * dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_padded_iff_valuemasklookup))) /\ (exists ge_balance_positive_padded_iff_valuemasklookupvalue ge_balance_negative_padded_iff_valuemasklookupvalue. (((((dc_value_padded_iff_valuemask) = 2 * (ge_balance_positive_padded_iff_valuemasklookupvalue) /\ (ge_balance_negative_padded_iff_valuemasklookupvalue) = 0) \/ exists ge_signed_half_padded_iff_valuemasklookupvaluedecode. (((dc_value_padded_iff_valuemask) = 2 * ge_signed_half_padded_iff_valuemasklookupvaluedecode + 1 /\ (ge_balance_positive_padded_iff_valuemasklookupvalue) = 0) /\ (ge_balance_negative_padded_iff_valuemasklookupvalue) = S ge_signed_half_padded_iff_valuemasklookupvaluedecode))) /\ ((dst_positive_padded_iff_valuemasklookup) + ge_balance_negative_padded_iff_valuemasklookupvalue = (dst_negative_padded_iff_valuemasklookup) + ge_balance_positive_padded_iff_valuemasklookupvalue))))))))) -> ((((~((dc_index_padded_iff_valuemask)=0)) /\ (exists dc_quotient_padded_iff_valuemaskentry dc_left_padded_iff_valuemaskentry dc_right_padded_iff_valuemaskentry. (((n)=(dc_index_padded_iff_valuemask)*dc_quotient_padded_iff_valuemaskentry) /\ (((exists dst_positive_code_padded_iff_valuemaskentryleft dst_positive_scale_padded_iff_valuemaskentryleft dst_negative_code_padded_iff_valuemaskentryleft dst_negative_scale_padded_iff_valuemaskentryleft dst_positive_padded_iff_valuemaskentryleft dst_negative_padded_iff_valuemaskentryleft. (((F) = (((((dst_positive_code_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft)) * S ((dst_positive_code_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft)) + ((dst_positive_scale_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft))) + (((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) * S ((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) + ((dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)))) * S ((((dst_positive_code_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft)) * S ((dst_positive_code_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft)) + ((dst_positive_scale_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft))) + (((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) * S ((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) + ((dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)))) + ((((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) * S ((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) + ((dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft))) + (((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) * S ((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) + ((dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)))))) /\ (((((exists ff_h_pvs_padded_iff_valuemaskentryleftpositive. ff_h_pvs_padded_iff_valuemaskentryleftpositive + S (dst_positive_padded_iff_valuemaskentryleft) = S ((S (dc_index_padded_iff_valuemask)) * dst_positive_scale_padded_iff_valuemaskentryleft)) /\ exists ff_q_pvs_padded_iff_valuemaskentryleftpositive. dst_positive_code_padded_iff_valuemaskentryleft = ff_q_pvs_padded_iff_valuemaskentryleftpositive * S ((S (dc_index_padded_iff_valuemask)) * dst_positive_scale_padded_iff_valuemaskentryleft) + (dst_positive_padded_iff_valuemaskentryleft))) /\ (((((exists ff_h_pvs_padded_iff_valuemaskentryleftnegative. ff_h_pvs_padded_iff_valuemaskentryleftnegative + S (dst_negative_padded_iff_valuemaskentryleft) = S ((S (dc_index_padded_iff_valuemask)) * dst_negative_scale_padded_iff_valuemaskentryleft)) /\ exists ff_q_pvs_padded_iff_valuemaskentryleftnegative. dst_negative_code_padded_iff_valuemaskentryleft = ff_q_pvs_padded_iff_valuemaskentryleftnegative * S ((S (dc_index_padded_iff_valuemask)) * dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_padded_iff_valuemaskentryleft))) /\ (exists ge_balance_positive_padded_iff_valuemaskentryleftvalue ge_balance_negative_padded_iff_valuemaskentryleftvalue. (((((dc_left_padded_iff_valuemaskentry) = 2 * (ge_balance_positive_padded_iff_valuemaskentryleftvalue) /\ (ge_balance_negative_padded_iff_valuemaskentryleftvalue) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryleftvaluedecode. (((dc_left_padded_iff_valuemaskentry) = 2 * ge_signed_half_padded_iff_valuemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_padded_iff_valuemaskentryleftvalue) = 0) /\ (ge_balance_negative_padded_iff_valuemaskentryleftvalue) = S ge_signed_half_padded_iff_valuemaskentryleftvaluedecode))) /\ ((dst_positive_padded_iff_valuemaskentryleft) + ge_balance_negative_padded_iff_valuemaskentryleftvalue = (dst_negative_padded_iff_valuemaskentryleft) + ge_balance_positive_padded_iff_valuemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_padded_iff_valuemaskentryright dst_positive_scale_padded_iff_valuemaskentryright dst_negative_code_padded_iff_valuemaskentryright dst_negative_scale_padded_iff_valuemaskentryright dst_positive_padded_iff_valuemaskentryright dst_negative_padded_iff_valuemaskentryright. (((G) = (((((dst_positive_code_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright)) * S ((dst_positive_code_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright)) + ((dst_positive_scale_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright))) + (((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) * S ((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) + ((dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)))) * S ((((dst_positive_code_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright)) * S ((dst_positive_code_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright)) + ((dst_positive_scale_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright))) + (((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) * S ((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) + ((dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)))) + ((((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) * S ((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) + ((dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright))) + (((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) * S ((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) + ((dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)))))) /\ (((((exists ff_h_pvs_padded_iff_valuemaskentryrightpositive. ff_h_pvs_padded_iff_valuemaskentryrightpositive + S (dst_positive_padded_iff_valuemaskentryright) = S ((S (dc_quotient_padded_iff_valuemaskentry)) * dst_positive_scale_padded_iff_valuemaskentryright)) /\ exists ff_q_pvs_padded_iff_valuemaskentryrightpositive. dst_positive_code_padded_iff_valuemaskentryright = ff_q_pvs_padded_iff_valuemaskentryrightpositive * S ((S (dc_quotient_padded_iff_valuemaskentry)) * dst_positive_scale_padded_iff_valuemaskentryright) + (dst_positive_padded_iff_valuemaskentryright))) /\ (((((exists ff_h_pvs_padded_iff_valuemaskentryrightnegative. ff_h_pvs_padded_iff_valuemaskentryrightnegative + S (dst_negative_padded_iff_valuemaskentryright) = S ((S (dc_quotient_padded_iff_valuemaskentry)) * dst_negative_scale_padded_iff_valuemaskentryright)) /\ exists ff_q_pvs_padded_iff_valuemaskentryrightnegative. dst_negative_code_padded_iff_valuemaskentryright = ff_q_pvs_padded_iff_valuemaskentryrightnegative * S ((S (dc_quotient_padded_iff_valuemaskentry)) * dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_padded_iff_valuemaskentryright))) /\ (exists ge_balance_positive_padded_iff_valuemaskentryrightvalue ge_balance_negative_padded_iff_valuemaskentryrightvalue. (((((dc_right_padded_iff_valuemaskentry) = 2 * (ge_balance_positive_padded_iff_valuemaskentryrightvalue) /\ (ge_balance_negative_padded_iff_valuemaskentryrightvalue) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryrightvaluedecode. (((dc_right_padded_iff_valuemaskentry) = 2 * ge_signed_half_padded_iff_valuemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_padded_iff_valuemaskentryrightvalue) = 0) /\ (ge_balance_negative_padded_iff_valuemaskentryrightvalue) = S ge_signed_half_padded_iff_valuemaskentryrightvaluedecode))) /\ ((dst_positive_padded_iff_valuemaskentryright) + ge_balance_negative_padded_iff_valuemaskentryrightvalue = (dst_negative_padded_iff_valuemaskentryright) + ge_balance_positive_padded_iff_valuemaskentryrightvalue))))))))) /\ (exists sto_ap_padded_iff_valuemaskentryproduct sto_an_padded_iff_valuemaskentryproduct sto_bp_padded_iff_valuemaskentryproduct sto_bn_padded_iff_valuemaskentryproduct sto_cp_padded_iff_valuemaskentryproduct sto_cn_padded_iff_valuemaskentryproduct. (((((dc_left_padded_iff_valuemaskentry) = 2 * (sto_ap_padded_iff_valuemaskentryproduct) /\ (sto_an_padded_iff_valuemaskentryproduct) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryproductleft. (((dc_left_padded_iff_valuemaskentry) = 2 * ge_signed_half_padded_iff_valuemaskentryproductleft + 1 /\ (sto_ap_padded_iff_valuemaskentryproduct) = 0) /\ (sto_an_padded_iff_valuemaskentryproduct) = S ge_signed_half_padded_iff_valuemaskentryproductleft))) /\ ((((((dc_right_padded_iff_valuemaskentry) = 2 * (sto_bp_padded_iff_valuemaskentryproduct) /\ (sto_bn_padded_iff_valuemaskentryproduct) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryproductright. (((dc_right_padded_iff_valuemaskentry) = 2 * ge_signed_half_padded_iff_valuemaskentryproductright + 1 /\ (sto_bp_padded_iff_valuemaskentryproduct) = 0) /\ (sto_bn_padded_iff_valuemaskentryproduct) = S ge_signed_half_padded_iff_valuemaskentryproductright))) /\ ((((((dc_value_padded_iff_valuemask) = 2 * (sto_cp_padded_iff_valuemaskentryproduct) /\ (sto_cn_padded_iff_valuemaskentryproduct) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryproductoutput. (((dc_value_padded_iff_valuemask) = 2 * ge_signed_half_padded_iff_valuemaskentryproductoutput + 1 /\ (sto_cp_padded_iff_valuemaskentryproduct) = 0) /\ (sto_cn_padded_iff_valuemaskentryproduct) = S ge_signed_half_padded_iff_valuemaskentryproductoutput))) /\ ((sto_ap_padded_iff_valuemaskentryproduct * sto_bp_padded_iff_valuemaskentryproduct + sto_an_padded_iff_valuemaskentryproduct * sto_bn_padded_iff_valuemaskentryproduct) + sto_cn_padded_iff_valuemaskentryproduct = (sto_ap_padded_iff_valuemaskentryproduct * sto_bn_padded_iff_valuemaskentryproduct + sto_an_padded_iff_valuemaskentryproduct * sto_bp_padded_iff_valuemaskentryproduct) + sto_cp_padded_iff_valuemaskentryproduct))))))))))))))) \/ ((((dc_index_padded_iff_valuemask)=0 \/ ~(exists pvs_factor_padded_iff_valuemaskentrynondivisor. (n) = (dc_index_padded_iff_valuemask) * pvs_factor_padded_iff_valuemaskentrynondivisor)) /\ ((dc_value_padded_iff_valuemask)=0))))))) /\ (exists dst_positive_code_padded_iff_valuefold dst_positive_scale_padded_iff_valuefold dst_negative_code_padded_iff_valuefold dst_negative_scale_padded_iff_valuefold dst_positive_sum_padded_iff_valuefold dst_negative_sum_padded_iff_valuefold. (((dc_mask_padded_iff_value) = (((((dst_positive_code_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold)) * S ((dst_positive_code_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold)) + ((dst_positive_scale_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold))) + (((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) * S ((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) + ((dst_negative_scale_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)))) * S ((((dst_positive_code_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold)) * S ((dst_positive_code_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold)) + ((dst_positive_scale_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold))) + (((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) * S ((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) + ((dst_negative_scale_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)))) + ((((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) * S ((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) + ((dst_negative_scale_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold))) + (((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) * S ((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) + ((dst_negative_scale_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)))))) /\ (((exists fs_u_dst_padded_iff_valuefoldpositive fs_v_dst_padded_iff_valuefoldpositive. ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_start. fs_h_dst_padded_iff_valuefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_iff_valuefoldpositive)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_start. fs_u_dst_padded_iff_valuefoldpositive = fs_q_dst_padded_iff_valuefoldpositive_body_start * S ((S (0)) * fs_v_dst_padded_iff_valuefoldpositive) + (0))) /\ ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_terminal. fs_h_dst_padded_iff_valuefoldpositive_body_terminal + S (dst_positive_sum_padded_iff_valuefold) = S ((S (S (n))) * fs_v_dst_padded_iff_valuefoldpositive)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_terminal. fs_u_dst_padded_iff_valuefoldpositive = fs_q_dst_padded_iff_valuefoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_padded_iff_valuefoldpositive) + (dst_positive_sum_padded_iff_valuefold))) /\ forall fs_i_dst_padded_iff_valuefoldpositive_body_steps. (exists fs_lt_dst_padded_iff_valuefoldpositive_body_steps_bound. fs_lt_dst_padded_iff_valuefoldpositive_body_steps_bound + S fs_i_dst_padded_iff_valuefoldpositive_body_steps = S (n)) -> exists fs_a_dst_padded_iff_valuefoldpositive_body_steps fs_r_dst_padded_iff_valuefoldpositive_body_steps fs_s_dst_padded_iff_valuefoldpositive_body_steps. ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_steps_summand. fs_h_dst_padded_iff_valuefoldpositive_body_steps_summand + S (fs_a_dst_padded_iff_valuefoldpositive_body_steps) = S ((S (fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * dst_positive_scale_padded_iff_valuefold)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_steps_summand. dst_positive_code_padded_iff_valuefold = fs_q_dst_padded_iff_valuefoldpositive_body_steps_summand * S ((S (fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * dst_positive_scale_padded_iff_valuefold) + (fs_a_dst_padded_iff_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_steps_partial. fs_h_dst_padded_iff_valuefoldpositive_body_steps_partial + S (fs_r_dst_padded_iff_valuefoldpositive_body_steps) = S ((S (fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * fs_v_dst_padded_iff_valuefoldpositive)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_steps_partial. fs_u_dst_padded_iff_valuefoldpositive = fs_q_dst_padded_iff_valuefoldpositive_body_steps_partial * S ((S (fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * fs_v_dst_padded_iff_valuefoldpositive) + (fs_r_dst_padded_iff_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_steps_successor. fs_h_dst_padded_iff_valuefoldpositive_body_steps_successor + S (fs_s_dst_padded_iff_valuefoldpositive_body_steps) = S ((S (S fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * fs_v_dst_padded_iff_valuefoldpositive)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_steps_successor. fs_u_dst_padded_iff_valuefoldpositive = fs_q_dst_padded_iff_valuefoldpositive_body_steps_successor * S ((S (S fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * fs_v_dst_padded_iff_valuefoldpositive) + (fs_s_dst_padded_iff_valuefoldpositive_body_steps))) /\ fs_s_dst_padded_iff_valuefoldpositive_body_steps = fs_r_dst_padded_iff_valuefoldpositive_body_steps + fs_a_dst_padded_iff_valuefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_padded_iff_valuefoldnegative fs_v_dst_padded_iff_valuefoldnegative. ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_start. fs_h_dst_padded_iff_valuefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_iff_valuefoldnegative)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_start. fs_u_dst_padded_iff_valuefoldnegative = fs_q_dst_padded_iff_valuefoldnegative_body_start * S ((S (0)) * fs_v_dst_padded_iff_valuefoldnegative) + (0))) /\ ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_terminal. fs_h_dst_padded_iff_valuefoldnegative_body_terminal + S (dst_negative_sum_padded_iff_valuefold) = S ((S (S (n))) * fs_v_dst_padded_iff_valuefoldnegative)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_terminal. fs_u_dst_padded_iff_valuefoldnegative = fs_q_dst_padded_iff_valuefoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_padded_iff_valuefoldnegative) + (dst_negative_sum_padded_iff_valuefold))) /\ forall fs_i_dst_padded_iff_valuefoldnegative_body_steps. (exists fs_lt_dst_padded_iff_valuefoldnegative_body_steps_bound. fs_lt_dst_padded_iff_valuefoldnegative_body_steps_bound + S fs_i_dst_padded_iff_valuefoldnegative_body_steps = S (n)) -> exists fs_a_dst_padded_iff_valuefoldnegative_body_steps fs_r_dst_padded_iff_valuefoldnegative_body_steps fs_s_dst_padded_iff_valuefoldnegative_body_steps. ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_steps_summand. fs_h_dst_padded_iff_valuefoldnegative_body_steps_summand + S (fs_a_dst_padded_iff_valuefoldnegative_body_steps) = S ((S (fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * dst_negative_scale_padded_iff_valuefold)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_steps_summand. dst_negative_code_padded_iff_valuefold = fs_q_dst_padded_iff_valuefoldnegative_body_steps_summand * S ((S (fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * dst_negative_scale_padded_iff_valuefold) + (fs_a_dst_padded_iff_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_steps_partial. fs_h_dst_padded_iff_valuefoldnegative_body_steps_partial + S (fs_r_dst_padded_iff_valuefoldnegative_body_steps) = S ((S (fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * fs_v_dst_padded_iff_valuefoldnegative)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_steps_partial. fs_u_dst_padded_iff_valuefoldnegative = fs_q_dst_padded_iff_valuefoldnegative_body_steps_partial * S ((S (fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * fs_v_dst_padded_iff_valuefoldnegative) + (fs_r_dst_padded_iff_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_steps_successor. fs_h_dst_padded_iff_valuefoldnegative_body_steps_successor + S (fs_s_dst_padded_iff_valuefoldnegative_body_steps) = S ((S (S fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * fs_v_dst_padded_iff_valuefoldnegative)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_steps_successor. fs_u_dst_padded_iff_valuefoldnegative = fs_q_dst_padded_iff_valuefoldnegative_body_steps_successor * S ((S (S fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * fs_v_dst_padded_iff_valuefoldnegative) + (fs_s_dst_padded_iff_valuefoldnegative_body_steps))) /\ fs_s_dst_padded_iff_valuefoldnegative_body_steps = fs_r_dst_padded_iff_valuefoldnegative_body_steps + fs_a_dst_padded_iff_valuefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_padded_iff_valuefoldresult ge_balance_negative_padded_iff_valuefoldresult. (((((z) = 2 * (ge_balance_positive_padded_iff_valuefoldresult) /\ (ge_balance_negative_padded_iff_valuefoldresult) = 0) \/ exists ge_signed_half_padded_iff_valuefoldresultdecode. (((z) = 2 * ge_signed_half_padded_iff_valuefoldresultdecode + 1 /\ (ge_balance_positive_padded_iff_valuefoldresult) = 0) /\ (ge_balance_negative_padded_iff_valuefoldresult) = S ge_signed_half_padded_iff_valuefoldresultdecode))) /\ ((dst_positive_sum_padded_iff_valuefold) + ge_balance_negative_padded_iff_valuefoldresult = (dst_negative_sum_padded_iff_valuefold) + ge_balance_positive_padded_iff_valuefoldresult)))))))))))))) /\ ((((~((n)=0)) /\ (exists dc_mask_padded_iff_value. ((((exists dst_positive_code_padded_iff_valuemasktable dst_positive_scale_padded_iff_valuemasktable dst_negative_code_padded_iff_valuemasktable dst_negative_scale_padded_iff_valuemasktable. (((dc_mask_padded_iff_value) = (((((dst_positive_code_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable)) * S ((dst_positive_code_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable)) + ((dst_positive_scale_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable))) + (((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) * S ((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) + ((dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)))) * S ((((dst_positive_code_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable)) * S ((dst_positive_code_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable)) + ((dst_positive_scale_padded_iff_valuemasktable) + (dst_positive_scale_padded_iff_valuemasktable))) + (((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) * S ((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) + ((dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)))) + ((((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) * S ((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) + ((dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable))) + (((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) * S ((dst_negative_code_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)) + ((dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_scale_padded_iff_valuemasktable)))))) /\ (forall dst_index_padded_iff_valuemasktable. (exists pvs_le_gap_padded_iff_valuemasktabledomain. pvs_le_gap_padded_iff_valuemasktabledomain + (dst_index_padded_iff_valuemasktable) = (n)) -> exists dst_positive_padded_iff_valuemasktable dst_negative_padded_iff_valuemasktable dst_value_padded_iff_valuemasktable. ((((exists ff_h_pvs_padded_iff_valuemasktableentrypositive. ff_h_pvs_padded_iff_valuemasktableentrypositive + S (dst_positive_padded_iff_valuemasktable) = S ((S (dst_index_padded_iff_valuemasktable)) * dst_positive_scale_padded_iff_valuemasktable)) /\ exists ff_q_pvs_padded_iff_valuemasktableentrypositive. dst_positive_code_padded_iff_valuemasktable = ff_q_pvs_padded_iff_valuemasktableentrypositive * S ((S (dst_index_padded_iff_valuemasktable)) * dst_positive_scale_padded_iff_valuemasktable) + (dst_positive_padded_iff_valuemasktable))) /\ (((((exists ff_h_pvs_padded_iff_valuemasktableentrynegative. ff_h_pvs_padded_iff_valuemasktableentrynegative + S (dst_negative_padded_iff_valuemasktable) = S ((S (dst_index_padded_iff_valuemasktable)) * dst_negative_scale_padded_iff_valuemasktable)) /\ exists ff_q_pvs_padded_iff_valuemasktableentrynegative. dst_negative_code_padded_iff_valuemasktable = ff_q_pvs_padded_iff_valuemasktableentrynegative * S ((S (dst_index_padded_iff_valuemasktable)) * dst_negative_scale_padded_iff_valuemasktable) + (dst_negative_padded_iff_valuemasktable))) /\ (exists ge_balance_positive_padded_iff_valuemasktableentryvalue ge_balance_negative_padded_iff_valuemasktableentryvalue. (((((dst_value_padded_iff_valuemasktable) = 2 * (ge_balance_positive_padded_iff_valuemasktableentryvalue) /\ (ge_balance_negative_padded_iff_valuemasktableentryvalue) = 0) \/ exists ge_signed_half_padded_iff_valuemasktableentryvaluedecode. (((dst_value_padded_iff_valuemasktable) = 2 * ge_signed_half_padded_iff_valuemasktableentryvaluedecode + 1 /\ (ge_balance_positive_padded_iff_valuemasktableentryvalue) = 0) /\ (ge_balance_negative_padded_iff_valuemasktableentryvalue) = S ge_signed_half_padded_iff_valuemasktableentryvaluedecode))) /\ ((dst_positive_padded_iff_valuemasktable) + ge_balance_negative_padded_iff_valuemasktableentryvalue = (dst_negative_padded_iff_valuemasktable) + ge_balance_positive_padded_iff_valuemasktableentryvalue))))))))) /\ (forall dc_index_padded_iff_valuemask dc_value_padded_iff_valuemask. (exists pvs_le_gap_padded_iff_valuemaskdomain. pvs_le_gap_padded_iff_valuemaskdomain + (dc_index_padded_iff_valuemask) = (n)) -> (exists dst_positive_code_padded_iff_valuemasklookup dst_positive_scale_padded_iff_valuemasklookup dst_negative_code_padded_iff_valuemasklookup dst_negative_scale_padded_iff_valuemasklookup dst_positive_padded_iff_valuemasklookup dst_negative_padded_iff_valuemasklookup. (((dc_mask_padded_iff_value) = (((((dst_positive_code_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup)) * S ((dst_positive_code_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup)) + ((dst_positive_scale_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup))) + (((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) * S ((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) + ((dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)))) * S ((((dst_positive_code_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup)) * S ((dst_positive_code_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup)) + ((dst_positive_scale_padded_iff_valuemasklookup) + (dst_positive_scale_padded_iff_valuemasklookup))) + (((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) * S ((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) + ((dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)))) + ((((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) * S ((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) + ((dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup))) + (((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) * S ((dst_negative_code_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)) + ((dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_scale_padded_iff_valuemasklookup)))))) /\ (((((exists ff_h_pvs_padded_iff_valuemasklookuppositive. ff_h_pvs_padded_iff_valuemasklookuppositive + S (dst_positive_padded_iff_valuemasklookup) = S ((S (dc_index_padded_iff_valuemask)) * dst_positive_scale_padded_iff_valuemasklookup)) /\ exists ff_q_pvs_padded_iff_valuemasklookuppositive. dst_positive_code_padded_iff_valuemasklookup = ff_q_pvs_padded_iff_valuemasklookuppositive * S ((S (dc_index_padded_iff_valuemask)) * dst_positive_scale_padded_iff_valuemasklookup) + (dst_positive_padded_iff_valuemasklookup))) /\ (((((exists ff_h_pvs_padded_iff_valuemasklookupnegative. ff_h_pvs_padded_iff_valuemasklookupnegative + S (dst_negative_padded_iff_valuemasklookup) = S ((S (dc_index_padded_iff_valuemask)) * dst_negative_scale_padded_iff_valuemasklookup)) /\ exists ff_q_pvs_padded_iff_valuemasklookupnegative. dst_negative_code_padded_iff_valuemasklookup = ff_q_pvs_padded_iff_valuemasklookupnegative * S ((S (dc_index_padded_iff_valuemask)) * dst_negative_scale_padded_iff_valuemasklookup) + (dst_negative_padded_iff_valuemasklookup))) /\ (exists ge_balance_positive_padded_iff_valuemasklookupvalue ge_balance_negative_padded_iff_valuemasklookupvalue. (((((dc_value_padded_iff_valuemask) = 2 * (ge_balance_positive_padded_iff_valuemasklookupvalue) /\ (ge_balance_negative_padded_iff_valuemasklookupvalue) = 0) \/ exists ge_signed_half_padded_iff_valuemasklookupvaluedecode. (((dc_value_padded_iff_valuemask) = 2 * ge_signed_half_padded_iff_valuemasklookupvaluedecode + 1 /\ (ge_balance_positive_padded_iff_valuemasklookupvalue) = 0) /\ (ge_balance_negative_padded_iff_valuemasklookupvalue) = S ge_signed_half_padded_iff_valuemasklookupvaluedecode))) /\ ((dst_positive_padded_iff_valuemasklookup) + ge_balance_negative_padded_iff_valuemasklookupvalue = (dst_negative_padded_iff_valuemasklookup) + ge_balance_positive_padded_iff_valuemasklookupvalue))))))))) -> ((((~((dc_index_padded_iff_valuemask)=0)) /\ (exists dc_quotient_padded_iff_valuemaskentry dc_left_padded_iff_valuemaskentry dc_right_padded_iff_valuemaskentry. (((n)=(dc_index_padded_iff_valuemask)*dc_quotient_padded_iff_valuemaskentry) /\ (((exists dst_positive_code_padded_iff_valuemaskentryleft dst_positive_scale_padded_iff_valuemaskentryleft dst_negative_code_padded_iff_valuemaskentryleft dst_negative_scale_padded_iff_valuemaskentryleft dst_positive_padded_iff_valuemaskentryleft dst_negative_padded_iff_valuemaskentryleft. (((F) = (((((dst_positive_code_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft)) * S ((dst_positive_code_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft)) + ((dst_positive_scale_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft))) + (((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) * S ((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) + ((dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)))) * S ((((dst_positive_code_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft)) * S ((dst_positive_code_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft)) + ((dst_positive_scale_padded_iff_valuemaskentryleft) + (dst_positive_scale_padded_iff_valuemaskentryleft))) + (((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) * S ((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) + ((dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)))) + ((((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) * S ((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) + ((dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft))) + (((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) * S ((dst_negative_code_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)) + ((dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_scale_padded_iff_valuemaskentryleft)))))) /\ (((((exists ff_h_pvs_padded_iff_valuemaskentryleftpositive. ff_h_pvs_padded_iff_valuemaskentryleftpositive + S (dst_positive_padded_iff_valuemaskentryleft) = S ((S (dc_index_padded_iff_valuemask)) * dst_positive_scale_padded_iff_valuemaskentryleft)) /\ exists ff_q_pvs_padded_iff_valuemaskentryleftpositive. dst_positive_code_padded_iff_valuemaskentryleft = ff_q_pvs_padded_iff_valuemaskentryleftpositive * S ((S (dc_index_padded_iff_valuemask)) * dst_positive_scale_padded_iff_valuemaskentryleft) + (dst_positive_padded_iff_valuemaskentryleft))) /\ (((((exists ff_h_pvs_padded_iff_valuemaskentryleftnegative. ff_h_pvs_padded_iff_valuemaskentryleftnegative + S (dst_negative_padded_iff_valuemaskentryleft) = S ((S (dc_index_padded_iff_valuemask)) * dst_negative_scale_padded_iff_valuemaskentryleft)) /\ exists ff_q_pvs_padded_iff_valuemaskentryleftnegative. dst_negative_code_padded_iff_valuemaskentryleft = ff_q_pvs_padded_iff_valuemaskentryleftnegative * S ((S (dc_index_padded_iff_valuemask)) * dst_negative_scale_padded_iff_valuemaskentryleft) + (dst_negative_padded_iff_valuemaskentryleft))) /\ (exists ge_balance_positive_padded_iff_valuemaskentryleftvalue ge_balance_negative_padded_iff_valuemaskentryleftvalue. (((((dc_left_padded_iff_valuemaskentry) = 2 * (ge_balance_positive_padded_iff_valuemaskentryleftvalue) /\ (ge_balance_negative_padded_iff_valuemaskentryleftvalue) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryleftvaluedecode. (((dc_left_padded_iff_valuemaskentry) = 2 * ge_signed_half_padded_iff_valuemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_padded_iff_valuemaskentryleftvalue) = 0) /\ (ge_balance_negative_padded_iff_valuemaskentryleftvalue) = S ge_signed_half_padded_iff_valuemaskentryleftvaluedecode))) /\ ((dst_positive_padded_iff_valuemaskentryleft) + ge_balance_negative_padded_iff_valuemaskentryleftvalue = (dst_negative_padded_iff_valuemaskentryleft) + ge_balance_positive_padded_iff_valuemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_padded_iff_valuemaskentryright dst_positive_scale_padded_iff_valuemaskentryright dst_negative_code_padded_iff_valuemaskentryright dst_negative_scale_padded_iff_valuemaskentryright dst_positive_padded_iff_valuemaskentryright dst_negative_padded_iff_valuemaskentryright. (((G) = (((((dst_positive_code_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright)) * S ((dst_positive_code_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright)) + ((dst_positive_scale_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright))) + (((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) * S ((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) + ((dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)))) * S ((((dst_positive_code_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright)) * S ((dst_positive_code_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright)) + ((dst_positive_scale_padded_iff_valuemaskentryright) + (dst_positive_scale_padded_iff_valuemaskentryright))) + (((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) * S ((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) + ((dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)))) + ((((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) * S ((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) + ((dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright))) + (((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) * S ((dst_negative_code_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)) + ((dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_scale_padded_iff_valuemaskentryright)))))) /\ (((((exists ff_h_pvs_padded_iff_valuemaskentryrightpositive. ff_h_pvs_padded_iff_valuemaskentryrightpositive + S (dst_positive_padded_iff_valuemaskentryright) = S ((S (dc_quotient_padded_iff_valuemaskentry)) * dst_positive_scale_padded_iff_valuemaskentryright)) /\ exists ff_q_pvs_padded_iff_valuemaskentryrightpositive. dst_positive_code_padded_iff_valuemaskentryright = ff_q_pvs_padded_iff_valuemaskentryrightpositive * S ((S (dc_quotient_padded_iff_valuemaskentry)) * dst_positive_scale_padded_iff_valuemaskentryright) + (dst_positive_padded_iff_valuemaskentryright))) /\ (((((exists ff_h_pvs_padded_iff_valuemaskentryrightnegative. ff_h_pvs_padded_iff_valuemaskentryrightnegative + S (dst_negative_padded_iff_valuemaskentryright) = S ((S (dc_quotient_padded_iff_valuemaskentry)) * dst_negative_scale_padded_iff_valuemaskentryright)) /\ exists ff_q_pvs_padded_iff_valuemaskentryrightnegative. dst_negative_code_padded_iff_valuemaskentryright = ff_q_pvs_padded_iff_valuemaskentryrightnegative * S ((S (dc_quotient_padded_iff_valuemaskentry)) * dst_negative_scale_padded_iff_valuemaskentryright) + (dst_negative_padded_iff_valuemaskentryright))) /\ (exists ge_balance_positive_padded_iff_valuemaskentryrightvalue ge_balance_negative_padded_iff_valuemaskentryrightvalue. (((((dc_right_padded_iff_valuemaskentry) = 2 * (ge_balance_positive_padded_iff_valuemaskentryrightvalue) /\ (ge_balance_negative_padded_iff_valuemaskentryrightvalue) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryrightvaluedecode. (((dc_right_padded_iff_valuemaskentry) = 2 * ge_signed_half_padded_iff_valuemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_padded_iff_valuemaskentryrightvalue) = 0) /\ (ge_balance_negative_padded_iff_valuemaskentryrightvalue) = S ge_signed_half_padded_iff_valuemaskentryrightvaluedecode))) /\ ((dst_positive_padded_iff_valuemaskentryright) + ge_balance_negative_padded_iff_valuemaskentryrightvalue = (dst_negative_padded_iff_valuemaskentryright) + ge_balance_positive_padded_iff_valuemaskentryrightvalue))))))))) /\ (exists sto_ap_padded_iff_valuemaskentryproduct sto_an_padded_iff_valuemaskentryproduct sto_bp_padded_iff_valuemaskentryproduct sto_bn_padded_iff_valuemaskentryproduct sto_cp_padded_iff_valuemaskentryproduct sto_cn_padded_iff_valuemaskentryproduct. (((((dc_left_padded_iff_valuemaskentry) = 2 * (sto_ap_padded_iff_valuemaskentryproduct) /\ (sto_an_padded_iff_valuemaskentryproduct) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryproductleft. (((dc_left_padded_iff_valuemaskentry) = 2 * ge_signed_half_padded_iff_valuemaskentryproductleft + 1 /\ (sto_ap_padded_iff_valuemaskentryproduct) = 0) /\ (sto_an_padded_iff_valuemaskentryproduct) = S ge_signed_half_padded_iff_valuemaskentryproductleft))) /\ ((((((dc_right_padded_iff_valuemaskentry) = 2 * (sto_bp_padded_iff_valuemaskentryproduct) /\ (sto_bn_padded_iff_valuemaskentryproduct) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryproductright. (((dc_right_padded_iff_valuemaskentry) = 2 * ge_signed_half_padded_iff_valuemaskentryproductright + 1 /\ (sto_bp_padded_iff_valuemaskentryproduct) = 0) /\ (sto_bn_padded_iff_valuemaskentryproduct) = S ge_signed_half_padded_iff_valuemaskentryproductright))) /\ ((((((dc_value_padded_iff_valuemask) = 2 * (sto_cp_padded_iff_valuemaskentryproduct) /\ (sto_cn_padded_iff_valuemaskentryproduct) = 0) \/ exists ge_signed_half_padded_iff_valuemaskentryproductoutput. (((dc_value_padded_iff_valuemask) = 2 * ge_signed_half_padded_iff_valuemaskentryproductoutput + 1 /\ (sto_cp_padded_iff_valuemaskentryproduct) = 0) /\ (sto_cn_padded_iff_valuemaskentryproduct) = S ge_signed_half_padded_iff_valuemaskentryproductoutput))) /\ ((sto_ap_padded_iff_valuemaskentryproduct * sto_bp_padded_iff_valuemaskentryproduct + sto_an_padded_iff_valuemaskentryproduct * sto_bn_padded_iff_valuemaskentryproduct) + sto_cn_padded_iff_valuemaskentryproduct = (sto_ap_padded_iff_valuemaskentryproduct * sto_bn_padded_iff_valuemaskentryproduct + sto_an_padded_iff_valuemaskentryproduct * sto_bp_padded_iff_valuemaskentryproduct) + sto_cp_padded_iff_valuemaskentryproduct))))))))))))))) \/ ((((dc_index_padded_iff_valuemask)=0 \/ ~(exists pvs_factor_padded_iff_valuemaskentrynondivisor. (n) = (dc_index_padded_iff_valuemask) * pvs_factor_padded_iff_valuemaskentrynondivisor)) /\ ((dc_value_padded_iff_valuemask)=0))))))) /\ (exists dst_positive_code_padded_iff_valuefold dst_positive_scale_padded_iff_valuefold dst_negative_code_padded_iff_valuefold dst_negative_scale_padded_iff_valuefold dst_positive_sum_padded_iff_valuefold dst_negative_sum_padded_iff_valuefold. (((dc_mask_padded_iff_value) = (((((dst_positive_code_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold)) * S ((dst_positive_code_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold)) + ((dst_positive_scale_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold))) + (((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) * S ((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) + ((dst_negative_scale_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)))) * S ((((dst_positive_code_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold)) * S ((dst_positive_code_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold)) + ((dst_positive_scale_padded_iff_valuefold) + (dst_positive_scale_padded_iff_valuefold))) + (((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) * S ((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) + ((dst_negative_scale_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)))) + ((((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) * S ((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) + ((dst_negative_scale_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold))) + (((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) * S ((dst_negative_code_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)) + ((dst_negative_scale_padded_iff_valuefold) + (dst_negative_scale_padded_iff_valuefold)))))) /\ (((exists fs_u_dst_padded_iff_valuefoldpositive fs_v_dst_padded_iff_valuefoldpositive. ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_start. fs_h_dst_padded_iff_valuefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_iff_valuefoldpositive)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_start. fs_u_dst_padded_iff_valuefoldpositive = fs_q_dst_padded_iff_valuefoldpositive_body_start * S ((S (0)) * fs_v_dst_padded_iff_valuefoldpositive) + (0))) /\ ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_terminal. fs_h_dst_padded_iff_valuefoldpositive_body_terminal + S (dst_positive_sum_padded_iff_valuefold) = S ((S (S (n))) * fs_v_dst_padded_iff_valuefoldpositive)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_terminal. fs_u_dst_padded_iff_valuefoldpositive = fs_q_dst_padded_iff_valuefoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_padded_iff_valuefoldpositive) + (dst_positive_sum_padded_iff_valuefold))) /\ forall fs_i_dst_padded_iff_valuefoldpositive_body_steps. (exists fs_lt_dst_padded_iff_valuefoldpositive_body_steps_bound. fs_lt_dst_padded_iff_valuefoldpositive_body_steps_bound + S fs_i_dst_padded_iff_valuefoldpositive_body_steps = S (n)) -> exists fs_a_dst_padded_iff_valuefoldpositive_body_steps fs_r_dst_padded_iff_valuefoldpositive_body_steps fs_s_dst_padded_iff_valuefoldpositive_body_steps. ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_steps_summand. fs_h_dst_padded_iff_valuefoldpositive_body_steps_summand + S (fs_a_dst_padded_iff_valuefoldpositive_body_steps) = S ((S (fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * dst_positive_scale_padded_iff_valuefold)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_steps_summand. dst_positive_code_padded_iff_valuefold = fs_q_dst_padded_iff_valuefoldpositive_body_steps_summand * S ((S (fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * dst_positive_scale_padded_iff_valuefold) + (fs_a_dst_padded_iff_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_steps_partial. fs_h_dst_padded_iff_valuefoldpositive_body_steps_partial + S (fs_r_dst_padded_iff_valuefoldpositive_body_steps) = S ((S (fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * fs_v_dst_padded_iff_valuefoldpositive)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_steps_partial. fs_u_dst_padded_iff_valuefoldpositive = fs_q_dst_padded_iff_valuefoldpositive_body_steps_partial * S ((S (fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * fs_v_dst_padded_iff_valuefoldpositive) + (fs_r_dst_padded_iff_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_iff_valuefoldpositive_body_steps_successor. fs_h_dst_padded_iff_valuefoldpositive_body_steps_successor + S (fs_s_dst_padded_iff_valuefoldpositive_body_steps) = S ((S (S fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * fs_v_dst_padded_iff_valuefoldpositive)) /\ exists fs_q_dst_padded_iff_valuefoldpositive_body_steps_successor. fs_u_dst_padded_iff_valuefoldpositive = fs_q_dst_padded_iff_valuefoldpositive_body_steps_successor * S ((S (S fs_i_dst_padded_iff_valuefoldpositive_body_steps)) * fs_v_dst_padded_iff_valuefoldpositive) + (fs_s_dst_padded_iff_valuefoldpositive_body_steps))) /\ fs_s_dst_padded_iff_valuefoldpositive_body_steps = fs_r_dst_padded_iff_valuefoldpositive_body_steps + fs_a_dst_padded_iff_valuefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_padded_iff_valuefoldnegative fs_v_dst_padded_iff_valuefoldnegative. ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_start. fs_h_dst_padded_iff_valuefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_iff_valuefoldnegative)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_start. fs_u_dst_padded_iff_valuefoldnegative = fs_q_dst_padded_iff_valuefoldnegative_body_start * S ((S (0)) * fs_v_dst_padded_iff_valuefoldnegative) + (0))) /\ ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_terminal. fs_h_dst_padded_iff_valuefoldnegative_body_terminal + S (dst_negative_sum_padded_iff_valuefold) = S ((S (S (n))) * fs_v_dst_padded_iff_valuefoldnegative)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_terminal. fs_u_dst_padded_iff_valuefoldnegative = fs_q_dst_padded_iff_valuefoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_padded_iff_valuefoldnegative) + (dst_negative_sum_padded_iff_valuefold))) /\ forall fs_i_dst_padded_iff_valuefoldnegative_body_steps. (exists fs_lt_dst_padded_iff_valuefoldnegative_body_steps_bound. fs_lt_dst_padded_iff_valuefoldnegative_body_steps_bound + S fs_i_dst_padded_iff_valuefoldnegative_body_steps = S (n)) -> exists fs_a_dst_padded_iff_valuefoldnegative_body_steps fs_r_dst_padded_iff_valuefoldnegative_body_steps fs_s_dst_padded_iff_valuefoldnegative_body_steps. ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_steps_summand. fs_h_dst_padded_iff_valuefoldnegative_body_steps_summand + S (fs_a_dst_padded_iff_valuefoldnegative_body_steps) = S ((S (fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * dst_negative_scale_padded_iff_valuefold)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_steps_summand. dst_negative_code_padded_iff_valuefold = fs_q_dst_padded_iff_valuefoldnegative_body_steps_summand * S ((S (fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * dst_negative_scale_padded_iff_valuefold) + (fs_a_dst_padded_iff_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_steps_partial. fs_h_dst_padded_iff_valuefoldnegative_body_steps_partial + S (fs_r_dst_padded_iff_valuefoldnegative_body_steps) = S ((S (fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * fs_v_dst_padded_iff_valuefoldnegative)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_steps_partial. fs_u_dst_padded_iff_valuefoldnegative = fs_q_dst_padded_iff_valuefoldnegative_body_steps_partial * S ((S (fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * fs_v_dst_padded_iff_valuefoldnegative) + (fs_r_dst_padded_iff_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_iff_valuefoldnegative_body_steps_successor. fs_h_dst_padded_iff_valuefoldnegative_body_steps_successor + S (fs_s_dst_padded_iff_valuefoldnegative_body_steps) = S ((S (S fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * fs_v_dst_padded_iff_valuefoldnegative)) /\ exists fs_q_dst_padded_iff_valuefoldnegative_body_steps_successor. fs_u_dst_padded_iff_valuefoldnegative = fs_q_dst_padded_iff_valuefoldnegative_body_steps_successor * S ((S (S fs_i_dst_padded_iff_valuefoldnegative_body_steps)) * fs_v_dst_padded_iff_valuefoldnegative) + (fs_s_dst_padded_iff_valuefoldnegative_body_steps))) /\ fs_s_dst_padded_iff_valuefoldnegative_body_steps = fs_r_dst_padded_iff_valuefoldnegative_body_steps + fs_a_dst_padded_iff_valuefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_padded_iff_valuefoldresult ge_balance_negative_padded_iff_valuefoldresult. (((((z) = 2 * (ge_balance_positive_padded_iff_valuefoldresult) /\ (ge_balance_negative_padded_iff_valuefoldresult) = 0) \/ exists ge_signed_half_padded_iff_valuefoldresultdecode. (((z) = 2 * ge_signed_half_padded_iff_valuefoldresultdecode + 1 /\ (ge_balance_positive_padded_iff_valuefoldresult) = 0) /\ (ge_balance_negative_padded_iff_valuefoldresult) = S ge_signed_half_padded_iff_valuefoldresultdecode))) /\ ((dst_positive_sum_padded_iff_valuefold) + ge_balance_negative_padded_iff_valuefoldresult = (dst_negative_sum_padded_iff_valuefold) + ge_balance_positive_padded_iff_valuefoldresult))))))))))))) -> (exists dst_positive_code_padded_iff_fold dst_positive_scale_padded_iff_fold dst_negative_code_padded_iff_fold dst_negative_scale_padded_iff_fold dst_positive_sum_padded_iff_fold dst_negative_sum_padded_iff_fold. (((M) = (((((dst_positive_code_padded_iff_fold) + (dst_positive_scale_padded_iff_fold)) * S ((dst_positive_code_padded_iff_fold) + (dst_positive_scale_padded_iff_fold)) + ((dst_positive_scale_padded_iff_fold) + (dst_positive_scale_padded_iff_fold))) + (((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) * S ((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) + ((dst_negative_scale_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)))) * S ((((dst_positive_code_padded_iff_fold) + (dst_positive_scale_padded_iff_fold)) * S ((dst_positive_code_padded_iff_fold) + (dst_positive_scale_padded_iff_fold)) + ((dst_positive_scale_padded_iff_fold) + (dst_positive_scale_padded_iff_fold))) + (((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) * S ((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) + ((dst_negative_scale_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)))) + ((((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) * S ((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) + ((dst_negative_scale_padded_iff_fold) + (dst_negative_scale_padded_iff_fold))) + (((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) * S ((dst_negative_code_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)) + ((dst_negative_scale_padded_iff_fold) + (dst_negative_scale_padded_iff_fold)))))) /\ (((exists fs_u_dst_padded_iff_foldpositive fs_v_dst_padded_iff_foldpositive. ((((exists fs_h_dst_padded_iff_foldpositive_body_start. fs_h_dst_padded_iff_foldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_iff_foldpositive)) /\ exists fs_q_dst_padded_iff_foldpositive_body_start. fs_u_dst_padded_iff_foldpositive = fs_q_dst_padded_iff_foldpositive_body_start * S ((S (0)) * fs_v_dst_padded_iff_foldpositive) + (0))) /\ ((((exists fs_h_dst_padded_iff_foldpositive_body_terminal. fs_h_dst_padded_iff_foldpositive_body_terminal + S (dst_positive_sum_padded_iff_fold) = S ((S (S L)) * fs_v_dst_padded_iff_foldpositive)) /\ exists fs_q_dst_padded_iff_foldpositive_body_terminal. fs_u_dst_padded_iff_foldpositive = fs_q_dst_padded_iff_foldpositive_body_terminal * S ((S (S L)) * fs_v_dst_padded_iff_foldpositive) + (dst_positive_sum_padded_iff_fold))) /\ forall fs_i_dst_padded_iff_foldpositive_body_steps. (exists fs_lt_dst_padded_iff_foldpositive_body_steps_bound. fs_lt_dst_padded_iff_foldpositive_body_steps_bound + S fs_i_dst_padded_iff_foldpositive_body_steps = S L) -> exists fs_a_dst_padded_iff_foldpositive_body_steps fs_r_dst_padded_iff_foldpositive_body_steps fs_s_dst_padded_iff_foldpositive_body_steps. ((((exists fs_h_dst_padded_iff_foldpositive_body_steps_summand. fs_h_dst_padded_iff_foldpositive_body_steps_summand + S (fs_a_dst_padded_iff_foldpositive_body_steps) = S ((S (fs_i_dst_padded_iff_foldpositive_body_steps)) * dst_positive_scale_padded_iff_fold)) /\ exists fs_q_dst_padded_iff_foldpositive_body_steps_summand. dst_positive_code_padded_iff_fold = fs_q_dst_padded_iff_foldpositive_body_steps_summand * S ((S (fs_i_dst_padded_iff_foldpositive_body_steps)) * dst_positive_scale_padded_iff_fold) + (fs_a_dst_padded_iff_foldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_iff_foldpositive_body_steps_partial. fs_h_dst_padded_iff_foldpositive_body_steps_partial + S (fs_r_dst_padded_iff_foldpositive_body_steps) = S ((S (fs_i_dst_padded_iff_foldpositive_body_steps)) * fs_v_dst_padded_iff_foldpositive)) /\ exists fs_q_dst_padded_iff_foldpositive_body_steps_partial. fs_u_dst_padded_iff_foldpositive = fs_q_dst_padded_iff_foldpositive_body_steps_partial * S ((S (fs_i_dst_padded_iff_foldpositive_body_steps)) * fs_v_dst_padded_iff_foldpositive) + (fs_r_dst_padded_iff_foldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_iff_foldpositive_body_steps_successor. fs_h_dst_padded_iff_foldpositive_body_steps_successor + S (fs_s_dst_padded_iff_foldpositive_body_steps) = S ((S (S fs_i_dst_padded_iff_foldpositive_body_steps)) * fs_v_dst_padded_iff_foldpositive)) /\ exists fs_q_dst_padded_iff_foldpositive_body_steps_successor. fs_u_dst_padded_iff_foldpositive = fs_q_dst_padded_iff_foldpositive_body_steps_successor * S ((S (S fs_i_dst_padded_iff_foldpositive_body_steps)) * fs_v_dst_padded_iff_foldpositive) + (fs_s_dst_padded_iff_foldpositive_body_steps))) /\ fs_s_dst_padded_iff_foldpositive_body_steps = fs_r_dst_padded_iff_foldpositive_body_steps + fs_a_dst_padded_iff_foldpositive_body_steps)))))) /\ (((exists fs_u_dst_padded_iff_foldnegative fs_v_dst_padded_iff_foldnegative. ((((exists fs_h_dst_padded_iff_foldnegative_body_start. fs_h_dst_padded_iff_foldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_iff_foldnegative)) /\ exists fs_q_dst_padded_iff_foldnegative_body_start. fs_u_dst_padded_iff_foldnegative = fs_q_dst_padded_iff_foldnegative_body_start * S ((S (0)) * fs_v_dst_padded_iff_foldnegative) + (0))) /\ ((((exists fs_h_dst_padded_iff_foldnegative_body_terminal. fs_h_dst_padded_iff_foldnegative_body_terminal + S (dst_negative_sum_padded_iff_fold) = S ((S (S L)) * fs_v_dst_padded_iff_foldnegative)) /\ exists fs_q_dst_padded_iff_foldnegative_body_terminal. fs_u_dst_padded_iff_foldnegative = fs_q_dst_padded_iff_foldnegative_body_terminal * S ((S (S L)) * fs_v_dst_padded_iff_foldnegative) + (dst_negative_sum_padded_iff_fold))) /\ forall fs_i_dst_padded_iff_foldnegative_body_steps. (exists fs_lt_dst_padded_iff_foldnegative_body_steps_bound. fs_lt_dst_padded_iff_foldnegative_body_steps_bound + S fs_i_dst_padded_iff_foldnegative_body_steps = S L) -> exists fs_a_dst_padded_iff_foldnegative_body_steps fs_r_dst_padded_iff_foldnegative_body_steps fs_s_dst_padded_iff_foldnegative_body_steps. ((((exists fs_h_dst_padded_iff_foldnegative_body_steps_summand. fs_h_dst_padded_iff_foldnegative_body_steps_summand + S (fs_a_dst_padded_iff_foldnegative_body_steps) = S ((S (fs_i_dst_padded_iff_foldnegative_body_steps)) * dst_negative_scale_padded_iff_fold)) /\ exists fs_q_dst_padded_iff_foldnegative_body_steps_summand. dst_negative_code_padded_iff_fold = fs_q_dst_padded_iff_foldnegative_body_steps_summand * S ((S (fs_i_dst_padded_iff_foldnegative_body_steps)) * dst_negative_scale_padded_iff_fold) + (fs_a_dst_padded_iff_foldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_iff_foldnegative_body_steps_partial. fs_h_dst_padded_iff_foldnegative_body_steps_partial + S (fs_r_dst_padded_iff_foldnegative_body_steps) = S ((S (fs_i_dst_padded_iff_foldnegative_body_steps)) * fs_v_dst_padded_iff_foldnegative)) /\ exists fs_q_dst_padded_iff_foldnegative_body_steps_partial. fs_u_dst_padded_iff_foldnegative = fs_q_dst_padded_iff_foldnegative_body_steps_partial * S ((S (fs_i_dst_padded_iff_foldnegative_body_steps)) * fs_v_dst_padded_iff_foldnegative) + (fs_r_dst_padded_iff_foldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_iff_foldnegative_body_steps_successor. fs_h_dst_padded_iff_foldnegative_body_steps_successor + S (fs_s_dst_padded_iff_foldnegative_body_steps) = S ((S (S fs_i_dst_padded_iff_foldnegative_body_steps)) * fs_v_dst_padded_iff_foldnegative)) /\ exists fs_q_dst_padded_iff_foldnegative_body_steps_successor. fs_u_dst_padded_iff_foldnegative = fs_q_dst_padded_iff_foldnegative_body_steps_successor * S ((S (S fs_i_dst_padded_iff_foldnegative_body_steps)) * fs_v_dst_padded_iff_foldnegative) + (fs_s_dst_padded_iff_foldnegative_body_steps))) /\ fs_s_dst_padded_iff_foldnegative_body_steps = fs_r_dst_padded_iff_foldnegative_body_steps + fs_a_dst_padded_iff_foldnegative_body_steps)))))) /\ (exists ge_balance_positive_padded_iff_foldresult ge_balance_negative_padded_iff_foldresult. (((((z) = 2 * (ge_balance_positive_padded_iff_foldresult) /\ (ge_balance_negative_padded_iff_foldresult) = 0) \/ exists ge_signed_half_padded_iff_foldresultdecode. (((z) = 2 * ge_signed_half_padded_iff_foldresultdecode + 1 /\ (ge_balance_positive_padded_iff_foldresult) = 0) /\ (ge_balance_negative_padded_iff_foldresult) = S ge_signed_half_padded_iff_foldresultdecode))) /\ ((dst_positive_sum_padded_iff_fold) + ge_balance_negative_padded_iff_foldresult = (dst_negative_sum_padded_iff_fold) + ge_balance_positive_padded_iff_foldresult)))))))))))Complete tactic proof in conservative notation
All 53 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
53 script commands · 13 reading checkpoints · 2 local claims
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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–9
02Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
split
03Fix variables and assumptionsL11–11
Work with arbitrary variables or the premises of the current implication.
- L11
intro hs
04Use earlier factsL12–21
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L12
specialize dirichlet_convolution_from_padded_prefix (F) - L13
specialize dirichlet_convolution_from_padded_prefix (G) - L14
specialize dirichlet_convolution_from_padded_prefix (n) - L15
specialize dirichlet_convolution_from_padded_prefix (L) - L16
specialize dirichlet_convolution_from_padded_prefix (M) - L17
specialize dirichlet_convolution_from_padded_prefix (z) - L18
apply dirichlet_convolution_from_padded_prefix - L19
exact hn - L20
exact hbound - L21
exact hp
05Use earlier factsL22–22
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L22
exact hs
06Fix variables and assumptionsL23–23
Work with arbitrary variables or the premises of the current implication.
- L23
intro hs
07Separate the logical casesL24–24
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L24
cases hp
08Establish htL25–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed sum exists.
- L25
have ht : ∃ a. SignedPrefixSum(M,S L,a)Definitions: SignedPrefixSum(M,S L,a)Original native command in the exact edition - L26
specialize arithmetic_signed_sum_exists (L) - L27
specialize arithmetic_signed_sum_exists (M) - L28
specialize arithmetic_signed_sum_exists (S L) - L29
apply arithmetic_signed_sum_exists - L30
exact hp_left
09Separate the logical casesL31–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L31
cases ht
10Establish heL32–41
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution sum functional.
- L32
have he : x=z - L33
specialize dirichlet_convolution_sum_functional (F) - L34
specialize dirichlet_convolution_sum_functional (G) - L35
specialize dirichlet_convolution_sum_functional (n) - L36
specialize dirichlet_convolution_sum_functional (x) - L37
specialize dirichlet_convolution_sum_functional (z) - L38
apply dirichlet_convolution_sum_functional - L39
specialize dirichlet_convolution_from_padded_prefix (F) - L40
specialize dirichlet_convolution_from_padded_prefix (G) - L41
specialize dirichlet_convolution_from_padded_prefix (n)
11Use earlier factsL42–50
Instantiate or apply named facts and discharge the corresponding proof obligations.
12Calculate and transport equalitiesL51–52
13Use earlier factsL53–53
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L53
exact ht_witness
Original defined command ledger · 53 lines
- 0001
intro F - 0002
intro G - 0003
intro n - 0004
intro L - 0005
intro M - 0006
intro z - 0007
intro hn - 0008
intro hbound - 0009
intro hp - 0010
split - 0011
intro hs - 0012
specialize dirichlet_convolution_from_padded_prefix (F) - 0013
specialize dirichlet_convolution_from_padded_prefix (G) - 0014
specialize dirichlet_convolution_from_padded_prefix (n) - 0015
specialize dirichlet_convolution_from_padded_prefix (L) - 0016
specialize dirichlet_convolution_from_padded_prefix (M) - 0017
specialize dirichlet_convolution_from_padded_prefix (z) - 0018
apply dirichlet_convolution_from_padded_prefix - 0019
exact hn - 0020
exact hbound - 0021
exact hp - 0022
exact hs - 0023
intro hs - 0024
cases hp - 0025
have ht : ∃ a. SignedPrefixSum(M,S L,a) - 0026
specialize arithmetic_signed_sum_exists (L) - 0027
specialize arithmetic_signed_sum_exists (M) - 0028
specialize arithmetic_signed_sum_exists (S L) - 0029
apply arithmetic_signed_sum_exists - 0030
exact hp_left - 0031
cases ht - 0032
have he : x=z - 0033
specialize dirichlet_convolution_sum_functional (F) - 0034
specialize dirichlet_convolution_sum_functional (G) - 0035
specialize dirichlet_convolution_sum_functional (n) - 0036
specialize dirichlet_convolution_sum_functional (x) - 0037
specialize dirichlet_convolution_sum_functional (z) - 0038
apply dirichlet_convolution_sum_functional - 0039
specialize dirichlet_convolution_from_padded_prefix (F) - 0040
specialize dirichlet_convolution_from_padded_prefix (G) - 0041
specialize dirichlet_convolution_from_padded_prefix (n) - 0042
specialize dirichlet_convolution_from_padded_prefix (L) - 0043
specialize dirichlet_convolution_from_padded_prefix (M) - 0044
specialize dirichlet_convolution_from_padded_prefix (x) - 0045
apply dirichlet_convolution_from_padded_prefix - 0046
exact hn - 0047
exact hbound - 0048
exact hp - 0049
exact ht_witness - 0050
exact hs - 0051
rewrite he at ht_witness - 0052
rewrite he at ht_witness - 0053
exact ht_witness