dirichlet_convolution_sum_commutative

Exact expanded first-order arithmetic statement

forall F G n a b. (((~((n)=0)) /\ (exists dc_mask_commutative_first. ((((exists dst_positive_code_commutative_firstmasktable dst_positive_scale_commutative_firstmasktable dst_negative_code_commutative_firstmasktable dst_negative_scale_commutative_firstmasktable. (((dc_mask_commutative_first) = (((((dst_positive_code_commutative_firstmasktable) + (dst_positive_scale_commutative_firstmasktable)) * S ((dst_positive_code_commutative_firstmasktable) + (dst_positive_scale_commutative_firstmasktable)) + ((dst_positive_scale_commutative_firstmasktable) + (dst_positive_scale_commutative_firstmasktable))) + (((dst_negative_code_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)) * S ((dst_negative_code_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)) + ((dst_negative_scale_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)))) * S ((((dst_positive_code_commutative_firstmasktable) + (dst_positive_scale_commutative_firstmasktable)) * S ((dst_positive_code_commutative_firstmasktable) + (dst_positive_scale_commutative_firstmasktable)) + ((dst_positive_scale_commutative_firstmasktable) + (dst_positive_scale_commutative_firstmasktable))) + (((dst_negative_code_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)) * S ((dst_negative_code_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)) + ((dst_negative_scale_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)))) + ((((dst_negative_code_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)) * S ((dst_negative_code_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)) + ((dst_negative_scale_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable))) + (((dst_negative_code_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)) * S ((dst_negative_code_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)) + ((dst_negative_scale_commutative_firstmasktable) + (dst_negative_scale_commutative_firstmasktable)))))) /\ (forall dst_index_commutative_firstmasktable. (exists pvs_le_gap_commutative_firstmasktabledomain. pvs_le_gap_commutative_firstmasktabledomain + (dst_index_commutative_firstmasktable) = (n)) -> exists dst_positive_commutative_firstmasktable dst_negative_commutative_firstmasktable dst_value_commutative_firstmasktable. ((((exists ff_h_pvs_commutative_firstmasktableentrypositive. ff_h_pvs_commutative_firstmasktableentrypositive + S (dst_positive_commutative_firstmasktable) = S ((S (dst_index_commutative_firstmasktable)) * dst_positive_scale_commutative_firstmasktable)) /\ exists ff_q_pvs_commutative_firstmasktableentrypositive. dst_positive_code_commutative_firstmasktable = ff_q_pvs_commutative_firstmasktableentrypositive * S ((S (dst_index_commutative_firstmasktable)) * dst_positive_scale_commutative_firstmasktable) + (dst_positive_commutative_firstmasktable))) /\ (((((exists ff_h_pvs_commutative_firstmasktableentrynegative. ff_h_pvs_commutative_firstmasktableentrynegative + S (dst_negative_commutative_firstmasktable) = S ((S (dst_index_commutative_firstmasktable)) * dst_negative_scale_commutative_firstmasktable)) /\ exists ff_q_pvs_commutative_firstmasktableentrynegative. dst_negative_code_commutative_firstmasktable = ff_q_pvs_commutative_firstmasktableentrynegative * S ((S (dst_index_commutative_firstmasktable)) * dst_negative_scale_commutative_firstmasktable) + (dst_negative_commutative_firstmasktable))) /\ (exists ge_balance_positive_commutative_firstmasktableentryvalue ge_balance_negative_commutative_firstmasktableentryvalue. (((((dst_value_commutative_firstmasktable) = 2 * (ge_balance_positive_commutative_firstmasktableentryvalue) /\ (ge_balance_negative_commutative_firstmasktableentryvalue) = 0) \/ exists ge_signed_half_commutative_firstmasktableentryvaluedecode. (((dst_value_commutative_firstmasktable) = 2 * ge_signed_half_commutative_firstmasktableentryvaluedecode + 1 /\ (ge_balance_positive_commutative_firstmasktableentryvalue) = 0) /\ (ge_balance_negative_commutative_firstmasktableentryvalue) = S ge_signed_half_commutative_firstmasktableentryvaluedecode))) /\ ((dst_positive_commutative_firstmasktable) + ge_balance_negative_commutative_firstmasktableentryvalue = (dst_negative_commutative_firstmasktable) + ge_balance_positive_commutative_firstmasktableentryvalue))))))))) /\ (forall dc_index_commutative_firstmask dc_value_commutative_firstmask. (exists pvs_le_gap_commutative_firstmaskdomain. pvs_le_gap_commutative_firstmaskdomain + (dc_index_commutative_firstmask) = (n)) -> (exists dst_positive_code_commutative_firstmasklookup dst_positive_scale_commutative_firstmasklookup dst_negative_code_commutative_firstmasklookup dst_negative_scale_commutative_firstmasklookup dst_positive_commutative_firstmasklookup dst_negative_commutative_firstmasklookup. (((dc_mask_commutative_first) = (((((dst_positive_code_commutative_firstmasklookup) + (dst_positive_scale_commutative_firstmasklookup)) * S ((dst_positive_code_commutative_firstmasklookup) + (dst_positive_scale_commutative_firstmasklookup)) + ((dst_positive_scale_commutative_firstmasklookup) + (dst_positive_scale_commutative_firstmasklookup))) + (((dst_negative_code_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)) * S ((dst_negative_code_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)) + ((dst_negative_scale_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)))) * S ((((dst_positive_code_commutative_firstmasklookup) + (dst_positive_scale_commutative_firstmasklookup)) * S ((dst_positive_code_commutative_firstmasklookup) + (dst_positive_scale_commutative_firstmasklookup)) + ((dst_positive_scale_commutative_firstmasklookup) + (dst_positive_scale_commutative_firstmasklookup))) + (((dst_negative_code_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)) * S ((dst_negative_code_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)) + ((dst_negative_scale_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)))) + ((((dst_negative_code_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)) * S ((dst_negative_code_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)) + ((dst_negative_scale_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup))) + (((dst_negative_code_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)) * S ((dst_negative_code_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)) + ((dst_negative_scale_commutative_firstmasklookup) + (dst_negative_scale_commutative_firstmasklookup)))))) /\ (((((exists ff_h_pvs_commutative_firstmasklookuppositive. ff_h_pvs_commutative_firstmasklookuppositive + S (dst_positive_commutative_firstmasklookup) = S ((S (dc_index_commutative_firstmask)) * dst_positive_scale_commutative_firstmasklookup)) /\ exists ff_q_pvs_commutative_firstmasklookuppositive. dst_positive_code_commutative_firstmasklookup = ff_q_pvs_commutative_firstmasklookuppositive * S ((S (dc_index_commutative_firstmask)) * dst_positive_scale_commutative_firstmasklookup) + (dst_positive_commutative_firstmasklookup))) /\ (((((exists ff_h_pvs_commutative_firstmasklookupnegative. ff_h_pvs_commutative_firstmasklookupnegative + S (dst_negative_commutative_firstmasklookup) = S ((S (dc_index_commutative_firstmask)) * dst_negative_scale_commutative_firstmasklookup)) /\ exists ff_q_pvs_commutative_firstmasklookupnegative. dst_negative_code_commutative_firstmasklookup = ff_q_pvs_commutative_firstmasklookupnegative * S ((S (dc_index_commutative_firstmask)) * dst_negative_scale_commutative_firstmasklookup) + (dst_negative_commutative_firstmasklookup))) /\ (exists ge_balance_positive_commutative_firstmasklookupvalue ge_balance_negative_commutative_firstmasklookupvalue. (((((dc_value_commutative_firstmask) = 2 * (ge_balance_positive_commutative_firstmasklookupvalue) /\ (ge_balance_negative_commutative_firstmasklookupvalue) = 0) \/ exists ge_signed_half_commutative_firstmasklookupvaluedecode. (((dc_value_commutative_firstmask) = 2 * ge_signed_half_commutative_firstmasklookupvaluedecode + 1 /\ (ge_balance_positive_commutative_firstmasklookupvalue) = 0) /\ (ge_balance_negative_commutative_firstmasklookupvalue) = S ge_signed_half_commutative_firstmasklookupvaluedecode))) /\ ((dst_positive_commutative_firstmasklookup) + ge_balance_negative_commutative_firstmasklookupvalue = (dst_negative_commutative_firstmasklookup) + ge_balance_positive_commutative_firstmasklookupvalue))))))))) -> ((((~((dc_index_commutative_firstmask)=0)) /\ (exists dc_quotient_commutative_firstmaskentry dc_left_commutative_firstmaskentry dc_right_commutative_firstmaskentry. (((n)=(dc_index_commutative_firstmask)*dc_quotient_commutative_firstmaskentry) /\ (((exists dst_positive_code_commutative_firstmaskentryleft dst_positive_scale_commutative_firstmaskentryleft dst_negative_code_commutative_firstmaskentryleft dst_negative_scale_commutative_firstmaskentryleft dst_positive_commutative_firstmaskentryleft dst_negative_commutative_firstmaskentryleft. (((F) = (((((dst_positive_code_commutative_firstmaskentryleft) + (dst_positive_scale_commutative_firstmaskentryleft)) * S ((dst_positive_code_commutative_firstmaskentryleft) + (dst_positive_scale_commutative_firstmaskentryleft)) + ((dst_positive_scale_commutative_firstmaskentryleft) + (dst_positive_scale_commutative_firstmaskentryleft))) + (((dst_negative_code_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)) * S ((dst_negative_code_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)) + ((dst_negative_scale_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)))) * S ((((dst_positive_code_commutative_firstmaskentryleft) + (dst_positive_scale_commutative_firstmaskentryleft)) * S ((dst_positive_code_commutative_firstmaskentryleft) + (dst_positive_scale_commutative_firstmaskentryleft)) + ((dst_positive_scale_commutative_firstmaskentryleft) + (dst_positive_scale_commutative_firstmaskentryleft))) + (((dst_negative_code_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)) * S ((dst_negative_code_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)) + ((dst_negative_scale_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)))) + ((((dst_negative_code_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)) * S ((dst_negative_code_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)) + ((dst_negative_scale_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft))) + (((dst_negative_code_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)) * S ((dst_negative_code_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)) + ((dst_negative_scale_commutative_firstmaskentryleft) + (dst_negative_scale_commutative_firstmaskentryleft)))))) /\ (((((exists ff_h_pvs_commutative_firstmaskentryleftpositive. ff_h_pvs_commutative_firstmaskentryleftpositive + S (dst_positive_commutative_firstmaskentryleft) = S ((S (dc_index_commutative_firstmask)) * dst_positive_scale_commutative_firstmaskentryleft)) /\ exists ff_q_pvs_commutative_firstmaskentryleftpositive. dst_positive_code_commutative_firstmaskentryleft = ff_q_pvs_commutative_firstmaskentryleftpositive * S ((S (dc_index_commutative_firstmask)) * dst_positive_scale_commutative_firstmaskentryleft) + (dst_positive_commutative_firstmaskentryleft))) /\ (((((exists ff_h_pvs_commutative_firstmaskentryleftnegative. ff_h_pvs_commutative_firstmaskentryleftnegative + S (dst_negative_commutative_firstmaskentryleft) = S ((S (dc_index_commutative_firstmask)) * dst_negative_scale_commutative_firstmaskentryleft)) /\ exists ff_q_pvs_commutative_firstmaskentryleftnegative. dst_negative_code_commutative_firstmaskentryleft = ff_q_pvs_commutative_firstmaskentryleftnegative * S ((S (dc_index_commutative_firstmask)) * dst_negative_scale_commutative_firstmaskentryleft) + (dst_negative_commutative_firstmaskentryleft))) /\ (exists ge_balance_positive_commutative_firstmaskentryleftvalue ge_balance_negative_commutative_firstmaskentryleftvalue. (((((dc_left_commutative_firstmaskentry) = 2 * (ge_balance_positive_commutative_firstmaskentryleftvalue) /\ (ge_balance_negative_commutative_firstmaskentryleftvalue) = 0) \/ exists ge_signed_half_commutative_firstmaskentryleftvaluedecode. (((dc_left_commutative_firstmaskentry) = 2 * ge_signed_half_commutative_firstmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_commutative_firstmaskentryleftvalue) = 0) /\ (ge_balance_negative_commutative_firstmaskentryleftvalue) = S ge_signed_half_commutative_firstmaskentryleftvaluedecode))) /\ ((dst_positive_commutative_firstmaskentryleft) + ge_balance_negative_commutative_firstmaskentryleftvalue = (dst_negative_commutative_firstmaskentryleft) + ge_balance_positive_commutative_firstmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_commutative_firstmaskentryright dst_positive_scale_commutative_firstmaskentryright dst_negative_code_commutative_firstmaskentryright dst_negative_scale_commutative_firstmaskentryright dst_positive_commutative_firstmaskentryright dst_negative_commutative_firstmaskentryright. (((G) = (((((dst_positive_code_commutative_firstmaskentryright) + (dst_positive_scale_commutative_firstmaskentryright)) * S ((dst_positive_code_commutative_firstmaskentryright) + (dst_positive_scale_commutative_firstmaskentryright)) + ((dst_positive_scale_commutative_firstmaskentryright) + (dst_positive_scale_commutative_firstmaskentryright))) + (((dst_negative_code_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)) * S ((dst_negative_code_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)) + ((dst_negative_scale_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)))) * S ((((dst_positive_code_commutative_firstmaskentryright) + (dst_positive_scale_commutative_firstmaskentryright)) * S ((dst_positive_code_commutative_firstmaskentryright) + (dst_positive_scale_commutative_firstmaskentryright)) + ((dst_positive_scale_commutative_firstmaskentryright) + (dst_positive_scale_commutative_firstmaskentryright))) + (((dst_negative_code_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)) * S ((dst_negative_code_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)) + ((dst_negative_scale_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)))) + ((((dst_negative_code_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)) * S ((dst_negative_code_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)) + ((dst_negative_scale_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright))) + (((dst_negative_code_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)) * S ((dst_negative_code_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)) + ((dst_negative_scale_commutative_firstmaskentryright) + (dst_negative_scale_commutative_firstmaskentryright)))))) /\ (((((exists ff_h_pvs_commutative_firstmaskentryrightpositive. ff_h_pvs_commutative_firstmaskentryrightpositive + S (dst_positive_commutative_firstmaskentryright) = S ((S (dc_quotient_commutative_firstmaskentry)) * dst_positive_scale_commutative_firstmaskentryright)) /\ exists ff_q_pvs_commutative_firstmaskentryrightpositive. dst_positive_code_commutative_firstmaskentryright = ff_q_pvs_commutative_firstmaskentryrightpositive * S ((S (dc_quotient_commutative_firstmaskentry)) * dst_positive_scale_commutative_firstmaskentryright) + (dst_positive_commutative_firstmaskentryright))) /\ (((((exists ff_h_pvs_commutative_firstmaskentryrightnegative. ff_h_pvs_commutative_firstmaskentryrightnegative + S (dst_negative_commutative_firstmaskentryright) = S ((S (dc_quotient_commutative_firstmaskentry)) * dst_negative_scale_commutative_firstmaskentryright)) /\ exists ff_q_pvs_commutative_firstmaskentryrightnegative. dst_negative_code_commutative_firstmaskentryright = ff_q_pvs_commutative_firstmaskentryrightnegative * S ((S (dc_quotient_commutative_firstmaskentry)) * dst_negative_scale_commutative_firstmaskentryright) + (dst_negative_commutative_firstmaskentryright))) /\ (exists ge_balance_positive_commutative_firstmaskentryrightvalue ge_balance_negative_commutative_firstmaskentryrightvalue. (((((dc_right_commutative_firstmaskentry) = 2 * (ge_balance_positive_commutative_firstmaskentryrightvalue) /\ (ge_balance_negative_commutative_firstmaskentryrightvalue) = 0) \/ exists ge_signed_half_commutative_firstmaskentryrightvaluedecode. (((dc_right_commutative_firstmaskentry) = 2 * ge_signed_half_commutative_firstmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_commutative_firstmaskentryrightvalue) = 0) /\ (ge_balance_negative_commutative_firstmaskentryrightvalue) = S ge_signed_half_commutative_firstmaskentryrightvaluedecode))) /\ ((dst_positive_commutative_firstmaskentryright) + ge_balance_negative_commutative_firstmaskentryrightvalue = (dst_negative_commutative_firstmaskentryright) + ge_balance_positive_commutative_firstmaskentryrightvalue))))))))) /\ (exists sto_ap_commutative_firstmaskentryproduct sto_an_commutative_firstmaskentryproduct sto_bp_commutative_firstmaskentryproduct sto_bn_commutative_firstmaskentryproduct sto_cp_commutative_firstmaskentryproduct sto_cn_commutative_firstmaskentryproduct. (((((dc_left_commutative_firstmaskentry) = 2 * (sto_ap_commutative_firstmaskentryproduct) /\ (sto_an_commutative_firstmaskentryproduct) = 0) \/ exists ge_signed_half_commutative_firstmaskentryproductleft. (((dc_left_commutative_firstmaskentry) = 2 * ge_signed_half_commutative_firstmaskentryproductleft + 1 /\ (sto_ap_commutative_firstmaskentryproduct) = 0) /\ (sto_an_commutative_firstmaskentryproduct) = S ge_signed_half_commutative_firstmaskentryproductleft))) /\ ((((((dc_right_commutative_firstmaskentry) = 2 * (sto_bp_commutative_firstmaskentryproduct) /\ (sto_bn_commutative_firstmaskentryproduct) = 0) \/ exists ge_signed_half_commutative_firstmaskentryproductright. (((dc_right_commutative_firstmaskentry) = 2 * ge_signed_half_commutative_firstmaskentryproductright + 1 /\ (sto_bp_commutative_firstmaskentryproduct) = 0) /\ (sto_bn_commutative_firstmaskentryproduct) = S ge_signed_half_commutative_firstmaskentryproductright))) /\ ((((((dc_value_commutative_firstmask) = 2 * (sto_cp_commutative_firstmaskentryproduct) /\ (sto_cn_commutative_firstmaskentryproduct) = 0) \/ exists ge_signed_half_commutative_firstmaskentryproductoutput. (((dc_value_commutative_firstmask) = 2 * ge_signed_half_commutative_firstmaskentryproductoutput + 1 /\ (sto_cp_commutative_firstmaskentryproduct) = 0) /\ (sto_cn_commutative_firstmaskentryproduct) = S ge_signed_half_commutative_firstmaskentryproductoutput))) /\ ((sto_ap_commutative_firstmaskentryproduct * sto_bp_commutative_firstmaskentryproduct + sto_an_commutative_firstmaskentryproduct * sto_bn_commutative_firstmaskentryproduct) + sto_cn_commutative_firstmaskentryproduct = (sto_ap_commutative_firstmaskentryproduct * sto_bn_commutative_firstmaskentryproduct + sto_an_commutative_firstmaskentryproduct * sto_bp_commutative_firstmaskentryproduct) + sto_cp_commutative_firstmaskentryproduct))))))))))))))) \/ ((((dc_index_commutative_firstmask)=0 \/ ~(exists pvs_factor_commutative_firstmaskentrynondivisor. (n) = (dc_index_commutative_firstmask) * pvs_factor_commutative_firstmaskentrynondivisor)) /\ ((dc_value_commutative_firstmask)=0))))))) /\ (exists dst_positive_code_commutative_firstfold dst_positive_scale_commutative_firstfold dst_negative_code_commutative_firstfold dst_negative_scale_commutative_firstfold dst_positive_sum_commutative_firstfold dst_negative_sum_commutative_firstfold. (((dc_mask_commutative_first) = (((((dst_positive_code_commutative_firstfold) + (dst_positive_scale_commutative_firstfold)) * S ((dst_positive_code_commutative_firstfold) + (dst_positive_scale_commutative_firstfold)) + ((dst_positive_scale_commutative_firstfold) + (dst_positive_scale_commutative_firstfold))) + (((dst_negative_code_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)) * S ((dst_negative_code_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)) + ((dst_negative_scale_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)))) * S ((((dst_positive_code_commutative_firstfold) + (dst_positive_scale_commutative_firstfold)) * S ((dst_positive_code_commutative_firstfold) + (dst_positive_scale_commutative_firstfold)) + ((dst_positive_scale_commutative_firstfold) + (dst_positive_scale_commutative_firstfold))) + (((dst_negative_code_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)) * S ((dst_negative_code_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)) + ((dst_negative_scale_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)))) + ((((dst_negative_code_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)) * S ((dst_negative_code_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)) + ((dst_negative_scale_commutative_firstfold) + (dst_negative_scale_commutative_firstfold))) + (((dst_negative_code_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)) * S ((dst_negative_code_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)) + ((dst_negative_scale_commutative_firstfold) + (dst_negative_scale_commutative_firstfold)))))) /\ (((exists fs_u_dst_commutative_firstfoldpositive fs_v_dst_commutative_firstfoldpositive. ((((exists fs_h_dst_commutative_firstfoldpositive_body_start. fs_h_dst_commutative_firstfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_commutative_firstfoldpositive)) /\ exists fs_q_dst_commutative_firstfoldpositive_body_start. fs_u_dst_commutative_firstfoldpositive = fs_q_dst_commutative_firstfoldpositive_body_start * S ((S (0)) * fs_v_dst_commutative_firstfoldpositive) + (0))) /\ ((((exists fs_h_dst_commutative_firstfoldpositive_body_terminal. fs_h_dst_commutative_firstfoldpositive_body_terminal + S (dst_positive_sum_commutative_firstfold) = S ((S (S (n))) * fs_v_dst_commutative_firstfoldpositive)) /\ exists fs_q_dst_commutative_firstfoldpositive_body_terminal. fs_u_dst_commutative_firstfoldpositive = fs_q_dst_commutative_firstfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_commutative_firstfoldpositive) + (dst_positive_sum_commutative_firstfold))) /\ forall fs_i_dst_commutative_firstfoldpositive_body_steps. (exists fs_lt_dst_commutative_firstfoldpositive_body_steps_bound. fs_lt_dst_commutative_firstfoldpositive_body_steps_bound + S fs_i_dst_commutative_firstfoldpositive_body_steps = S (n)) -> exists fs_a_dst_commutative_firstfoldpositive_body_steps fs_r_dst_commutative_firstfoldpositive_body_steps fs_s_dst_commutative_firstfoldpositive_body_steps. ((((exists fs_h_dst_commutative_firstfoldpositive_body_steps_summand. fs_h_dst_commutative_firstfoldpositive_body_steps_summand + S (fs_a_dst_commutative_firstfoldpositive_body_steps) = S ((S (fs_i_dst_commutative_firstfoldpositive_body_steps)) * dst_positive_scale_commutative_firstfold)) /\ exists fs_q_dst_commutative_firstfoldpositive_body_steps_summand. dst_positive_code_commutative_firstfold = fs_q_dst_commutative_firstfoldpositive_body_steps_summand * S ((S (fs_i_dst_commutative_firstfoldpositive_body_steps)) * dst_positive_scale_commutative_firstfold) + (fs_a_dst_commutative_firstfoldpositive_body_steps))) /\ ((((exists fs_h_dst_commutative_firstfoldpositive_body_steps_partial. fs_h_dst_commutative_firstfoldpositive_body_steps_partial + S (fs_r_dst_commutative_firstfoldpositive_body_steps) = S ((S (fs_i_dst_commutative_firstfoldpositive_body_steps)) * fs_v_dst_commutative_firstfoldpositive)) /\ exists fs_q_dst_commutative_firstfoldpositive_body_steps_partial. fs_u_dst_commutative_firstfoldpositive = fs_q_dst_commutative_firstfoldpositive_body_steps_partial * S ((S (fs_i_dst_commutative_firstfoldpositive_body_steps)) * fs_v_dst_commutative_firstfoldpositive) + (fs_r_dst_commutative_firstfoldpositive_body_steps))) /\ ((((exists fs_h_dst_commutative_firstfoldpositive_body_steps_successor. fs_h_dst_commutative_firstfoldpositive_body_steps_successor + S (fs_s_dst_commutative_firstfoldpositive_body_steps) = S ((S (S fs_i_dst_commutative_firstfoldpositive_body_steps)) * fs_v_dst_commutative_firstfoldpositive)) /\ exists fs_q_dst_commutative_firstfoldpositive_body_steps_successor. fs_u_dst_commutative_firstfoldpositive = fs_q_dst_commutative_firstfoldpositive_body_steps_successor * S ((S (S fs_i_dst_commutative_firstfoldpositive_body_steps)) * fs_v_dst_commutative_firstfoldpositive) + (fs_s_dst_commutative_firstfoldpositive_body_steps))) /\ fs_s_dst_commutative_firstfoldpositive_body_steps = fs_r_dst_commutative_firstfoldpositive_body_steps + fs_a_dst_commutative_firstfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_commutative_firstfoldnegative fs_v_dst_commutative_firstfoldnegative. ((((exists fs_h_dst_commutative_firstfoldnegative_body_start. fs_h_dst_commutative_firstfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_commutative_firstfoldnegative)) /\ exists fs_q_dst_commutative_firstfoldnegative_body_start. fs_u_dst_commutative_firstfoldnegative = fs_q_dst_commutative_firstfoldnegative_body_start * S ((S (0)) * fs_v_dst_commutative_firstfoldnegative) + (0))) /\ ((((exists fs_h_dst_commutative_firstfoldnegative_body_terminal. fs_h_dst_commutative_firstfoldnegative_body_terminal + S (dst_negative_sum_commutative_firstfold) = S ((S (S (n))) * fs_v_dst_commutative_firstfoldnegative)) /\ exists fs_q_dst_commutative_firstfoldnegative_body_terminal. fs_u_dst_commutative_firstfoldnegative = fs_q_dst_commutative_firstfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_commutative_firstfoldnegative) + (dst_negative_sum_commutative_firstfold))) /\ forall fs_i_dst_commutative_firstfoldnegative_body_steps. (exists fs_lt_dst_commutative_firstfoldnegative_body_steps_bound. fs_lt_dst_commutative_firstfoldnegative_body_steps_bound + S fs_i_dst_commutative_firstfoldnegative_body_steps = S (n)) -> exists fs_a_dst_commutative_firstfoldnegative_body_steps fs_r_dst_commutative_firstfoldnegative_body_steps fs_s_dst_commutative_firstfoldnegative_body_steps. ((((exists fs_h_dst_commutative_firstfoldnegative_body_steps_summand. fs_h_dst_commutative_firstfoldnegative_body_steps_summand + S (fs_a_dst_commutative_firstfoldnegative_body_steps) = S ((S (fs_i_dst_commutative_firstfoldnegative_body_steps)) * dst_negative_scale_commutative_firstfold)) /\ exists fs_q_dst_commutative_firstfoldnegative_body_steps_summand. dst_negative_code_commutative_firstfold = fs_q_dst_commutative_firstfoldnegative_body_steps_summand * S ((S (fs_i_dst_commutative_firstfoldnegative_body_steps)) * dst_negative_scale_commutative_firstfold) + (fs_a_dst_commutative_firstfoldnegative_body_steps))) /\ ((((exists fs_h_dst_commutative_firstfoldnegative_body_steps_partial. fs_h_dst_commutative_firstfoldnegative_body_steps_partial + S (fs_r_dst_commutative_firstfoldnegative_body_steps) = S ((S (fs_i_dst_commutative_firstfoldnegative_body_steps)) * fs_v_dst_commutative_firstfoldnegative)) /\ exists fs_q_dst_commutative_firstfoldnegative_body_steps_partial. fs_u_dst_commutative_firstfoldnegative = fs_q_dst_commutative_firstfoldnegative_body_steps_partial * S ((S (fs_i_dst_commutative_firstfoldnegative_body_steps)) * fs_v_dst_commutative_firstfoldnegative) + (fs_r_dst_commutative_firstfoldnegative_body_steps))) /\ ((((exists fs_h_dst_commutative_firstfoldnegative_body_steps_successor. fs_h_dst_commutative_firstfoldnegative_body_steps_successor + S (fs_s_dst_commutative_firstfoldnegative_body_steps) = S ((S (S fs_i_dst_commutative_firstfoldnegative_body_steps)) * fs_v_dst_commutative_firstfoldnegative)) /\ exists fs_q_dst_commutative_firstfoldnegative_body_steps_successor. fs_u_dst_commutative_firstfoldnegative = fs_q_dst_commutative_firstfoldnegative_body_steps_successor * S ((S (S fs_i_dst_commutative_firstfoldnegative_body_steps)) * fs_v_dst_commutative_firstfoldnegative) + (fs_s_dst_commutative_firstfoldnegative_body_steps))) /\ fs_s_dst_commutative_firstfoldnegative_body_steps = fs_r_dst_commutative_firstfoldnegative_body_steps + fs_a_dst_commutative_firstfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_commutative_firstfoldresult ge_balance_negative_commutative_firstfoldresult. (((((a) = 2 * (ge_balance_positive_commutative_firstfoldresult) /\ (ge_balance_negative_commutative_firstfoldresult) = 0) \/ exists ge_signed_half_commutative_firstfoldresultdecode. (((a) = 2 * ge_signed_half_commutative_firstfoldresultdecode + 1 /\ (ge_balance_positive_commutative_firstfoldresult) = 0) /\ (ge_balance_negative_commutative_firstfoldresult) = S ge_signed_half_commutative_firstfoldresultdecode))) /\ ((dst_positive_sum_commutative_firstfold) + ge_balance_negative_commutative_firstfoldresult = (dst_negative_sum_commutative_firstfold) + ge_balance_positive_commutative_firstfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dc_mask_commutative_second. ((((exists dst_positive_code_commutative_secondmasktable dst_positive_scale_commutative_secondmasktable dst_negative_code_commutative_secondmasktable dst_negative_scale_commutative_secondmasktable. (((dc_mask_commutative_second) = (((((dst_positive_code_commutative_secondmasktable) + (dst_positive_scale_commutative_secondmasktable)) * S ((dst_positive_code_commutative_secondmasktable) + (dst_positive_scale_commutative_secondmasktable)) + ((dst_positive_scale_commutative_secondmasktable) + (dst_positive_scale_commutative_secondmasktable))) + (((dst_negative_code_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)) * S ((dst_negative_code_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)) + ((dst_negative_scale_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)))) * S ((((dst_positive_code_commutative_secondmasktable) + (dst_positive_scale_commutative_secondmasktable)) * S ((dst_positive_code_commutative_secondmasktable) + (dst_positive_scale_commutative_secondmasktable)) + ((dst_positive_scale_commutative_secondmasktable) + (dst_positive_scale_commutative_secondmasktable))) + (((dst_negative_code_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)) * S ((dst_negative_code_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)) + ((dst_negative_scale_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)))) + ((((dst_negative_code_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)) * S ((dst_negative_code_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)) + ((dst_negative_scale_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable))) + (((dst_negative_code_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)) * S ((dst_negative_code_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)) + ((dst_negative_scale_commutative_secondmasktable) + (dst_negative_scale_commutative_secondmasktable)))))) /\ (forall dst_index_commutative_secondmasktable. (exists pvs_le_gap_commutative_secondmasktabledomain. pvs_le_gap_commutative_secondmasktabledomain + (dst_index_commutative_secondmasktable) = (n)) -> exists dst_positive_commutative_secondmasktable dst_negative_commutative_secondmasktable dst_value_commutative_secondmasktable. ((((exists ff_h_pvs_commutative_secondmasktableentrypositive. ff_h_pvs_commutative_secondmasktableentrypositive + S (dst_positive_commutative_secondmasktable) = S ((S (dst_index_commutative_secondmasktable)) * dst_positive_scale_commutative_secondmasktable)) /\ exists ff_q_pvs_commutative_secondmasktableentrypositive. dst_positive_code_commutative_secondmasktable = ff_q_pvs_commutative_secondmasktableentrypositive * S ((S (dst_index_commutative_secondmasktable)) * dst_positive_scale_commutative_secondmasktable) + (dst_positive_commutative_secondmasktable))) /\ (((((exists ff_h_pvs_commutative_secondmasktableentrynegative. ff_h_pvs_commutative_secondmasktableentrynegative + S (dst_negative_commutative_secondmasktable) = S ((S (dst_index_commutative_secondmasktable)) * dst_negative_scale_commutative_secondmasktable)) /\ exists ff_q_pvs_commutative_secondmasktableentrynegative. dst_negative_code_commutative_secondmasktable = ff_q_pvs_commutative_secondmasktableentrynegative * S ((S (dst_index_commutative_secondmasktable)) * dst_negative_scale_commutative_secondmasktable) + (dst_negative_commutative_secondmasktable))) /\ (exists ge_balance_positive_commutative_secondmasktableentryvalue ge_balance_negative_commutative_secondmasktableentryvalue. (((((dst_value_commutative_secondmasktable) = 2 * (ge_balance_positive_commutative_secondmasktableentryvalue) /\ (ge_balance_negative_commutative_secondmasktableentryvalue) = 0) \/ exists ge_signed_half_commutative_secondmasktableentryvaluedecode. (((dst_value_commutative_secondmasktable) = 2 * ge_signed_half_commutative_secondmasktableentryvaluedecode + 1 /\ (ge_balance_positive_commutative_secondmasktableentryvalue) = 0) /\ (ge_balance_negative_commutative_secondmasktableentryvalue) = S ge_signed_half_commutative_secondmasktableentryvaluedecode))) /\ ((dst_positive_commutative_secondmasktable) + ge_balance_negative_commutative_secondmasktableentryvalue = (dst_negative_commutative_secondmasktable) + ge_balance_positive_commutative_secondmasktableentryvalue))))))))) /\ (forall dc_index_commutative_secondmask dc_value_commutative_secondmask. (exists pvs_le_gap_commutative_secondmaskdomain. pvs_le_gap_commutative_secondmaskdomain + (dc_index_commutative_secondmask) = (n)) -> (exists dst_positive_code_commutative_secondmasklookup dst_positive_scale_commutative_secondmasklookup dst_negative_code_commutative_secondmasklookup dst_negative_scale_commutative_secondmasklookup dst_positive_commutative_secondmasklookup dst_negative_commutative_secondmasklookup. (((dc_mask_commutative_second) = (((((dst_positive_code_commutative_secondmasklookup) + (dst_positive_scale_commutative_secondmasklookup)) * S ((dst_positive_code_commutative_secondmasklookup) + (dst_positive_scale_commutative_secondmasklookup)) + ((dst_positive_scale_commutative_secondmasklookup) + (dst_positive_scale_commutative_secondmasklookup))) + (((dst_negative_code_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)) * S ((dst_negative_code_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)) + ((dst_negative_scale_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)))) * S ((((dst_positive_code_commutative_secondmasklookup) + (dst_positive_scale_commutative_secondmasklookup)) * S ((dst_positive_code_commutative_secondmasklookup) + (dst_positive_scale_commutative_secondmasklookup)) + ((dst_positive_scale_commutative_secondmasklookup) + (dst_positive_scale_commutative_secondmasklookup))) + (((dst_negative_code_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)) * S ((dst_negative_code_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)) + ((dst_negative_scale_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)))) + ((((dst_negative_code_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)) * S ((dst_negative_code_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)) + ((dst_negative_scale_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup))) + (((dst_negative_code_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)) * S ((dst_negative_code_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)) + ((dst_negative_scale_commutative_secondmasklookup) + (dst_negative_scale_commutative_secondmasklookup)))))) /\ (((((exists ff_h_pvs_commutative_secondmasklookuppositive. ff_h_pvs_commutative_secondmasklookuppositive + S (dst_positive_commutative_secondmasklookup) = S ((S (dc_index_commutative_secondmask)) * dst_positive_scale_commutative_secondmasklookup)) /\ exists ff_q_pvs_commutative_secondmasklookuppositive. dst_positive_code_commutative_secondmasklookup = ff_q_pvs_commutative_secondmasklookuppositive * S ((S (dc_index_commutative_secondmask)) * dst_positive_scale_commutative_secondmasklookup) + (dst_positive_commutative_secondmasklookup))) /\ (((((exists ff_h_pvs_commutative_secondmasklookupnegative. ff_h_pvs_commutative_secondmasklookupnegative + S (dst_negative_commutative_secondmasklookup) = S ((S (dc_index_commutative_secondmask)) * dst_negative_scale_commutative_secondmasklookup)) /\ exists ff_q_pvs_commutative_secondmasklookupnegative. dst_negative_code_commutative_secondmasklookup = ff_q_pvs_commutative_secondmasklookupnegative * S ((S (dc_index_commutative_secondmask)) * dst_negative_scale_commutative_secondmasklookup) + (dst_negative_commutative_secondmasklookup))) /\ (exists ge_balance_positive_commutative_secondmasklookupvalue ge_balance_negative_commutative_secondmasklookupvalue. (((((dc_value_commutative_secondmask) = 2 * (ge_balance_positive_commutative_secondmasklookupvalue) /\ (ge_balance_negative_commutative_secondmasklookupvalue) = 0) \/ exists ge_signed_half_commutative_secondmasklookupvaluedecode. (((dc_value_commutative_secondmask) = 2 * ge_signed_half_commutative_secondmasklookupvaluedecode + 1 /\ (ge_balance_positive_commutative_secondmasklookupvalue) = 0) /\ (ge_balance_negative_commutative_secondmasklookupvalue) = S ge_signed_half_commutative_secondmasklookupvaluedecode))) /\ ((dst_positive_commutative_secondmasklookup) + ge_balance_negative_commutative_secondmasklookupvalue = (dst_negative_commutative_secondmasklookup) + ge_balance_positive_commutative_secondmasklookupvalue))))))))) -> ((((~((dc_index_commutative_secondmask)=0)) /\ (exists dc_quotient_commutative_secondmaskentry dc_left_commutative_secondmaskentry dc_right_commutative_secondmaskentry. (((n)=(dc_index_commutative_secondmask)*dc_quotient_commutative_secondmaskentry) /\ (((exists dst_positive_code_commutative_secondmaskentryleft dst_positive_scale_commutative_secondmaskentryleft dst_negative_code_commutative_secondmaskentryleft dst_negative_scale_commutative_secondmaskentryleft dst_positive_commutative_secondmaskentryleft dst_negative_commutative_secondmaskentryleft. (((G) = (((((dst_positive_code_commutative_secondmaskentryleft) + (dst_positive_scale_commutative_secondmaskentryleft)) * S ((dst_positive_code_commutative_secondmaskentryleft) + (dst_positive_scale_commutative_secondmaskentryleft)) + ((dst_positive_scale_commutative_secondmaskentryleft) + (dst_positive_scale_commutative_secondmaskentryleft))) + (((dst_negative_code_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)) * S ((dst_negative_code_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)) + ((dst_negative_scale_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)))) * S ((((dst_positive_code_commutative_secondmaskentryleft) + (dst_positive_scale_commutative_secondmaskentryleft)) * S ((dst_positive_code_commutative_secondmaskentryleft) + (dst_positive_scale_commutative_secondmaskentryleft)) + ((dst_positive_scale_commutative_secondmaskentryleft) + (dst_positive_scale_commutative_secondmaskentryleft))) + (((dst_negative_code_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)) * S ((dst_negative_code_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)) + ((dst_negative_scale_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)))) + ((((dst_negative_code_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)) * S ((dst_negative_code_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)) + ((dst_negative_scale_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft))) + (((dst_negative_code_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)) * S ((dst_negative_code_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)) + ((dst_negative_scale_commutative_secondmaskentryleft) + (dst_negative_scale_commutative_secondmaskentryleft)))))) /\ (((((exists ff_h_pvs_commutative_secondmaskentryleftpositive. ff_h_pvs_commutative_secondmaskentryleftpositive + S (dst_positive_commutative_secondmaskentryleft) = S ((S (dc_index_commutative_secondmask)) * dst_positive_scale_commutative_secondmaskentryleft)) /\ exists ff_q_pvs_commutative_secondmaskentryleftpositive. dst_positive_code_commutative_secondmaskentryleft = ff_q_pvs_commutative_secondmaskentryleftpositive * S ((S (dc_index_commutative_secondmask)) * dst_positive_scale_commutative_secondmaskentryleft) + (dst_positive_commutative_secondmaskentryleft))) /\ (((((exists ff_h_pvs_commutative_secondmaskentryleftnegative. ff_h_pvs_commutative_secondmaskentryleftnegative + S (dst_negative_commutative_secondmaskentryleft) = S ((S (dc_index_commutative_secondmask)) * dst_negative_scale_commutative_secondmaskentryleft)) /\ exists ff_q_pvs_commutative_secondmaskentryleftnegative. dst_negative_code_commutative_secondmaskentryleft = ff_q_pvs_commutative_secondmaskentryleftnegative * S ((S (dc_index_commutative_secondmask)) * dst_negative_scale_commutative_secondmaskentryleft) + (dst_negative_commutative_secondmaskentryleft))) /\ (exists ge_balance_positive_commutative_secondmaskentryleftvalue ge_balance_negative_commutative_secondmaskentryleftvalue. (((((dc_left_commutative_secondmaskentry) = 2 * (ge_balance_positive_commutative_secondmaskentryleftvalue) /\ (ge_balance_negative_commutative_secondmaskentryleftvalue) = 0) \/ exists ge_signed_half_commutative_secondmaskentryleftvaluedecode. (((dc_left_commutative_secondmaskentry) = 2 * ge_signed_half_commutative_secondmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_commutative_secondmaskentryleftvalue) = 0) /\ (ge_balance_negative_commutative_secondmaskentryleftvalue) = S ge_signed_half_commutative_secondmaskentryleftvaluedecode))) /\ ((dst_positive_commutative_secondmaskentryleft) + ge_balance_negative_commutative_secondmaskentryleftvalue = (dst_negative_commutative_secondmaskentryleft) + ge_balance_positive_commutative_secondmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_commutative_secondmaskentryright dst_positive_scale_commutative_secondmaskentryright dst_negative_code_commutative_secondmaskentryright dst_negative_scale_commutative_secondmaskentryright dst_positive_commutative_secondmaskentryright dst_negative_commutative_secondmaskentryright. (((F) = (((((dst_positive_code_commutative_secondmaskentryright) + (dst_positive_scale_commutative_secondmaskentryright)) * S ((dst_positive_code_commutative_secondmaskentryright) + (dst_positive_scale_commutative_secondmaskentryright)) + ((dst_positive_scale_commutative_secondmaskentryright) + (dst_positive_scale_commutative_secondmaskentryright))) + (((dst_negative_code_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)) * S ((dst_negative_code_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)) + ((dst_negative_scale_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)))) * S ((((dst_positive_code_commutative_secondmaskentryright) + (dst_positive_scale_commutative_secondmaskentryright)) * S ((dst_positive_code_commutative_secondmaskentryright) + (dst_positive_scale_commutative_secondmaskentryright)) + ((dst_positive_scale_commutative_secondmaskentryright) + (dst_positive_scale_commutative_secondmaskentryright))) + (((dst_negative_code_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)) * S ((dst_negative_code_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)) + ((dst_negative_scale_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)))) + ((((dst_negative_code_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)) * S ((dst_negative_code_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)) + ((dst_negative_scale_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright))) + (((dst_negative_code_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)) * S ((dst_negative_code_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)) + ((dst_negative_scale_commutative_secondmaskentryright) + (dst_negative_scale_commutative_secondmaskentryright)))))) /\ (((((exists ff_h_pvs_commutative_secondmaskentryrightpositive. ff_h_pvs_commutative_secondmaskentryrightpositive + S (dst_positive_commutative_secondmaskentryright) = S ((S (dc_quotient_commutative_secondmaskentry)) * dst_positive_scale_commutative_secondmaskentryright)) /\ exists ff_q_pvs_commutative_secondmaskentryrightpositive. dst_positive_code_commutative_secondmaskentryright = ff_q_pvs_commutative_secondmaskentryrightpositive * S ((S (dc_quotient_commutative_secondmaskentry)) * dst_positive_scale_commutative_secondmaskentryright) + (dst_positive_commutative_secondmaskentryright))) /\ (((((exists ff_h_pvs_commutative_secondmaskentryrightnegative. ff_h_pvs_commutative_secondmaskentryrightnegative + S (dst_negative_commutative_secondmaskentryright) = S ((S (dc_quotient_commutative_secondmaskentry)) * dst_negative_scale_commutative_secondmaskentryright)) /\ exists ff_q_pvs_commutative_secondmaskentryrightnegative. dst_negative_code_commutative_secondmaskentryright = ff_q_pvs_commutative_secondmaskentryrightnegative * S ((S (dc_quotient_commutative_secondmaskentry)) * dst_negative_scale_commutative_secondmaskentryright) + (dst_negative_commutative_secondmaskentryright))) /\ (exists ge_balance_positive_commutative_secondmaskentryrightvalue ge_balance_negative_commutative_secondmaskentryrightvalue. (((((dc_right_commutative_secondmaskentry) = 2 * (ge_balance_positive_commutative_secondmaskentryrightvalue) /\ (ge_balance_negative_commutative_secondmaskentryrightvalue) = 0) \/ exists ge_signed_half_commutative_secondmaskentryrightvaluedecode. (((dc_right_commutative_secondmaskentry) = 2 * ge_signed_half_commutative_secondmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_commutative_secondmaskentryrightvalue) = 0) /\ (ge_balance_negative_commutative_secondmaskentryrightvalue) = S ge_signed_half_commutative_secondmaskentryrightvaluedecode))) /\ ((dst_positive_commutative_secondmaskentryright) + ge_balance_negative_commutative_secondmaskentryrightvalue = (dst_negative_commutative_secondmaskentryright) + ge_balance_positive_commutative_secondmaskentryrightvalue))))))))) /\ (exists sto_ap_commutative_secondmaskentryproduct sto_an_commutative_secondmaskentryproduct sto_bp_commutative_secondmaskentryproduct sto_bn_commutative_secondmaskentryproduct sto_cp_commutative_secondmaskentryproduct sto_cn_commutative_secondmaskentryproduct. (((((dc_left_commutative_secondmaskentry) = 2 * (sto_ap_commutative_secondmaskentryproduct) /\ (sto_an_commutative_secondmaskentryproduct) = 0) \/ exists ge_signed_half_commutative_secondmaskentryproductleft. (((dc_left_commutative_secondmaskentry) = 2 * ge_signed_half_commutative_secondmaskentryproductleft + 1 /\ (sto_ap_commutative_secondmaskentryproduct) = 0) /\ (sto_an_commutative_secondmaskentryproduct) = S ge_signed_half_commutative_secondmaskentryproductleft))) /\ ((((((dc_right_commutative_secondmaskentry) = 2 * (sto_bp_commutative_secondmaskentryproduct) /\ (sto_bn_commutative_secondmaskentryproduct) = 0) \/ exists ge_signed_half_commutative_secondmaskentryproductright. (((dc_right_commutative_secondmaskentry) = 2 * ge_signed_half_commutative_secondmaskentryproductright + 1 /\ (sto_bp_commutative_secondmaskentryproduct) = 0) /\ (sto_bn_commutative_secondmaskentryproduct) = S ge_signed_half_commutative_secondmaskentryproductright))) /\ ((((((dc_value_commutative_secondmask) = 2 * (sto_cp_commutative_secondmaskentryproduct) /\ (sto_cn_commutative_secondmaskentryproduct) = 0) \/ exists ge_signed_half_commutative_secondmaskentryproductoutput. (((dc_value_commutative_secondmask) = 2 * ge_signed_half_commutative_secondmaskentryproductoutput + 1 /\ (sto_cp_commutative_secondmaskentryproduct) = 0) /\ (sto_cn_commutative_secondmaskentryproduct) = S ge_signed_half_commutative_secondmaskentryproductoutput))) /\ ((sto_ap_commutative_secondmaskentryproduct * sto_bp_commutative_secondmaskentryproduct + sto_an_commutative_secondmaskentryproduct * sto_bn_commutative_secondmaskentryproduct) + sto_cn_commutative_secondmaskentryproduct = (sto_ap_commutative_secondmaskentryproduct * sto_bn_commutative_secondmaskentryproduct + sto_an_commutative_secondmaskentryproduct * sto_bp_commutative_secondmaskentryproduct) + sto_cp_commutative_secondmaskentryproduct))))))))))))))) \/ ((((dc_index_commutative_secondmask)=0 \/ ~(exists pvs_factor_commutative_secondmaskentrynondivisor. (n) = (dc_index_commutative_secondmask) * pvs_factor_commutative_secondmaskentrynondivisor)) /\ ((dc_value_commutative_secondmask)=0))))))) /\ (exists dst_positive_code_commutative_secondfold dst_positive_scale_commutative_secondfold dst_negative_code_commutative_secondfold dst_negative_scale_commutative_secondfold dst_positive_sum_commutative_secondfold dst_negative_sum_commutative_secondfold. (((dc_mask_commutative_second) = (((((dst_positive_code_commutative_secondfold) + (dst_positive_scale_commutative_secondfold)) * S ((dst_positive_code_commutative_secondfold) + (dst_positive_scale_commutative_secondfold)) + ((dst_positive_scale_commutative_secondfold) + (dst_positive_scale_commutative_secondfold))) + (((dst_negative_code_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)) * S ((dst_negative_code_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)) + ((dst_negative_scale_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)))) * S ((((dst_positive_code_commutative_secondfold) + (dst_positive_scale_commutative_secondfold)) * S ((dst_positive_code_commutative_secondfold) + (dst_positive_scale_commutative_secondfold)) + ((dst_positive_scale_commutative_secondfold) + (dst_positive_scale_commutative_secondfold))) + (((dst_negative_code_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)) * S ((dst_negative_code_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)) + ((dst_negative_scale_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)))) + ((((dst_negative_code_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)) * S ((dst_negative_code_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)) + ((dst_negative_scale_commutative_secondfold) + (dst_negative_scale_commutative_secondfold))) + (((dst_negative_code_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)) * S ((dst_negative_code_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)) + ((dst_negative_scale_commutative_secondfold) + (dst_negative_scale_commutative_secondfold)))))) /\ (((exists fs_u_dst_commutative_secondfoldpositive fs_v_dst_commutative_secondfoldpositive. ((((exists fs_h_dst_commutative_secondfoldpositive_body_start. fs_h_dst_commutative_secondfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_commutative_secondfoldpositive)) /\ exists fs_q_dst_commutative_secondfoldpositive_body_start. fs_u_dst_commutative_secondfoldpositive = fs_q_dst_commutative_secondfoldpositive_body_start * S ((S (0)) * fs_v_dst_commutative_secondfoldpositive) + (0))) /\ ((((exists fs_h_dst_commutative_secondfoldpositive_body_terminal. fs_h_dst_commutative_secondfoldpositive_body_terminal + S (dst_positive_sum_commutative_secondfold) = S ((S (S (n))) * fs_v_dst_commutative_secondfoldpositive)) /\ exists fs_q_dst_commutative_secondfoldpositive_body_terminal. fs_u_dst_commutative_secondfoldpositive = fs_q_dst_commutative_secondfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_commutative_secondfoldpositive) + (dst_positive_sum_commutative_secondfold))) /\ forall fs_i_dst_commutative_secondfoldpositive_body_steps. (exists fs_lt_dst_commutative_secondfoldpositive_body_steps_bound. fs_lt_dst_commutative_secondfoldpositive_body_steps_bound + S fs_i_dst_commutative_secondfoldpositive_body_steps = S (n)) -> exists fs_a_dst_commutative_secondfoldpositive_body_steps fs_r_dst_commutative_secondfoldpositive_body_steps fs_s_dst_commutative_secondfoldpositive_body_steps. ((((exists fs_h_dst_commutative_secondfoldpositive_body_steps_summand. fs_h_dst_commutative_secondfoldpositive_body_steps_summand + S (fs_a_dst_commutative_secondfoldpositive_body_steps) = S ((S (fs_i_dst_commutative_secondfoldpositive_body_steps)) * dst_positive_scale_commutative_secondfold)) /\ exists fs_q_dst_commutative_secondfoldpositive_body_steps_summand. dst_positive_code_commutative_secondfold = fs_q_dst_commutative_secondfoldpositive_body_steps_summand * S ((S (fs_i_dst_commutative_secondfoldpositive_body_steps)) * dst_positive_scale_commutative_secondfold) + (fs_a_dst_commutative_secondfoldpositive_body_steps))) /\ ((((exists fs_h_dst_commutative_secondfoldpositive_body_steps_partial. fs_h_dst_commutative_secondfoldpositive_body_steps_partial + S (fs_r_dst_commutative_secondfoldpositive_body_steps) = S ((S (fs_i_dst_commutative_secondfoldpositive_body_steps)) * fs_v_dst_commutative_secondfoldpositive)) /\ exists fs_q_dst_commutative_secondfoldpositive_body_steps_partial. fs_u_dst_commutative_secondfoldpositive = fs_q_dst_commutative_secondfoldpositive_body_steps_partial * S ((S (fs_i_dst_commutative_secondfoldpositive_body_steps)) * fs_v_dst_commutative_secondfoldpositive) + (fs_r_dst_commutative_secondfoldpositive_body_steps))) /\ ((((exists fs_h_dst_commutative_secondfoldpositive_body_steps_successor. fs_h_dst_commutative_secondfoldpositive_body_steps_successor + S (fs_s_dst_commutative_secondfoldpositive_body_steps) = S ((S (S fs_i_dst_commutative_secondfoldpositive_body_steps)) * fs_v_dst_commutative_secondfoldpositive)) /\ exists fs_q_dst_commutative_secondfoldpositive_body_steps_successor. fs_u_dst_commutative_secondfoldpositive = fs_q_dst_commutative_secondfoldpositive_body_steps_successor * S ((S (S fs_i_dst_commutative_secondfoldpositive_body_steps)) * fs_v_dst_commutative_secondfoldpositive) + (fs_s_dst_commutative_secondfoldpositive_body_steps))) /\ fs_s_dst_commutative_secondfoldpositive_body_steps = fs_r_dst_commutative_secondfoldpositive_body_steps + fs_a_dst_commutative_secondfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_commutative_secondfoldnegative fs_v_dst_commutative_secondfoldnegative. ((((exists fs_h_dst_commutative_secondfoldnegative_body_start. fs_h_dst_commutative_secondfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_commutative_secondfoldnegative)) /\ exists fs_q_dst_commutative_secondfoldnegative_body_start. fs_u_dst_commutative_secondfoldnegative = fs_q_dst_commutative_secondfoldnegative_body_start * S ((S (0)) * fs_v_dst_commutative_secondfoldnegative) + (0))) /\ ((((exists fs_h_dst_commutative_secondfoldnegative_body_terminal. fs_h_dst_commutative_secondfoldnegative_body_terminal + S (dst_negative_sum_commutative_secondfold) = S ((S (S (n))) * fs_v_dst_commutative_secondfoldnegative)) /\ exists fs_q_dst_commutative_secondfoldnegative_body_terminal. fs_u_dst_commutative_secondfoldnegative = fs_q_dst_commutative_secondfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_commutative_secondfoldnegative) + (dst_negative_sum_commutative_secondfold))) /\ forall fs_i_dst_commutative_secondfoldnegative_body_steps. (exists fs_lt_dst_commutative_secondfoldnegative_body_steps_bound. fs_lt_dst_commutative_secondfoldnegative_body_steps_bound + S fs_i_dst_commutative_secondfoldnegative_body_steps = S (n)) -> exists fs_a_dst_commutative_secondfoldnegative_body_steps fs_r_dst_commutative_secondfoldnegative_body_steps fs_s_dst_commutative_secondfoldnegative_body_steps. ((((exists fs_h_dst_commutative_secondfoldnegative_body_steps_summand. fs_h_dst_commutative_secondfoldnegative_body_steps_summand + S (fs_a_dst_commutative_secondfoldnegative_body_steps) = S ((S (fs_i_dst_commutative_secondfoldnegative_body_steps)) * dst_negative_scale_commutative_secondfold)) /\ exists fs_q_dst_commutative_secondfoldnegative_body_steps_summand. dst_negative_code_commutative_secondfold = fs_q_dst_commutative_secondfoldnegative_body_steps_summand * S ((S (fs_i_dst_commutative_secondfoldnegative_body_steps)) * dst_negative_scale_commutative_secondfold) + (fs_a_dst_commutative_secondfoldnegative_body_steps))) /\ ((((exists fs_h_dst_commutative_secondfoldnegative_body_steps_partial. fs_h_dst_commutative_secondfoldnegative_body_steps_partial + S (fs_r_dst_commutative_secondfoldnegative_body_steps) = S ((S (fs_i_dst_commutative_secondfoldnegative_body_steps)) * fs_v_dst_commutative_secondfoldnegative)) /\ exists fs_q_dst_commutative_secondfoldnegative_body_steps_partial. fs_u_dst_commutative_secondfoldnegative = fs_q_dst_commutative_secondfoldnegative_body_steps_partial * S ((S (fs_i_dst_commutative_secondfoldnegative_body_steps)) * fs_v_dst_commutative_secondfoldnegative) + (fs_r_dst_commutative_secondfoldnegative_body_steps))) /\ ((((exists fs_h_dst_commutative_secondfoldnegative_body_steps_successor. fs_h_dst_commutative_secondfoldnegative_body_steps_successor + S (fs_s_dst_commutative_secondfoldnegative_body_steps) = S ((S (S fs_i_dst_commutative_secondfoldnegative_body_steps)) * fs_v_dst_commutative_secondfoldnegative)) /\ exists fs_q_dst_commutative_secondfoldnegative_body_steps_successor. fs_u_dst_commutative_secondfoldnegative = fs_q_dst_commutative_secondfoldnegative_body_steps_successor * S ((S (S fs_i_dst_commutative_secondfoldnegative_body_steps)) * fs_v_dst_commutative_secondfoldnegative) + (fs_s_dst_commutative_secondfoldnegative_body_steps))) /\ fs_s_dst_commutative_secondfoldnegative_body_steps = fs_r_dst_commutative_secondfoldnegative_body_steps + fs_a_dst_commutative_secondfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_commutative_secondfoldresult ge_balance_negative_commutative_secondfoldresult. (((((b) = 2 * (ge_balance_positive_commutative_secondfoldresult) /\ (ge_balance_negative_commutative_secondfoldresult) = 0) \/ exists ge_signed_half_commutative_secondfoldresultdecode. (((b) = 2 * ge_signed_half_commutative_secondfoldresultdecode + 1 /\ (ge_balance_positive_commutative_secondfoldresult) = 0) /\ (ge_balance_negative_commutative_secondfoldresult) = S ge_signed_half_commutative_secondfoldresultdecode))) /\ ((dst_positive_sum_commutative_secondfold) + ge_balance_negative_commutative_secondfoldresult = (dst_negative_sum_commutative_secondfold) + ge_balance_positive_commutative_secondfoldresult))))))))))))) -> a=b