dirichlet_convolution_prefix_value_from_entry

Exact expanded first-order arithmetic statement

forall F G n l M d z. (((exists dst_positive_code_value_prefixtable dst_positive_scale_value_prefixtable dst_negative_code_value_prefixtable dst_negative_scale_value_prefixtable. (((M) = (((((dst_positive_code_value_prefixtable) + (dst_positive_scale_value_prefixtable)) * S ((dst_positive_code_value_prefixtable) + (dst_positive_scale_value_prefixtable)) + ((dst_positive_scale_value_prefixtable) + (dst_positive_scale_value_prefixtable))) + (((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) * S ((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) + ((dst_negative_scale_value_prefixtable) + (dst_negative_scale_value_prefixtable)))) * S ((((dst_positive_code_value_prefixtable) + (dst_positive_scale_value_prefixtable)) * S ((dst_positive_code_value_prefixtable) + (dst_positive_scale_value_prefixtable)) + ((dst_positive_scale_value_prefixtable) + (dst_positive_scale_value_prefixtable))) + (((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) * S ((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) + ((dst_negative_scale_value_prefixtable) + (dst_negative_scale_value_prefixtable)))) + ((((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) * S ((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) + ((dst_negative_scale_value_prefixtable) + (dst_negative_scale_value_prefixtable))) + (((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) * S ((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) + ((dst_negative_scale_value_prefixtable) + (dst_negative_scale_value_prefixtable)))))) /\ (forall dst_index_value_prefixtable. (exists pvs_le_gap_value_prefixtabledomain. pvs_le_gap_value_prefixtabledomain + (dst_index_value_prefixtable) = (l)) -> exists dst_positive_value_prefixtable dst_negative_value_prefixtable dst_value_value_prefixtable. ((((exists ff_h_pvs_value_prefixtableentrypositive. ff_h_pvs_value_prefixtableentrypositive + S (dst_positive_value_prefixtable) = S ((S (dst_index_value_prefixtable)) * dst_positive_scale_value_prefixtable)) /\ exists ff_q_pvs_value_prefixtableentrypositive. dst_positive_code_value_prefixtable = ff_q_pvs_value_prefixtableentrypositive * S ((S (dst_index_value_prefixtable)) * dst_positive_scale_value_prefixtable) + (dst_positive_value_prefixtable))) /\ (((((exists ff_h_pvs_value_prefixtableentrynegative. ff_h_pvs_value_prefixtableentrynegative + S (dst_negative_value_prefixtable) = S ((S (dst_index_value_prefixtable)) * dst_negative_scale_value_prefixtable)) /\ exists ff_q_pvs_value_prefixtableentrynegative. dst_negative_code_value_prefixtable = ff_q_pvs_value_prefixtableentrynegative * S ((S (dst_index_value_prefixtable)) * dst_negative_scale_value_prefixtable) + (dst_negative_value_prefixtable))) /\ (exists ge_balance_positive_value_prefixtableentryvalue ge_balance_negative_value_prefixtableentryvalue. (((((dst_value_value_prefixtable) = 2 * (ge_balance_positive_value_prefixtableentryvalue) /\ (ge_balance_negative_value_prefixtableentryvalue) = 0) \/ exists ge_signed_half_value_prefixtableentryvaluedecode. (((dst_value_value_prefixtable) = 2 * ge_signed_half_value_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_value_prefixtableentryvalue) = 0) /\ (ge_balance_negative_value_prefixtableentryvalue) = S ge_signed_half_value_prefixtableentryvaluedecode))) /\ ((dst_positive_value_prefixtable) + ge_balance_negative_value_prefixtableentryvalue = (dst_negative_value_prefixtable) + ge_balance_positive_value_prefixtableentryvalue))))))))) /\ (forall dc_index_value_prefix dc_value_value_prefix. (exists pvs_le_gap_value_prefixdomain. pvs_le_gap_value_prefixdomain + (dc_index_value_prefix) = (l)) -> (exists dst_positive_code_value_prefixlookup dst_positive_scale_value_prefixlookup dst_negative_code_value_prefixlookup dst_negative_scale_value_prefixlookup dst_positive_value_prefixlookup dst_negative_value_prefixlookup. (((M) = (((((dst_positive_code_value_prefixlookup) + (dst_positive_scale_value_prefixlookup)) * S ((dst_positive_code_value_prefixlookup) + (dst_positive_scale_value_prefixlookup)) + ((dst_positive_scale_value_prefixlookup) + (dst_positive_scale_value_prefixlookup))) + (((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) * S ((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) + ((dst_negative_scale_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)))) * S ((((dst_positive_code_value_prefixlookup) + (dst_positive_scale_value_prefixlookup)) * S ((dst_positive_code_value_prefixlookup) + (dst_positive_scale_value_prefixlookup)) + ((dst_positive_scale_value_prefixlookup) + (dst_positive_scale_value_prefixlookup))) + (((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) * S ((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) + ((dst_negative_scale_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)))) + ((((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) * S ((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) + ((dst_negative_scale_value_prefixlookup) + (dst_negative_scale_value_prefixlookup))) + (((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) * S ((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) + ((dst_negative_scale_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)))))) /\ (((((exists ff_h_pvs_value_prefixlookuppositive. ff_h_pvs_value_prefixlookuppositive + S (dst_positive_value_prefixlookup) = S ((S (dc_index_value_prefix)) * dst_positive_scale_value_prefixlookup)) /\ exists ff_q_pvs_value_prefixlookuppositive. dst_positive_code_value_prefixlookup = ff_q_pvs_value_prefixlookuppositive * S ((S (dc_index_value_prefix)) * dst_positive_scale_value_prefixlookup) + (dst_positive_value_prefixlookup))) /\ (((((exists ff_h_pvs_value_prefixlookupnegative. ff_h_pvs_value_prefixlookupnegative + S (dst_negative_value_prefixlookup) = S ((S (dc_index_value_prefix)) * dst_negative_scale_value_prefixlookup)) /\ exists ff_q_pvs_value_prefixlookupnegative. dst_negative_code_value_prefixlookup = ff_q_pvs_value_prefixlookupnegative * S ((S (dc_index_value_prefix)) * dst_negative_scale_value_prefixlookup) + (dst_negative_value_prefixlookup))) /\ (exists ge_balance_positive_value_prefixlookupvalue ge_balance_negative_value_prefixlookupvalue. (((((dc_value_value_prefix) = 2 * (ge_balance_positive_value_prefixlookupvalue) /\ (ge_balance_negative_value_prefixlookupvalue) = 0) \/ exists ge_signed_half_value_prefixlookupvaluedecode. (((dc_value_value_prefix) = 2 * ge_signed_half_value_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_value_prefixlookupvalue) = 0) /\ (ge_balance_negative_value_prefixlookupvalue) = S ge_signed_half_value_prefixlookupvaluedecode))) /\ ((dst_positive_value_prefixlookup) + ge_balance_negative_value_prefixlookupvalue = (dst_negative_value_prefixlookup) + ge_balance_positive_value_prefixlookupvalue))))))))) -> ((((~((dc_index_value_prefix)=0)) /\ (exists dc_quotient_value_prefixentry dc_left_value_prefixentry dc_right_value_prefixentry. (((n)=(dc_index_value_prefix)*dc_quotient_value_prefixentry) /\ (((exists dst_positive_code_value_prefixentryleft dst_positive_scale_value_prefixentryleft dst_negative_code_value_prefixentryleft dst_negative_scale_value_prefixentryleft dst_positive_value_prefixentryleft dst_negative_value_prefixentryleft. (((F) = (((((dst_positive_code_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft)) * S ((dst_positive_code_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft)) + ((dst_positive_scale_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft))) + (((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) * S ((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) + ((dst_negative_scale_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)))) * S ((((dst_positive_code_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft)) * S ((dst_positive_code_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft)) + ((dst_positive_scale_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft))) + (((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) * S ((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) + ((dst_negative_scale_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)))) + ((((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) * S ((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) + ((dst_negative_scale_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft))) + (((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) * S ((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) + ((dst_negative_scale_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)))))) /\ (((((exists ff_h_pvs_value_prefixentryleftpositive. ff_h_pvs_value_prefixentryleftpositive + S (dst_positive_value_prefixentryleft) = S ((S (dc_index_value_prefix)) * dst_positive_scale_value_prefixentryleft)) /\ exists ff_q_pvs_value_prefixentryleftpositive. dst_positive_code_value_prefixentryleft = ff_q_pvs_value_prefixentryleftpositive * S ((S (dc_index_value_prefix)) * dst_positive_scale_value_prefixentryleft) + (dst_positive_value_prefixentryleft))) /\ (((((exists ff_h_pvs_value_prefixentryleftnegative. ff_h_pvs_value_prefixentryleftnegative + S (dst_negative_value_prefixentryleft) = S ((S (dc_index_value_prefix)) * dst_negative_scale_value_prefixentryleft)) /\ exists ff_q_pvs_value_prefixentryleftnegative. dst_negative_code_value_prefixentryleft = ff_q_pvs_value_prefixentryleftnegative * S ((S (dc_index_value_prefix)) * dst_negative_scale_value_prefixentryleft) + (dst_negative_value_prefixentryleft))) /\ (exists ge_balance_positive_value_prefixentryleftvalue ge_balance_negative_value_prefixentryleftvalue. (((((dc_left_value_prefixentry) = 2 * (ge_balance_positive_value_prefixentryleftvalue) /\ (ge_balance_negative_value_prefixentryleftvalue) = 0) \/ exists ge_signed_half_value_prefixentryleftvaluedecode. (((dc_left_value_prefixentry) = 2 * ge_signed_half_value_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_value_prefixentryleftvalue) = 0) /\ (ge_balance_negative_value_prefixentryleftvalue) = S ge_signed_half_value_prefixentryleftvaluedecode))) /\ ((dst_positive_value_prefixentryleft) + ge_balance_negative_value_prefixentryleftvalue = (dst_negative_value_prefixentryleft) + ge_balance_positive_value_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_value_prefixentryright dst_positive_scale_value_prefixentryright dst_negative_code_value_prefixentryright dst_negative_scale_value_prefixentryright dst_positive_value_prefixentryright dst_negative_value_prefixentryright. (((G) = (((((dst_positive_code_value_prefixentryright) + (dst_positive_scale_value_prefixentryright)) * S ((dst_positive_code_value_prefixentryright) + (dst_positive_scale_value_prefixentryright)) + ((dst_positive_scale_value_prefixentryright) + (dst_positive_scale_value_prefixentryright))) + (((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) * S ((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) + ((dst_negative_scale_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)))) * S ((((dst_positive_code_value_prefixentryright) + (dst_positive_scale_value_prefixentryright)) * S ((dst_positive_code_value_prefixentryright) + (dst_positive_scale_value_prefixentryright)) + ((dst_positive_scale_value_prefixentryright) + (dst_positive_scale_value_prefixentryright))) + (((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) * S ((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) + ((dst_negative_scale_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)))) + ((((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) * S ((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) + ((dst_negative_scale_value_prefixentryright) + (dst_negative_scale_value_prefixentryright))) + (((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) * S ((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) + ((dst_negative_scale_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)))))) /\ (((((exists ff_h_pvs_value_prefixentryrightpositive. ff_h_pvs_value_prefixentryrightpositive + S (dst_positive_value_prefixentryright) = S ((S (dc_quotient_value_prefixentry)) * dst_positive_scale_value_prefixentryright)) /\ exists ff_q_pvs_value_prefixentryrightpositive. dst_positive_code_value_prefixentryright = ff_q_pvs_value_prefixentryrightpositive * S ((S (dc_quotient_value_prefixentry)) * dst_positive_scale_value_prefixentryright) + (dst_positive_value_prefixentryright))) /\ (((((exists ff_h_pvs_value_prefixentryrightnegative. ff_h_pvs_value_prefixentryrightnegative + S (dst_negative_value_prefixentryright) = S ((S (dc_quotient_value_prefixentry)) * dst_negative_scale_value_prefixentryright)) /\ exists ff_q_pvs_value_prefixentryrightnegative. dst_negative_code_value_prefixentryright = ff_q_pvs_value_prefixentryrightnegative * S ((S (dc_quotient_value_prefixentry)) * dst_negative_scale_value_prefixentryright) + (dst_negative_value_prefixentryright))) /\ (exists ge_balance_positive_value_prefixentryrightvalue ge_balance_negative_value_prefixentryrightvalue. (((((dc_right_value_prefixentry) = 2 * (ge_balance_positive_value_prefixentryrightvalue) /\ (ge_balance_negative_value_prefixentryrightvalue) = 0) \/ exists ge_signed_half_value_prefixentryrightvaluedecode. (((dc_right_value_prefixentry) = 2 * ge_signed_half_value_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_value_prefixentryrightvalue) = 0) /\ (ge_balance_negative_value_prefixentryrightvalue) = S ge_signed_half_value_prefixentryrightvaluedecode))) /\ ((dst_positive_value_prefixentryright) + ge_balance_negative_value_prefixentryrightvalue = (dst_negative_value_prefixentryright) + ge_balance_positive_value_prefixentryrightvalue))))))))) /\ (exists sto_ap_value_prefixentryproduct sto_an_value_prefixentryproduct sto_bp_value_prefixentryproduct sto_bn_value_prefixentryproduct sto_cp_value_prefixentryproduct sto_cn_value_prefixentryproduct. (((((dc_left_value_prefixentry) = 2 * (sto_ap_value_prefixentryproduct) /\ (sto_an_value_prefixentryproduct) = 0) \/ exists ge_signed_half_value_prefixentryproductleft. (((dc_left_value_prefixentry) = 2 * ge_signed_half_value_prefixentryproductleft + 1 /\ (sto_ap_value_prefixentryproduct) = 0) /\ (sto_an_value_prefixentryproduct) = S ge_signed_half_value_prefixentryproductleft))) /\ ((((((dc_right_value_prefixentry) = 2 * (sto_bp_value_prefixentryproduct) /\ (sto_bn_value_prefixentryproduct) = 0) \/ exists ge_signed_half_value_prefixentryproductright. (((dc_right_value_prefixentry) = 2 * ge_signed_half_value_prefixentryproductright + 1 /\ (sto_bp_value_prefixentryproduct) = 0) /\ (sto_bn_value_prefixentryproduct) = S ge_signed_half_value_prefixentryproductright))) /\ ((((((dc_value_value_prefix) = 2 * (sto_cp_value_prefixentryproduct) /\ (sto_cn_value_prefixentryproduct) = 0) \/ exists ge_signed_half_value_prefixentryproductoutput. (((dc_value_value_prefix) = 2 * ge_signed_half_value_prefixentryproductoutput + 1 /\ (sto_cp_value_prefixentryproduct) = 0) /\ (sto_cn_value_prefixentryproduct) = S ge_signed_half_value_prefixentryproductoutput))) /\ ((sto_ap_value_prefixentryproduct * sto_bp_value_prefixentryproduct + sto_an_value_prefixentryproduct * sto_bn_value_prefixentryproduct) + sto_cn_value_prefixentryproduct = (sto_ap_value_prefixentryproduct * sto_bn_value_prefixentryproduct + sto_an_value_prefixentryproduct * sto_bp_value_prefixentryproduct) + sto_cp_value_prefixentryproduct))))))))))))))) \/ ((((dc_index_value_prefix)=0 \/ ~(exists pvs_factor_value_prefixentrynondivisor. (n) = (dc_index_value_prefix) * pvs_factor_value_prefixentrynondivisor)) /\ ((dc_value_value_prefix)=0))))))) -> (exists pvs_le_gap_value_bound. pvs_le_gap_value_bound + (d) = (l)) -> ((((~((d)=0)) /\ (exists dc_quotient_value_graph dc_left_value_graph dc_right_value_graph. (((n)=(d)*dc_quotient_value_graph) /\ (((exists dst_positive_code_value_graphleft dst_positive_scale_value_graphleft dst_negative_code_value_graphleft dst_negative_scale_value_graphleft dst_positive_value_graphleft dst_negative_value_graphleft. (((F) = (((((dst_positive_code_value_graphleft) + (dst_positive_scale_value_graphleft)) * S ((dst_positive_code_value_graphleft) + (dst_positive_scale_value_graphleft)) + ((dst_positive_scale_value_graphleft) + (dst_positive_scale_value_graphleft))) + (((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) * S ((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) + ((dst_negative_scale_value_graphleft) + (dst_negative_scale_value_graphleft)))) * S ((((dst_positive_code_value_graphleft) + (dst_positive_scale_value_graphleft)) * S ((dst_positive_code_value_graphleft) + (dst_positive_scale_value_graphleft)) + ((dst_positive_scale_value_graphleft) + (dst_positive_scale_value_graphleft))) + (((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) * S ((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) + ((dst_negative_scale_value_graphleft) + (dst_negative_scale_value_graphleft)))) + ((((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) * S ((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) + ((dst_negative_scale_value_graphleft) + (dst_negative_scale_value_graphleft))) + (((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) * S ((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) + ((dst_negative_scale_value_graphleft) + (dst_negative_scale_value_graphleft)))))) /\ (((((exists ff_h_pvs_value_graphleftpositive. ff_h_pvs_value_graphleftpositive + S (dst_positive_value_graphleft) = S ((S (d)) * dst_positive_scale_value_graphleft)) /\ exists ff_q_pvs_value_graphleftpositive. dst_positive_code_value_graphleft = ff_q_pvs_value_graphleftpositive * S ((S (d)) * dst_positive_scale_value_graphleft) + (dst_positive_value_graphleft))) /\ (((((exists ff_h_pvs_value_graphleftnegative. ff_h_pvs_value_graphleftnegative + S (dst_negative_value_graphleft) = S ((S (d)) * dst_negative_scale_value_graphleft)) /\ exists ff_q_pvs_value_graphleftnegative. dst_negative_code_value_graphleft = ff_q_pvs_value_graphleftnegative * S ((S (d)) * dst_negative_scale_value_graphleft) + (dst_negative_value_graphleft))) /\ (exists ge_balance_positive_value_graphleftvalue ge_balance_negative_value_graphleftvalue. (((((dc_left_value_graph) = 2 * (ge_balance_positive_value_graphleftvalue) /\ (ge_balance_negative_value_graphleftvalue) = 0) \/ exists ge_signed_half_value_graphleftvaluedecode. (((dc_left_value_graph) = 2 * ge_signed_half_value_graphleftvaluedecode + 1 /\ (ge_balance_positive_value_graphleftvalue) = 0) /\ (ge_balance_negative_value_graphleftvalue) = S ge_signed_half_value_graphleftvaluedecode))) /\ ((dst_positive_value_graphleft) + ge_balance_negative_value_graphleftvalue = (dst_negative_value_graphleft) + ge_balance_positive_value_graphleftvalue))))))))) /\ (((exists dst_positive_code_value_graphright dst_positive_scale_value_graphright dst_negative_code_value_graphright dst_negative_scale_value_graphright dst_positive_value_graphright dst_negative_value_graphright. (((G) = (((((dst_positive_code_value_graphright) + (dst_positive_scale_value_graphright)) * S ((dst_positive_code_value_graphright) + (dst_positive_scale_value_graphright)) + ((dst_positive_scale_value_graphright) + (dst_positive_scale_value_graphright))) + (((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) * S ((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) + ((dst_negative_scale_value_graphright) + (dst_negative_scale_value_graphright)))) * S ((((dst_positive_code_value_graphright) + (dst_positive_scale_value_graphright)) * S ((dst_positive_code_value_graphright) + (dst_positive_scale_value_graphright)) + ((dst_positive_scale_value_graphright) + (dst_positive_scale_value_graphright))) + (((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) * S ((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) + ((dst_negative_scale_value_graphright) + (dst_negative_scale_value_graphright)))) + ((((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) * S ((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) + ((dst_negative_scale_value_graphright) + (dst_negative_scale_value_graphright))) + (((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) * S ((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) + ((dst_negative_scale_value_graphright) + (dst_negative_scale_value_graphright)))))) /\ (((((exists ff_h_pvs_value_graphrightpositive. ff_h_pvs_value_graphrightpositive + S (dst_positive_value_graphright) = S ((S (dc_quotient_value_graph)) * dst_positive_scale_value_graphright)) /\ exists ff_q_pvs_value_graphrightpositive. dst_positive_code_value_graphright = ff_q_pvs_value_graphrightpositive * S ((S (dc_quotient_value_graph)) * dst_positive_scale_value_graphright) + (dst_positive_value_graphright))) /\ (((((exists ff_h_pvs_value_graphrightnegative. ff_h_pvs_value_graphrightnegative + S (dst_negative_value_graphright) = S ((S (dc_quotient_value_graph)) * dst_negative_scale_value_graphright)) /\ exists ff_q_pvs_value_graphrightnegative. dst_negative_code_value_graphright = ff_q_pvs_value_graphrightnegative * S ((S (dc_quotient_value_graph)) * dst_negative_scale_value_graphright) + (dst_negative_value_graphright))) /\ (exists ge_balance_positive_value_graphrightvalue ge_balance_negative_value_graphrightvalue. (((((dc_right_value_graph) = 2 * (ge_balance_positive_value_graphrightvalue) /\ (ge_balance_negative_value_graphrightvalue) = 0) \/ exists ge_signed_half_value_graphrightvaluedecode. (((dc_right_value_graph) = 2 * ge_signed_half_value_graphrightvaluedecode + 1 /\ (ge_balance_positive_value_graphrightvalue) = 0) /\ (ge_balance_negative_value_graphrightvalue) = S ge_signed_half_value_graphrightvaluedecode))) /\ ((dst_positive_value_graphright) + ge_balance_negative_value_graphrightvalue = (dst_negative_value_graphright) + ge_balance_positive_value_graphrightvalue))))))))) /\ (exists sto_ap_value_graphproduct sto_an_value_graphproduct sto_bp_value_graphproduct sto_bn_value_graphproduct sto_cp_value_graphproduct sto_cn_value_graphproduct. (((((dc_left_value_graph) = 2 * (sto_ap_value_graphproduct) /\ (sto_an_value_graphproduct) = 0) \/ exists ge_signed_half_value_graphproductleft. (((dc_left_value_graph) = 2 * ge_signed_half_value_graphproductleft + 1 /\ (sto_ap_value_graphproduct) = 0) /\ (sto_an_value_graphproduct) = S ge_signed_half_value_graphproductleft))) /\ ((((((dc_right_value_graph) = 2 * (sto_bp_value_graphproduct) /\ (sto_bn_value_graphproduct) = 0) \/ exists ge_signed_half_value_graphproductright. (((dc_right_value_graph) = 2 * ge_signed_half_value_graphproductright + 1 /\ (sto_bp_value_graphproduct) = 0) /\ (sto_bn_value_graphproduct) = S ge_signed_half_value_graphproductright))) /\ ((((((z) = 2 * (sto_cp_value_graphproduct) /\ (sto_cn_value_graphproduct) = 0) \/ exists ge_signed_half_value_graphproductoutput. (((z) = 2 * ge_signed_half_value_graphproductoutput + 1 /\ (sto_cp_value_graphproduct) = 0) /\ (sto_cn_value_graphproduct) = S ge_signed_half_value_graphproductoutput))) /\ ((sto_ap_value_graphproduct * sto_bp_value_graphproduct + sto_an_value_graphproduct * sto_bn_value_graphproduct) + sto_cn_value_graphproduct = (sto_ap_value_graphproduct * sto_bn_value_graphproduct + sto_an_value_graphproduct * sto_bp_value_graphproduct) + sto_cp_value_graphproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_value_graphnondivisor. (n) = (d) * pvs_factor_value_graphnondivisor)) /\ ((z)=0)))) -> (exists dst_positive_code_value_result dst_positive_scale_value_result dst_negative_code_value_result dst_negative_scale_value_result dst_positive_value_result dst_negative_value_result. (((M) = (((((dst_positive_code_value_result) + (dst_positive_scale_value_result)) * S ((dst_positive_code_value_result) + (dst_positive_scale_value_result)) + ((dst_positive_scale_value_result) + (dst_positive_scale_value_result))) + (((dst_negative_code_value_result) + (dst_negative_scale_value_result)) * S ((dst_negative_code_value_result) + (dst_negative_scale_value_result)) + ((dst_negative_scale_value_result) + (dst_negative_scale_value_result)))) * S ((((dst_positive_code_value_result) + (dst_positive_scale_value_result)) * S ((dst_positive_code_value_result) + (dst_positive_scale_value_result)) + ((dst_positive_scale_value_result) + (dst_positive_scale_value_result))) + (((dst_negative_code_value_result) + (dst_negative_scale_value_result)) * S ((dst_negative_code_value_result) + (dst_negative_scale_value_result)) + ((dst_negative_scale_value_result) + (dst_negative_scale_value_result)))) + ((((dst_negative_code_value_result) + (dst_negative_scale_value_result)) * S ((dst_negative_code_value_result) + (dst_negative_scale_value_result)) + ((dst_negative_scale_value_result) + (dst_negative_scale_value_result))) + (((dst_negative_code_value_result) + (dst_negative_scale_value_result)) * S ((dst_negative_code_value_result) + (dst_negative_scale_value_result)) + ((dst_negative_scale_value_result) + (dst_negative_scale_value_result)))))) /\ (((((exists ff_h_pvs_value_resultpositive. ff_h_pvs_value_resultpositive + S (dst_positive_value_result) = S ((S (d)) * dst_positive_scale_value_result)) /\ exists ff_q_pvs_value_resultpositive. dst_positive_code_value_result = ff_q_pvs_value_resultpositive * S ((S (d)) * dst_positive_scale_value_result) + (dst_positive_value_result))) /\ (((((exists ff_h_pvs_value_resultnegative. ff_h_pvs_value_resultnegative + S (dst_negative_value_result) = S ((S (d)) * dst_negative_scale_value_result)) /\ exists ff_q_pvs_value_resultnegative. dst_negative_code_value_result = ff_q_pvs_value_resultnegative * S ((S (d)) * dst_negative_scale_value_result) + (dst_negative_value_result))) /\ (exists ge_balance_positive_value_resultvalue ge_balance_negative_value_resultvalue. (((((z) = 2 * (ge_balance_positive_value_resultvalue) /\ (ge_balance_negative_value_resultvalue) = 0) \/ exists ge_signed_half_value_resultvaluedecode. (((z) = 2 * ge_signed_half_value_resultvaluedecode + 1 /\ (ge_balance_positive_value_resultvalue) = 0) /\ (ge_balance_negative_value_resultvalue) = S ge_signed_half_value_resultvaluedecode))) /\ ((dst_positive_value_result) + ge_balance_negative_value_resultvalue = (dst_negative_value_result) + ge_balance_positive_value_resultvalue)))))))))