dirichlet_convolution_prefix_lookup

Exact expanded first-order arithmetic statement

forall F G n l M d z. (((exists dst_positive_code_lookup_prefixtable dst_positive_scale_lookup_prefixtable dst_negative_code_lookup_prefixtable dst_negative_scale_lookup_prefixtable. (((M) = (((((dst_positive_code_lookup_prefixtable) + (dst_positive_scale_lookup_prefixtable)) * S ((dst_positive_code_lookup_prefixtable) + (dst_positive_scale_lookup_prefixtable)) + ((dst_positive_scale_lookup_prefixtable) + (dst_positive_scale_lookup_prefixtable))) + (((dst_negative_code_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)) * S ((dst_negative_code_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)) + ((dst_negative_scale_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)))) * S ((((dst_positive_code_lookup_prefixtable) + (dst_positive_scale_lookup_prefixtable)) * S ((dst_positive_code_lookup_prefixtable) + (dst_positive_scale_lookup_prefixtable)) + ((dst_positive_scale_lookup_prefixtable) + (dst_positive_scale_lookup_prefixtable))) + (((dst_negative_code_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)) * S ((dst_negative_code_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)) + ((dst_negative_scale_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)))) + ((((dst_negative_code_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)) * S ((dst_negative_code_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)) + ((dst_negative_scale_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable))) + (((dst_negative_code_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)) * S ((dst_negative_code_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)) + ((dst_negative_scale_lookup_prefixtable) + (dst_negative_scale_lookup_prefixtable)))))) /\ (forall dst_index_lookup_prefixtable. (exists pvs_le_gap_lookup_prefixtabledomain. pvs_le_gap_lookup_prefixtabledomain + (dst_index_lookup_prefixtable) = (l)) -> exists dst_positive_lookup_prefixtable dst_negative_lookup_prefixtable dst_value_lookup_prefixtable. ((((exists ff_h_pvs_lookup_prefixtableentrypositive. ff_h_pvs_lookup_prefixtableentrypositive + S (dst_positive_lookup_prefixtable) = S ((S (dst_index_lookup_prefixtable)) * dst_positive_scale_lookup_prefixtable)) /\ exists ff_q_pvs_lookup_prefixtableentrypositive. dst_positive_code_lookup_prefixtable = ff_q_pvs_lookup_prefixtableentrypositive * S ((S (dst_index_lookup_prefixtable)) * dst_positive_scale_lookup_prefixtable) + (dst_positive_lookup_prefixtable))) /\ (((((exists ff_h_pvs_lookup_prefixtableentrynegative. ff_h_pvs_lookup_prefixtableentrynegative + S (dst_negative_lookup_prefixtable) = S ((S (dst_index_lookup_prefixtable)) * dst_negative_scale_lookup_prefixtable)) /\ exists ff_q_pvs_lookup_prefixtableentrynegative. dst_negative_code_lookup_prefixtable = ff_q_pvs_lookup_prefixtableentrynegative * S ((S (dst_index_lookup_prefixtable)) * dst_negative_scale_lookup_prefixtable) + (dst_negative_lookup_prefixtable))) /\ (exists ge_balance_positive_lookup_prefixtableentryvalue ge_balance_negative_lookup_prefixtableentryvalue. (((((dst_value_lookup_prefixtable) = 2 * (ge_balance_positive_lookup_prefixtableentryvalue) /\ (ge_balance_negative_lookup_prefixtableentryvalue) = 0) \/ exists ge_signed_half_lookup_prefixtableentryvaluedecode. (((dst_value_lookup_prefixtable) = 2 * ge_signed_half_lookup_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_lookup_prefixtableentryvalue) = 0) /\ (ge_balance_negative_lookup_prefixtableentryvalue) = S ge_signed_half_lookup_prefixtableentryvaluedecode))) /\ ((dst_positive_lookup_prefixtable) + ge_balance_negative_lookup_prefixtableentryvalue = (dst_negative_lookup_prefixtable) + ge_balance_positive_lookup_prefixtableentryvalue))))))))) /\ (forall dc_index_lookup_prefix dc_value_lookup_prefix. (exists pvs_le_gap_lookup_prefixdomain. pvs_le_gap_lookup_prefixdomain + (dc_index_lookup_prefix) = (l)) -> (exists dst_positive_code_lookup_prefixlookup dst_positive_scale_lookup_prefixlookup dst_negative_code_lookup_prefixlookup dst_negative_scale_lookup_prefixlookup dst_positive_lookup_prefixlookup dst_negative_lookup_prefixlookup. (((M) = (((((dst_positive_code_lookup_prefixlookup) + (dst_positive_scale_lookup_prefixlookup)) * S ((dst_positive_code_lookup_prefixlookup) + (dst_positive_scale_lookup_prefixlookup)) + ((dst_positive_scale_lookup_prefixlookup) + (dst_positive_scale_lookup_prefixlookup))) + (((dst_negative_code_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)) * S ((dst_negative_code_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)) + ((dst_negative_scale_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)))) * S ((((dst_positive_code_lookup_prefixlookup) + (dst_positive_scale_lookup_prefixlookup)) * S ((dst_positive_code_lookup_prefixlookup) + (dst_positive_scale_lookup_prefixlookup)) + ((dst_positive_scale_lookup_prefixlookup) + (dst_positive_scale_lookup_prefixlookup))) + (((dst_negative_code_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)) * S ((dst_negative_code_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)) + ((dst_negative_scale_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)))) + ((((dst_negative_code_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)) * S ((dst_negative_code_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)) + ((dst_negative_scale_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup))) + (((dst_negative_code_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)) * S ((dst_negative_code_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)) + ((dst_negative_scale_lookup_prefixlookup) + (dst_negative_scale_lookup_prefixlookup)))))) /\ (((((exists ff_h_pvs_lookup_prefixlookuppositive. ff_h_pvs_lookup_prefixlookuppositive + S (dst_positive_lookup_prefixlookup) = S ((S (dc_index_lookup_prefix)) * dst_positive_scale_lookup_prefixlookup)) /\ exists ff_q_pvs_lookup_prefixlookuppositive. dst_positive_code_lookup_prefixlookup = ff_q_pvs_lookup_prefixlookuppositive * S ((S (dc_index_lookup_prefix)) * dst_positive_scale_lookup_prefixlookup) + (dst_positive_lookup_prefixlookup))) /\ (((((exists ff_h_pvs_lookup_prefixlookupnegative. ff_h_pvs_lookup_prefixlookupnegative + S (dst_negative_lookup_prefixlookup) = S ((S (dc_index_lookup_prefix)) * dst_negative_scale_lookup_prefixlookup)) /\ exists ff_q_pvs_lookup_prefixlookupnegative. dst_negative_code_lookup_prefixlookup = ff_q_pvs_lookup_prefixlookupnegative * S ((S (dc_index_lookup_prefix)) * dst_negative_scale_lookup_prefixlookup) + (dst_negative_lookup_prefixlookup))) /\ (exists ge_balance_positive_lookup_prefixlookupvalue ge_balance_negative_lookup_prefixlookupvalue. (((((dc_value_lookup_prefix) = 2 * (ge_balance_positive_lookup_prefixlookupvalue) /\ (ge_balance_negative_lookup_prefixlookupvalue) = 0) \/ exists ge_signed_half_lookup_prefixlookupvaluedecode. (((dc_value_lookup_prefix) = 2 * ge_signed_half_lookup_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_lookup_prefixlookupvalue) = 0) /\ (ge_balance_negative_lookup_prefixlookupvalue) = S ge_signed_half_lookup_prefixlookupvaluedecode))) /\ ((dst_positive_lookup_prefixlookup) + ge_balance_negative_lookup_prefixlookupvalue = (dst_negative_lookup_prefixlookup) + ge_balance_positive_lookup_prefixlookupvalue))))))))) -> ((((~((dc_index_lookup_prefix)=0)) /\ (exists dc_quotient_lookup_prefixentry dc_left_lookup_prefixentry dc_right_lookup_prefixentry. (((n)=(dc_index_lookup_prefix)*dc_quotient_lookup_prefixentry) /\ (((exists dst_positive_code_lookup_prefixentryleft dst_positive_scale_lookup_prefixentryleft dst_negative_code_lookup_prefixentryleft dst_negative_scale_lookup_prefixentryleft dst_positive_lookup_prefixentryleft dst_negative_lookup_prefixentryleft. (((F) = (((((dst_positive_code_lookup_prefixentryleft) + (dst_positive_scale_lookup_prefixentryleft)) * S ((dst_positive_code_lookup_prefixentryleft) + (dst_positive_scale_lookup_prefixentryleft)) + ((dst_positive_scale_lookup_prefixentryleft) + (dst_positive_scale_lookup_prefixentryleft))) + (((dst_negative_code_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)) * S ((dst_negative_code_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)) + ((dst_negative_scale_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)))) * S ((((dst_positive_code_lookup_prefixentryleft) + (dst_positive_scale_lookup_prefixentryleft)) * S ((dst_positive_code_lookup_prefixentryleft) + (dst_positive_scale_lookup_prefixentryleft)) + ((dst_positive_scale_lookup_prefixentryleft) + (dst_positive_scale_lookup_prefixentryleft))) + (((dst_negative_code_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)) * S ((dst_negative_code_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)) + ((dst_negative_scale_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)))) + ((((dst_negative_code_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)) * S ((dst_negative_code_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)) + ((dst_negative_scale_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft))) + (((dst_negative_code_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)) * S ((dst_negative_code_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)) + ((dst_negative_scale_lookup_prefixentryleft) + (dst_negative_scale_lookup_prefixentryleft)))))) /\ (((((exists ff_h_pvs_lookup_prefixentryleftpositive. ff_h_pvs_lookup_prefixentryleftpositive + S (dst_positive_lookup_prefixentryleft) = S ((S (dc_index_lookup_prefix)) * dst_positive_scale_lookup_prefixentryleft)) /\ exists ff_q_pvs_lookup_prefixentryleftpositive. dst_positive_code_lookup_prefixentryleft = ff_q_pvs_lookup_prefixentryleftpositive * S ((S (dc_index_lookup_prefix)) * dst_positive_scale_lookup_prefixentryleft) + (dst_positive_lookup_prefixentryleft))) /\ (((((exists ff_h_pvs_lookup_prefixentryleftnegative. ff_h_pvs_lookup_prefixentryleftnegative + S (dst_negative_lookup_prefixentryleft) = S ((S (dc_index_lookup_prefix)) * dst_negative_scale_lookup_prefixentryleft)) /\ exists ff_q_pvs_lookup_prefixentryleftnegative. dst_negative_code_lookup_prefixentryleft = ff_q_pvs_lookup_prefixentryleftnegative * S ((S (dc_index_lookup_prefix)) * dst_negative_scale_lookup_prefixentryleft) + (dst_negative_lookup_prefixentryleft))) /\ (exists ge_balance_positive_lookup_prefixentryleftvalue ge_balance_negative_lookup_prefixentryleftvalue. (((((dc_left_lookup_prefixentry) = 2 * (ge_balance_positive_lookup_prefixentryleftvalue) /\ (ge_balance_negative_lookup_prefixentryleftvalue) = 0) \/ exists ge_signed_half_lookup_prefixentryleftvaluedecode. (((dc_left_lookup_prefixentry) = 2 * ge_signed_half_lookup_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_lookup_prefixentryleftvalue) = 0) /\ (ge_balance_negative_lookup_prefixentryleftvalue) = S ge_signed_half_lookup_prefixentryleftvaluedecode))) /\ ((dst_positive_lookup_prefixentryleft) + ge_balance_negative_lookup_prefixentryleftvalue = (dst_negative_lookup_prefixentryleft) + ge_balance_positive_lookup_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_lookup_prefixentryright dst_positive_scale_lookup_prefixentryright dst_negative_code_lookup_prefixentryright dst_negative_scale_lookup_prefixentryright dst_positive_lookup_prefixentryright dst_negative_lookup_prefixentryright. (((G) = (((((dst_positive_code_lookup_prefixentryright) + (dst_positive_scale_lookup_prefixentryright)) * S ((dst_positive_code_lookup_prefixentryright) + (dst_positive_scale_lookup_prefixentryright)) + ((dst_positive_scale_lookup_prefixentryright) + (dst_positive_scale_lookup_prefixentryright))) + (((dst_negative_code_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)) * S ((dst_negative_code_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)) + ((dst_negative_scale_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)))) * S ((((dst_positive_code_lookup_prefixentryright) + (dst_positive_scale_lookup_prefixentryright)) * S ((dst_positive_code_lookup_prefixentryright) + (dst_positive_scale_lookup_prefixentryright)) + ((dst_positive_scale_lookup_prefixentryright) + (dst_positive_scale_lookup_prefixentryright))) + (((dst_negative_code_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)) * S ((dst_negative_code_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)) + ((dst_negative_scale_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)))) + ((((dst_negative_code_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)) * S ((dst_negative_code_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)) + ((dst_negative_scale_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright))) + (((dst_negative_code_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)) * S ((dst_negative_code_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)) + ((dst_negative_scale_lookup_prefixentryright) + (dst_negative_scale_lookup_prefixentryright)))))) /\ (((((exists ff_h_pvs_lookup_prefixentryrightpositive. ff_h_pvs_lookup_prefixentryrightpositive + S (dst_positive_lookup_prefixentryright) = S ((S (dc_quotient_lookup_prefixentry)) * dst_positive_scale_lookup_prefixentryright)) /\ exists ff_q_pvs_lookup_prefixentryrightpositive. dst_positive_code_lookup_prefixentryright = ff_q_pvs_lookup_prefixentryrightpositive * S ((S (dc_quotient_lookup_prefixentry)) * dst_positive_scale_lookup_prefixentryright) + (dst_positive_lookup_prefixentryright))) /\ (((((exists ff_h_pvs_lookup_prefixentryrightnegative. ff_h_pvs_lookup_prefixentryrightnegative + S (dst_negative_lookup_prefixentryright) = S ((S (dc_quotient_lookup_prefixentry)) * dst_negative_scale_lookup_prefixentryright)) /\ exists ff_q_pvs_lookup_prefixentryrightnegative. dst_negative_code_lookup_prefixentryright = ff_q_pvs_lookup_prefixentryrightnegative * S ((S (dc_quotient_lookup_prefixentry)) * dst_negative_scale_lookup_prefixentryright) + (dst_negative_lookup_prefixentryright))) /\ (exists ge_balance_positive_lookup_prefixentryrightvalue ge_balance_negative_lookup_prefixentryrightvalue. (((((dc_right_lookup_prefixentry) = 2 * (ge_balance_positive_lookup_prefixentryrightvalue) /\ (ge_balance_negative_lookup_prefixentryrightvalue) = 0) \/ exists ge_signed_half_lookup_prefixentryrightvaluedecode. (((dc_right_lookup_prefixentry) = 2 * ge_signed_half_lookup_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_lookup_prefixentryrightvalue) = 0) /\ (ge_balance_negative_lookup_prefixentryrightvalue) = S ge_signed_half_lookup_prefixentryrightvaluedecode))) /\ ((dst_positive_lookup_prefixentryright) + ge_balance_negative_lookup_prefixentryrightvalue = (dst_negative_lookup_prefixentryright) + ge_balance_positive_lookup_prefixentryrightvalue))))))))) /\ (exists sto_ap_lookup_prefixentryproduct sto_an_lookup_prefixentryproduct sto_bp_lookup_prefixentryproduct sto_bn_lookup_prefixentryproduct sto_cp_lookup_prefixentryproduct sto_cn_lookup_prefixentryproduct. (((((dc_left_lookup_prefixentry) = 2 * (sto_ap_lookup_prefixentryproduct) /\ (sto_an_lookup_prefixentryproduct) = 0) \/ exists ge_signed_half_lookup_prefixentryproductleft. (((dc_left_lookup_prefixentry) = 2 * ge_signed_half_lookup_prefixentryproductleft + 1 /\ (sto_ap_lookup_prefixentryproduct) = 0) /\ (sto_an_lookup_prefixentryproduct) = S ge_signed_half_lookup_prefixentryproductleft))) /\ ((((((dc_right_lookup_prefixentry) = 2 * (sto_bp_lookup_prefixentryproduct) /\ (sto_bn_lookup_prefixentryproduct) = 0) \/ exists ge_signed_half_lookup_prefixentryproductright. (((dc_right_lookup_prefixentry) = 2 * ge_signed_half_lookup_prefixentryproductright + 1 /\ (sto_bp_lookup_prefixentryproduct) = 0) /\ (sto_bn_lookup_prefixentryproduct) = S ge_signed_half_lookup_prefixentryproductright))) /\ ((((((dc_value_lookup_prefix) = 2 * (sto_cp_lookup_prefixentryproduct) /\ (sto_cn_lookup_prefixentryproduct) = 0) \/ exists ge_signed_half_lookup_prefixentryproductoutput. (((dc_value_lookup_prefix) = 2 * ge_signed_half_lookup_prefixentryproductoutput + 1 /\ (sto_cp_lookup_prefixentryproduct) = 0) /\ (sto_cn_lookup_prefixentryproduct) = S ge_signed_half_lookup_prefixentryproductoutput))) /\ ((sto_ap_lookup_prefixentryproduct * sto_bp_lookup_prefixentryproduct + sto_an_lookup_prefixentryproduct * sto_bn_lookup_prefixentryproduct) + sto_cn_lookup_prefixentryproduct = (sto_ap_lookup_prefixentryproduct * sto_bn_lookup_prefixentryproduct + sto_an_lookup_prefixentryproduct * sto_bp_lookup_prefixentryproduct) + sto_cp_lookup_prefixentryproduct))))))))))))))) \/ ((((dc_index_lookup_prefix)=0 \/ ~(exists pvs_factor_lookup_prefixentrynondivisor. (n) = (dc_index_lookup_prefix) * pvs_factor_lookup_prefixentrynondivisor)) /\ ((dc_value_lookup_prefix)=0))))))) -> (exists pvs_le_gap_lookup_bound. pvs_le_gap_lookup_bound + (d) = (l)) -> (exists dst_positive_code_lookup_entry dst_positive_scale_lookup_entry dst_negative_code_lookup_entry dst_negative_scale_lookup_entry dst_positive_lookup_entry dst_negative_lookup_entry. (((M) = (((((dst_positive_code_lookup_entry) + (dst_positive_scale_lookup_entry)) * S ((dst_positive_code_lookup_entry) + (dst_positive_scale_lookup_entry)) + ((dst_positive_scale_lookup_entry) + (dst_positive_scale_lookup_entry))) + (((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) * S ((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) + ((dst_negative_scale_lookup_entry) + (dst_negative_scale_lookup_entry)))) * S ((((dst_positive_code_lookup_entry) + (dst_positive_scale_lookup_entry)) * S ((dst_positive_code_lookup_entry) + (dst_positive_scale_lookup_entry)) + ((dst_positive_scale_lookup_entry) + (dst_positive_scale_lookup_entry))) + (((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) * S ((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) + ((dst_negative_scale_lookup_entry) + (dst_negative_scale_lookup_entry)))) + ((((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) * S ((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) + ((dst_negative_scale_lookup_entry) + (dst_negative_scale_lookup_entry))) + (((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) * S ((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) + ((dst_negative_scale_lookup_entry) + (dst_negative_scale_lookup_entry)))))) /\ (((((exists ff_h_pvs_lookup_entrypositive. ff_h_pvs_lookup_entrypositive + S (dst_positive_lookup_entry) = S ((S (d)) * dst_positive_scale_lookup_entry)) /\ exists ff_q_pvs_lookup_entrypositive. dst_positive_code_lookup_entry = ff_q_pvs_lookup_entrypositive * S ((S (d)) * dst_positive_scale_lookup_entry) + (dst_positive_lookup_entry))) /\ (((((exists ff_h_pvs_lookup_entrynegative. ff_h_pvs_lookup_entrynegative + S (dst_negative_lookup_entry) = S ((S (d)) * dst_negative_scale_lookup_entry)) /\ exists ff_q_pvs_lookup_entrynegative. dst_negative_code_lookup_entry = ff_q_pvs_lookup_entrynegative * S ((S (d)) * dst_negative_scale_lookup_entry) + (dst_negative_lookup_entry))) /\ (exists ge_balance_positive_lookup_entryvalue ge_balance_negative_lookup_entryvalue. (((((z) = 2 * (ge_balance_positive_lookup_entryvalue) /\ (ge_balance_negative_lookup_entryvalue) = 0) \/ exists ge_signed_half_lookup_entryvaluedecode. (((z) = 2 * ge_signed_half_lookup_entryvaluedecode + 1 /\ (ge_balance_positive_lookup_entryvalue) = 0) /\ (ge_balance_negative_lookup_entryvalue) = S ge_signed_half_lookup_entryvaluedecode))) /\ ((dst_positive_lookup_entry) + ge_balance_negative_lookup_entryvalue = (dst_negative_lookup_entry) + ge_balance_positive_lookup_entryvalue))))))))) -> ((((~((d)=0)) /\ (exists dc_quotient_lookup_result dc_left_lookup_result dc_right_lookup_result. (((n)=(d)*dc_quotient_lookup_result) /\ (((exists dst_positive_code_lookup_resultleft dst_positive_scale_lookup_resultleft dst_negative_code_lookup_resultleft dst_negative_scale_lookup_resultleft dst_positive_lookup_resultleft dst_negative_lookup_resultleft. (((F) = (((((dst_positive_code_lookup_resultleft) + (dst_positive_scale_lookup_resultleft)) * S ((dst_positive_code_lookup_resultleft) + (dst_positive_scale_lookup_resultleft)) + ((dst_positive_scale_lookup_resultleft) + (dst_positive_scale_lookup_resultleft))) + (((dst_negative_code_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)) * S ((dst_negative_code_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)) + ((dst_negative_scale_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)))) * S ((((dst_positive_code_lookup_resultleft) + (dst_positive_scale_lookup_resultleft)) * S ((dst_positive_code_lookup_resultleft) + (dst_positive_scale_lookup_resultleft)) + ((dst_positive_scale_lookup_resultleft) + (dst_positive_scale_lookup_resultleft))) + (((dst_negative_code_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)) * S ((dst_negative_code_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)) + ((dst_negative_scale_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)))) + ((((dst_negative_code_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)) * S ((dst_negative_code_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)) + ((dst_negative_scale_lookup_resultleft) + (dst_negative_scale_lookup_resultleft))) + (((dst_negative_code_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)) * S ((dst_negative_code_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)) + ((dst_negative_scale_lookup_resultleft) + (dst_negative_scale_lookup_resultleft)))))) /\ (((((exists ff_h_pvs_lookup_resultleftpositive. ff_h_pvs_lookup_resultleftpositive + S (dst_positive_lookup_resultleft) = S ((S (d)) * dst_positive_scale_lookup_resultleft)) /\ exists ff_q_pvs_lookup_resultleftpositive. dst_positive_code_lookup_resultleft = ff_q_pvs_lookup_resultleftpositive * S ((S (d)) * dst_positive_scale_lookup_resultleft) + (dst_positive_lookup_resultleft))) /\ (((((exists ff_h_pvs_lookup_resultleftnegative. ff_h_pvs_lookup_resultleftnegative + S (dst_negative_lookup_resultleft) = S ((S (d)) * dst_negative_scale_lookup_resultleft)) /\ exists ff_q_pvs_lookup_resultleftnegative. dst_negative_code_lookup_resultleft = ff_q_pvs_lookup_resultleftnegative * S ((S (d)) * dst_negative_scale_lookup_resultleft) + (dst_negative_lookup_resultleft))) /\ (exists ge_balance_positive_lookup_resultleftvalue ge_balance_negative_lookup_resultleftvalue. (((((dc_left_lookup_result) = 2 * (ge_balance_positive_lookup_resultleftvalue) /\ (ge_balance_negative_lookup_resultleftvalue) = 0) \/ exists ge_signed_half_lookup_resultleftvaluedecode. (((dc_left_lookup_result) = 2 * ge_signed_half_lookup_resultleftvaluedecode + 1 /\ (ge_balance_positive_lookup_resultleftvalue) = 0) /\ (ge_balance_negative_lookup_resultleftvalue) = S ge_signed_half_lookup_resultleftvaluedecode))) /\ ((dst_positive_lookup_resultleft) + ge_balance_negative_lookup_resultleftvalue = (dst_negative_lookup_resultleft) + ge_balance_positive_lookup_resultleftvalue))))))))) /\ (((exists dst_positive_code_lookup_resultright dst_positive_scale_lookup_resultright dst_negative_code_lookup_resultright dst_negative_scale_lookup_resultright dst_positive_lookup_resultright dst_negative_lookup_resultright. (((G) = (((((dst_positive_code_lookup_resultright) + (dst_positive_scale_lookup_resultright)) * S ((dst_positive_code_lookup_resultright) + (dst_positive_scale_lookup_resultright)) + ((dst_positive_scale_lookup_resultright) + (dst_positive_scale_lookup_resultright))) + (((dst_negative_code_lookup_resultright) + (dst_negative_scale_lookup_resultright)) * S ((dst_negative_code_lookup_resultright) + (dst_negative_scale_lookup_resultright)) + ((dst_negative_scale_lookup_resultright) + (dst_negative_scale_lookup_resultright)))) * S ((((dst_positive_code_lookup_resultright) + (dst_positive_scale_lookup_resultright)) * S ((dst_positive_code_lookup_resultright) + (dst_positive_scale_lookup_resultright)) + ((dst_positive_scale_lookup_resultright) + (dst_positive_scale_lookup_resultright))) + (((dst_negative_code_lookup_resultright) + (dst_negative_scale_lookup_resultright)) * S ((dst_negative_code_lookup_resultright) + (dst_negative_scale_lookup_resultright)) + ((dst_negative_scale_lookup_resultright) + (dst_negative_scale_lookup_resultright)))) + ((((dst_negative_code_lookup_resultright) + (dst_negative_scale_lookup_resultright)) * S ((dst_negative_code_lookup_resultright) + (dst_negative_scale_lookup_resultright)) + ((dst_negative_scale_lookup_resultright) + (dst_negative_scale_lookup_resultright))) + (((dst_negative_code_lookup_resultright) + (dst_negative_scale_lookup_resultright)) * S ((dst_negative_code_lookup_resultright) + (dst_negative_scale_lookup_resultright)) + ((dst_negative_scale_lookup_resultright) + (dst_negative_scale_lookup_resultright)))))) /\ (((((exists ff_h_pvs_lookup_resultrightpositive. ff_h_pvs_lookup_resultrightpositive + S (dst_positive_lookup_resultright) = S ((S (dc_quotient_lookup_result)) * dst_positive_scale_lookup_resultright)) /\ exists ff_q_pvs_lookup_resultrightpositive. dst_positive_code_lookup_resultright = ff_q_pvs_lookup_resultrightpositive * S ((S (dc_quotient_lookup_result)) * dst_positive_scale_lookup_resultright) + (dst_positive_lookup_resultright))) /\ (((((exists ff_h_pvs_lookup_resultrightnegative. ff_h_pvs_lookup_resultrightnegative + S (dst_negative_lookup_resultright) = S ((S (dc_quotient_lookup_result)) * dst_negative_scale_lookup_resultright)) /\ exists ff_q_pvs_lookup_resultrightnegative. dst_negative_code_lookup_resultright = ff_q_pvs_lookup_resultrightnegative * S ((S (dc_quotient_lookup_result)) * dst_negative_scale_lookup_resultright) + (dst_negative_lookup_resultright))) /\ (exists ge_balance_positive_lookup_resultrightvalue ge_balance_negative_lookup_resultrightvalue. (((((dc_right_lookup_result) = 2 * (ge_balance_positive_lookup_resultrightvalue) /\ (ge_balance_negative_lookup_resultrightvalue) = 0) \/ exists ge_signed_half_lookup_resultrightvaluedecode. (((dc_right_lookup_result) = 2 * ge_signed_half_lookup_resultrightvaluedecode + 1 /\ (ge_balance_positive_lookup_resultrightvalue) = 0) /\ (ge_balance_negative_lookup_resultrightvalue) = S ge_signed_half_lookup_resultrightvaluedecode))) /\ ((dst_positive_lookup_resultright) + ge_balance_negative_lookup_resultrightvalue = (dst_negative_lookup_resultright) + ge_balance_positive_lookup_resultrightvalue))))))))) /\ (exists sto_ap_lookup_resultproduct sto_an_lookup_resultproduct sto_bp_lookup_resultproduct sto_bn_lookup_resultproduct sto_cp_lookup_resultproduct sto_cn_lookup_resultproduct. (((((dc_left_lookup_result) = 2 * (sto_ap_lookup_resultproduct) /\ (sto_an_lookup_resultproduct) = 0) \/ exists ge_signed_half_lookup_resultproductleft. (((dc_left_lookup_result) = 2 * ge_signed_half_lookup_resultproductleft + 1 /\ (sto_ap_lookup_resultproduct) = 0) /\ (sto_an_lookup_resultproduct) = S ge_signed_half_lookup_resultproductleft))) /\ ((((((dc_right_lookup_result) = 2 * (sto_bp_lookup_resultproduct) /\ (sto_bn_lookup_resultproduct) = 0) \/ exists ge_signed_half_lookup_resultproductright. (((dc_right_lookup_result) = 2 * ge_signed_half_lookup_resultproductright + 1 /\ (sto_bp_lookup_resultproduct) = 0) /\ (sto_bn_lookup_resultproduct) = S ge_signed_half_lookup_resultproductright))) /\ ((((((z) = 2 * (sto_cp_lookup_resultproduct) /\ (sto_cn_lookup_resultproduct) = 0) \/ exists ge_signed_half_lookup_resultproductoutput. (((z) = 2 * ge_signed_half_lookup_resultproductoutput + 1 /\ (sto_cp_lookup_resultproduct) = 0) /\ (sto_cn_lookup_resultproduct) = S ge_signed_half_lookup_resultproductoutput))) /\ ((sto_ap_lookup_resultproduct * sto_bp_lookup_resultproduct + sto_an_lookup_resultproduct * sto_bn_lookup_resultproduct) + sto_cn_lookup_resultproduct = (sto_ap_lookup_resultproduct * sto_bn_lookup_resultproduct + sto_an_lookup_resultproduct * sto_bp_lookup_resultproduct) + sto_cp_lookup_resultproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_lookup_resultnondivisor. (n) = (d) * pvs_factor_lookup_resultnondivisor)) /\ ((z)=0))))