dirichlet_convolution_prefix_quotient_entry

Exact expanded first-order arithmetic statement

forall F G n l M d q a b z. (((exists dst_positive_code_keep_prefixtable dst_positive_scale_keep_prefixtable dst_negative_code_keep_prefixtable dst_negative_scale_keep_prefixtable. (((M) = (((((dst_positive_code_keep_prefixtable) + (dst_positive_scale_keep_prefixtable)) * S ((dst_positive_code_keep_prefixtable) + (dst_positive_scale_keep_prefixtable)) + ((dst_positive_scale_keep_prefixtable) + (dst_positive_scale_keep_prefixtable))) + (((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) * S ((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) + ((dst_negative_scale_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)))) * S ((((dst_positive_code_keep_prefixtable) + (dst_positive_scale_keep_prefixtable)) * S ((dst_positive_code_keep_prefixtable) + (dst_positive_scale_keep_prefixtable)) + ((dst_positive_scale_keep_prefixtable) + (dst_positive_scale_keep_prefixtable))) + (((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) * S ((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) + ((dst_negative_scale_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)))) + ((((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) * S ((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) + ((dst_negative_scale_keep_prefixtable) + (dst_negative_scale_keep_prefixtable))) + (((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) * S ((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) + ((dst_negative_scale_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)))))) /\ (forall dst_index_keep_prefixtable. (exists pvs_le_gap_keep_prefixtabledomain. pvs_le_gap_keep_prefixtabledomain + (dst_index_keep_prefixtable) = (l)) -> exists dst_positive_keep_prefixtable dst_negative_keep_prefixtable dst_value_keep_prefixtable. ((((exists ff_h_pvs_keep_prefixtableentrypositive. ff_h_pvs_keep_prefixtableentrypositive + S (dst_positive_keep_prefixtable) = S ((S (dst_index_keep_prefixtable)) * dst_positive_scale_keep_prefixtable)) /\ exists ff_q_pvs_keep_prefixtableentrypositive. dst_positive_code_keep_prefixtable = ff_q_pvs_keep_prefixtableentrypositive * S ((S (dst_index_keep_prefixtable)) * dst_positive_scale_keep_prefixtable) + (dst_positive_keep_prefixtable))) /\ (((((exists ff_h_pvs_keep_prefixtableentrynegative. ff_h_pvs_keep_prefixtableentrynegative + S (dst_negative_keep_prefixtable) = S ((S (dst_index_keep_prefixtable)) * dst_negative_scale_keep_prefixtable)) /\ exists ff_q_pvs_keep_prefixtableentrynegative. dst_negative_code_keep_prefixtable = ff_q_pvs_keep_prefixtableentrynegative * S ((S (dst_index_keep_prefixtable)) * dst_negative_scale_keep_prefixtable) + (dst_negative_keep_prefixtable))) /\ (exists ge_balance_positive_keep_prefixtableentryvalue ge_balance_negative_keep_prefixtableentryvalue. (((((dst_value_keep_prefixtable) = 2 * (ge_balance_positive_keep_prefixtableentryvalue) /\ (ge_balance_negative_keep_prefixtableentryvalue) = 0) \/ exists ge_signed_half_keep_prefixtableentryvaluedecode. (((dst_value_keep_prefixtable) = 2 * ge_signed_half_keep_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_keep_prefixtableentryvalue) = 0) /\ (ge_balance_negative_keep_prefixtableentryvalue) = S ge_signed_half_keep_prefixtableentryvaluedecode))) /\ ((dst_positive_keep_prefixtable) + ge_balance_negative_keep_prefixtableentryvalue = (dst_negative_keep_prefixtable) + ge_balance_positive_keep_prefixtableentryvalue))))))))) /\ (forall dc_index_keep_prefix dc_value_keep_prefix. (exists pvs_le_gap_keep_prefixdomain. pvs_le_gap_keep_prefixdomain + (dc_index_keep_prefix) = (l)) -> (exists dst_positive_code_keep_prefixlookup dst_positive_scale_keep_prefixlookup dst_negative_code_keep_prefixlookup dst_negative_scale_keep_prefixlookup dst_positive_keep_prefixlookup dst_negative_keep_prefixlookup. (((M) = (((((dst_positive_code_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup)) * S ((dst_positive_code_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup)) + ((dst_positive_scale_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup))) + (((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) * S ((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) + ((dst_negative_scale_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)))) * S ((((dst_positive_code_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup)) * S ((dst_positive_code_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup)) + ((dst_positive_scale_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup))) + (((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) * S ((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) + ((dst_negative_scale_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)))) + ((((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) * S ((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) + ((dst_negative_scale_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup))) + (((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) * S ((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) + ((dst_negative_scale_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)))))) /\ (((((exists ff_h_pvs_keep_prefixlookuppositive. ff_h_pvs_keep_prefixlookuppositive + S (dst_positive_keep_prefixlookup) = S ((S (dc_index_keep_prefix)) * dst_positive_scale_keep_prefixlookup)) /\ exists ff_q_pvs_keep_prefixlookuppositive. dst_positive_code_keep_prefixlookup = ff_q_pvs_keep_prefixlookuppositive * S ((S (dc_index_keep_prefix)) * dst_positive_scale_keep_prefixlookup) + (dst_positive_keep_prefixlookup))) /\ (((((exists ff_h_pvs_keep_prefixlookupnegative. ff_h_pvs_keep_prefixlookupnegative + S (dst_negative_keep_prefixlookup) = S ((S (dc_index_keep_prefix)) * dst_negative_scale_keep_prefixlookup)) /\ exists ff_q_pvs_keep_prefixlookupnegative. dst_negative_code_keep_prefixlookup = ff_q_pvs_keep_prefixlookupnegative * S ((S (dc_index_keep_prefix)) * dst_negative_scale_keep_prefixlookup) + (dst_negative_keep_prefixlookup))) /\ (exists ge_balance_positive_keep_prefixlookupvalue ge_balance_negative_keep_prefixlookupvalue. (((((dc_value_keep_prefix) = 2 * (ge_balance_positive_keep_prefixlookupvalue) /\ (ge_balance_negative_keep_prefixlookupvalue) = 0) \/ exists ge_signed_half_keep_prefixlookupvaluedecode. (((dc_value_keep_prefix) = 2 * ge_signed_half_keep_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_keep_prefixlookupvalue) = 0) /\ (ge_balance_negative_keep_prefixlookupvalue) = S ge_signed_half_keep_prefixlookupvaluedecode))) /\ ((dst_positive_keep_prefixlookup) + ge_balance_negative_keep_prefixlookupvalue = (dst_negative_keep_prefixlookup) + ge_balance_positive_keep_prefixlookupvalue))))))))) -> ((((~((dc_index_keep_prefix)=0)) /\ (exists dc_quotient_keep_prefixentry dc_left_keep_prefixentry dc_right_keep_prefixentry. (((n)=(dc_index_keep_prefix)*dc_quotient_keep_prefixentry) /\ (((exists dst_positive_code_keep_prefixentryleft dst_positive_scale_keep_prefixentryleft dst_negative_code_keep_prefixentryleft dst_negative_scale_keep_prefixentryleft dst_positive_keep_prefixentryleft dst_negative_keep_prefixentryleft. (((F) = (((((dst_positive_code_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft)) * S ((dst_positive_code_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft)) + ((dst_positive_scale_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft))) + (((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) * S ((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) + ((dst_negative_scale_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)))) * S ((((dst_positive_code_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft)) * S ((dst_positive_code_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft)) + ((dst_positive_scale_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft))) + (((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) * S ((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) + ((dst_negative_scale_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)))) + ((((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) * S ((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) + ((dst_negative_scale_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft))) + (((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) * S ((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) + ((dst_negative_scale_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)))))) /\ (((((exists ff_h_pvs_keep_prefixentryleftpositive. ff_h_pvs_keep_prefixentryleftpositive + S (dst_positive_keep_prefixentryleft) = S ((S (dc_index_keep_prefix)) * dst_positive_scale_keep_prefixentryleft)) /\ exists ff_q_pvs_keep_prefixentryleftpositive. dst_positive_code_keep_prefixentryleft = ff_q_pvs_keep_prefixentryleftpositive * S ((S (dc_index_keep_prefix)) * dst_positive_scale_keep_prefixentryleft) + (dst_positive_keep_prefixentryleft))) /\ (((((exists ff_h_pvs_keep_prefixentryleftnegative. ff_h_pvs_keep_prefixentryleftnegative + S (dst_negative_keep_prefixentryleft) = S ((S (dc_index_keep_prefix)) * dst_negative_scale_keep_prefixentryleft)) /\ exists ff_q_pvs_keep_prefixentryleftnegative. dst_negative_code_keep_prefixentryleft = ff_q_pvs_keep_prefixentryleftnegative * S ((S (dc_index_keep_prefix)) * dst_negative_scale_keep_prefixentryleft) + (dst_negative_keep_prefixentryleft))) /\ (exists ge_balance_positive_keep_prefixentryleftvalue ge_balance_negative_keep_prefixentryleftvalue. (((((dc_left_keep_prefixentry) = 2 * (ge_balance_positive_keep_prefixentryleftvalue) /\ (ge_balance_negative_keep_prefixentryleftvalue) = 0) \/ exists ge_signed_half_keep_prefixentryleftvaluedecode. (((dc_left_keep_prefixentry) = 2 * ge_signed_half_keep_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_keep_prefixentryleftvalue) = 0) /\ (ge_balance_negative_keep_prefixentryleftvalue) = S ge_signed_half_keep_prefixentryleftvaluedecode))) /\ ((dst_positive_keep_prefixentryleft) + ge_balance_negative_keep_prefixentryleftvalue = (dst_negative_keep_prefixentryleft) + ge_balance_positive_keep_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_keep_prefixentryright dst_positive_scale_keep_prefixentryright dst_negative_code_keep_prefixentryright dst_negative_scale_keep_prefixentryright dst_positive_keep_prefixentryright dst_negative_keep_prefixentryright. (((G) = (((((dst_positive_code_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright)) * S ((dst_positive_code_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright)) + ((dst_positive_scale_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright))) + (((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) * S ((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) + ((dst_negative_scale_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)))) * S ((((dst_positive_code_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright)) * S ((dst_positive_code_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright)) + ((dst_positive_scale_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright))) + (((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) * S ((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) + ((dst_negative_scale_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)))) + ((((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) * S ((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) + ((dst_negative_scale_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright))) + (((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) * S ((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) + ((dst_negative_scale_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)))))) /\ (((((exists ff_h_pvs_keep_prefixentryrightpositive. ff_h_pvs_keep_prefixentryrightpositive + S (dst_positive_keep_prefixentryright) = S ((S (dc_quotient_keep_prefixentry)) * dst_positive_scale_keep_prefixentryright)) /\ exists ff_q_pvs_keep_prefixentryrightpositive. dst_positive_code_keep_prefixentryright = ff_q_pvs_keep_prefixentryrightpositive * S ((S (dc_quotient_keep_prefixentry)) * dst_positive_scale_keep_prefixentryright) + (dst_positive_keep_prefixentryright))) /\ (((((exists ff_h_pvs_keep_prefixentryrightnegative. ff_h_pvs_keep_prefixentryrightnegative + S (dst_negative_keep_prefixentryright) = S ((S (dc_quotient_keep_prefixentry)) * dst_negative_scale_keep_prefixentryright)) /\ exists ff_q_pvs_keep_prefixentryrightnegative. dst_negative_code_keep_prefixentryright = ff_q_pvs_keep_prefixentryrightnegative * S ((S (dc_quotient_keep_prefixentry)) * dst_negative_scale_keep_prefixentryright) + (dst_negative_keep_prefixentryright))) /\ (exists ge_balance_positive_keep_prefixentryrightvalue ge_balance_negative_keep_prefixentryrightvalue. (((((dc_right_keep_prefixentry) = 2 * (ge_balance_positive_keep_prefixentryrightvalue) /\ (ge_balance_negative_keep_prefixentryrightvalue) = 0) \/ exists ge_signed_half_keep_prefixentryrightvaluedecode. (((dc_right_keep_prefixentry) = 2 * ge_signed_half_keep_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_keep_prefixentryrightvalue) = 0) /\ (ge_balance_negative_keep_prefixentryrightvalue) = S ge_signed_half_keep_prefixentryrightvaluedecode))) /\ ((dst_positive_keep_prefixentryright) + ge_balance_negative_keep_prefixentryrightvalue = (dst_negative_keep_prefixentryright) + ge_balance_positive_keep_prefixentryrightvalue))))))))) /\ (exists sto_ap_keep_prefixentryproduct sto_an_keep_prefixentryproduct sto_bp_keep_prefixentryproduct sto_bn_keep_prefixentryproduct sto_cp_keep_prefixentryproduct sto_cn_keep_prefixentryproduct. (((((dc_left_keep_prefixentry) = 2 * (sto_ap_keep_prefixentryproduct) /\ (sto_an_keep_prefixentryproduct) = 0) \/ exists ge_signed_half_keep_prefixentryproductleft. (((dc_left_keep_prefixentry) = 2 * ge_signed_half_keep_prefixentryproductleft + 1 /\ (sto_ap_keep_prefixentryproduct) = 0) /\ (sto_an_keep_prefixentryproduct) = S ge_signed_half_keep_prefixentryproductleft))) /\ ((((((dc_right_keep_prefixentry) = 2 * (sto_bp_keep_prefixentryproduct) /\ (sto_bn_keep_prefixentryproduct) = 0) \/ exists ge_signed_half_keep_prefixentryproductright. (((dc_right_keep_prefixentry) = 2 * ge_signed_half_keep_prefixentryproductright + 1 /\ (sto_bp_keep_prefixentryproduct) = 0) /\ (sto_bn_keep_prefixentryproduct) = S ge_signed_half_keep_prefixentryproductright))) /\ ((((((dc_value_keep_prefix) = 2 * (sto_cp_keep_prefixentryproduct) /\ (sto_cn_keep_prefixentryproduct) = 0) \/ exists ge_signed_half_keep_prefixentryproductoutput. (((dc_value_keep_prefix) = 2 * ge_signed_half_keep_prefixentryproductoutput + 1 /\ (sto_cp_keep_prefixentryproduct) = 0) /\ (sto_cn_keep_prefixentryproduct) = S ge_signed_half_keep_prefixentryproductoutput))) /\ ((sto_ap_keep_prefixentryproduct * sto_bp_keep_prefixentryproduct + sto_an_keep_prefixentryproduct * sto_bn_keep_prefixentryproduct) + sto_cn_keep_prefixentryproduct = (sto_ap_keep_prefixentryproduct * sto_bn_keep_prefixentryproduct + sto_an_keep_prefixentryproduct * sto_bp_keep_prefixentryproduct) + sto_cp_keep_prefixentryproduct))))))))))))))) \/ ((((dc_index_keep_prefix)=0 \/ ~(exists pvs_factor_keep_prefixentrynondivisor. (n) = (dc_index_keep_prefix) * pvs_factor_keep_prefixentrynondivisor)) /\ ((dc_value_keep_prefix)=0))))))) -> (exists pvs_le_gap_keep_bound. pvs_le_gap_keep_bound + (d) = (l)) -> ~(d=0) -> n=d*q -> (exists dst_positive_code_keep_left dst_positive_scale_keep_left dst_negative_code_keep_left dst_negative_scale_keep_left dst_positive_keep_left dst_negative_keep_left. (((F) = (((((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) * S ((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) + ((dst_positive_scale_keep_left) + (dst_positive_scale_keep_left))) + (((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left)))) * S ((((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) * S ((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) + ((dst_positive_scale_keep_left) + (dst_positive_scale_keep_left))) + (((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left)))) + ((((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left))) + (((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left)))))) /\ (((((exists ff_h_pvs_keep_leftpositive. ff_h_pvs_keep_leftpositive + S (dst_positive_keep_left) = S ((S (d)) * dst_positive_scale_keep_left)) /\ exists ff_q_pvs_keep_leftpositive. dst_positive_code_keep_left = ff_q_pvs_keep_leftpositive * S ((S (d)) * dst_positive_scale_keep_left) + (dst_positive_keep_left))) /\ (((((exists ff_h_pvs_keep_leftnegative. ff_h_pvs_keep_leftnegative + S (dst_negative_keep_left) = S ((S (d)) * dst_negative_scale_keep_left)) /\ exists ff_q_pvs_keep_leftnegative. dst_negative_code_keep_left = ff_q_pvs_keep_leftnegative * S ((S (d)) * dst_negative_scale_keep_left) + (dst_negative_keep_left))) /\ (exists ge_balance_positive_keep_leftvalue ge_balance_negative_keep_leftvalue. (((((a) = 2 * (ge_balance_positive_keep_leftvalue) /\ (ge_balance_negative_keep_leftvalue) = 0) \/ exists ge_signed_half_keep_leftvaluedecode. (((a) = 2 * ge_signed_half_keep_leftvaluedecode + 1 /\ (ge_balance_positive_keep_leftvalue) = 0) /\ (ge_balance_negative_keep_leftvalue) = S ge_signed_half_keep_leftvaluedecode))) /\ ((dst_positive_keep_left) + ge_balance_negative_keep_leftvalue = (dst_negative_keep_left) + ge_balance_positive_keep_leftvalue))))))))) -> (exists dst_positive_code_keep_right dst_positive_scale_keep_right dst_negative_code_keep_right dst_negative_scale_keep_right dst_positive_keep_right dst_negative_keep_right. (((G) = (((((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) * S ((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) + ((dst_positive_scale_keep_right) + (dst_positive_scale_keep_right))) + (((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right)))) * S ((((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) * S ((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) + ((dst_positive_scale_keep_right) + (dst_positive_scale_keep_right))) + (((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right)))) + ((((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right))) + (((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right)))))) /\ (((((exists ff_h_pvs_keep_rightpositive. ff_h_pvs_keep_rightpositive + S (dst_positive_keep_right) = S ((S (q)) * dst_positive_scale_keep_right)) /\ exists ff_q_pvs_keep_rightpositive. dst_positive_code_keep_right = ff_q_pvs_keep_rightpositive * S ((S (q)) * dst_positive_scale_keep_right) + (dst_positive_keep_right))) /\ (((((exists ff_h_pvs_keep_rightnegative. ff_h_pvs_keep_rightnegative + S (dst_negative_keep_right) = S ((S (q)) * dst_negative_scale_keep_right)) /\ exists ff_q_pvs_keep_rightnegative. dst_negative_code_keep_right = ff_q_pvs_keep_rightnegative * S ((S (q)) * dst_negative_scale_keep_right) + (dst_negative_keep_right))) /\ (exists ge_balance_positive_keep_rightvalue ge_balance_negative_keep_rightvalue. (((((b) = 2 * (ge_balance_positive_keep_rightvalue) /\ (ge_balance_negative_keep_rightvalue) = 0) \/ exists ge_signed_half_keep_rightvaluedecode. (((b) = 2 * ge_signed_half_keep_rightvaluedecode + 1 /\ (ge_balance_positive_keep_rightvalue) = 0) /\ (ge_balance_negative_keep_rightvalue) = S ge_signed_half_keep_rightvaluedecode))) /\ ((dst_positive_keep_right) + ge_balance_negative_keep_rightvalue = (dst_negative_keep_right) + ge_balance_positive_keep_rightvalue))))))))) -> (exists sto_ap_keep_product sto_an_keep_product sto_bp_keep_product sto_bn_keep_product sto_cp_keep_product sto_cn_keep_product. (((((a) = 2 * (sto_ap_keep_product) /\ (sto_an_keep_product) = 0) \/ exists ge_signed_half_keep_productleft. (((a) = 2 * ge_signed_half_keep_productleft + 1 /\ (sto_ap_keep_product) = 0) /\ (sto_an_keep_product) = S ge_signed_half_keep_productleft))) /\ ((((((b) = 2 * (sto_bp_keep_product) /\ (sto_bn_keep_product) = 0) \/ exists ge_signed_half_keep_productright. (((b) = 2 * ge_signed_half_keep_productright + 1 /\ (sto_bp_keep_product) = 0) /\ (sto_bn_keep_product) = S ge_signed_half_keep_productright))) /\ ((((((z) = 2 * (sto_cp_keep_product) /\ (sto_cn_keep_product) = 0) \/ exists ge_signed_half_keep_productoutput. (((z) = 2 * ge_signed_half_keep_productoutput + 1 /\ (sto_cp_keep_product) = 0) /\ (sto_cn_keep_product) = S ge_signed_half_keep_productoutput))) /\ ((sto_ap_keep_product * sto_bp_keep_product + sto_an_keep_product * sto_bn_keep_product) + sto_cn_keep_product = (sto_ap_keep_product * sto_bn_keep_product + sto_an_keep_product * sto_bp_keep_product) + sto_cp_keep_product))))))) -> (exists dst_positive_code_keep_result dst_positive_scale_keep_result dst_negative_code_keep_result dst_negative_scale_keep_result dst_positive_keep_result dst_negative_keep_result. (((M) = (((((dst_positive_code_keep_result) + (dst_positive_scale_keep_result)) * S ((dst_positive_code_keep_result) + (dst_positive_scale_keep_result)) + ((dst_positive_scale_keep_result) + (dst_positive_scale_keep_result))) + (((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) * S ((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) + ((dst_negative_scale_keep_result) + (dst_negative_scale_keep_result)))) * S ((((dst_positive_code_keep_result) + (dst_positive_scale_keep_result)) * S ((dst_positive_code_keep_result) + (dst_positive_scale_keep_result)) + ((dst_positive_scale_keep_result) + (dst_positive_scale_keep_result))) + (((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) * S ((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) + ((dst_negative_scale_keep_result) + (dst_negative_scale_keep_result)))) + ((((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) * S ((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) + ((dst_negative_scale_keep_result) + (dst_negative_scale_keep_result))) + (((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) * S ((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) + ((dst_negative_scale_keep_result) + (dst_negative_scale_keep_result)))))) /\ (((((exists ff_h_pvs_keep_resultpositive. ff_h_pvs_keep_resultpositive + S (dst_positive_keep_result) = S ((S (d)) * dst_positive_scale_keep_result)) /\ exists ff_q_pvs_keep_resultpositive. dst_positive_code_keep_result = ff_q_pvs_keep_resultpositive * S ((S (d)) * dst_positive_scale_keep_result) + (dst_positive_keep_result))) /\ (((((exists ff_h_pvs_keep_resultnegative. ff_h_pvs_keep_resultnegative + S (dst_negative_keep_result) = S ((S (d)) * dst_negative_scale_keep_result)) /\ exists ff_q_pvs_keep_resultnegative. dst_negative_code_keep_result = ff_q_pvs_keep_resultnegative * S ((S (d)) * dst_negative_scale_keep_result) + (dst_negative_keep_result))) /\ (exists ge_balance_positive_keep_resultvalue ge_balance_negative_keep_resultvalue. (((((z) = 2 * (ge_balance_positive_keep_resultvalue) /\ (ge_balance_negative_keep_resultvalue) = 0) \/ exists ge_signed_half_keep_resultvaluedecode. (((z) = 2 * ge_signed_half_keep_resultvaluedecode + 1 /\ (ge_balance_positive_keep_resultvalue) = 0) /\ (ge_balance_negative_keep_resultvalue) = S ge_signed_half_keep_resultvaluedecode))) /\ ((dst_positive_keep_result) + ge_balance_negative_keep_resultvalue = (dst_negative_keep_result) + ge_balance_positive_keep_resultvalue)))))))))