dirichlet_convolution_padded_prefix_iff

Exact expanded first-order arithmetic 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)))))))))))