dirichlet_convolution_prefix_restrict

Exact expanded first-order arithmetic statement

forall F G n l k M. (((exists dst_positive_code_restrict_sourcetable dst_positive_scale_restrict_sourcetable dst_negative_code_restrict_sourcetable dst_negative_scale_restrict_sourcetable. (((M) = (((((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) * S ((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) + ((dst_positive_scale_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable))) + (((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)))) * S ((((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) * S ((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) + ((dst_positive_scale_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable))) + (((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)))) + ((((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable))) + (((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)))))) /\ (forall dst_index_restrict_sourcetable. (exists pvs_le_gap_restrict_sourcetabledomain. pvs_le_gap_restrict_sourcetabledomain + (dst_index_restrict_sourcetable) = (l)) -> exists dst_positive_restrict_sourcetable dst_negative_restrict_sourcetable dst_value_restrict_sourcetable. ((((exists ff_h_pvs_restrict_sourcetableentrypositive. ff_h_pvs_restrict_sourcetableentrypositive + S (dst_positive_restrict_sourcetable) = S ((S (dst_index_restrict_sourcetable)) * dst_positive_scale_restrict_sourcetable)) /\ exists ff_q_pvs_restrict_sourcetableentrypositive. dst_positive_code_restrict_sourcetable = ff_q_pvs_restrict_sourcetableentrypositive * S ((S (dst_index_restrict_sourcetable)) * dst_positive_scale_restrict_sourcetable) + (dst_positive_restrict_sourcetable))) /\ (((((exists ff_h_pvs_restrict_sourcetableentrynegative. ff_h_pvs_restrict_sourcetableentrynegative + S (dst_negative_restrict_sourcetable) = S ((S (dst_index_restrict_sourcetable)) * dst_negative_scale_restrict_sourcetable)) /\ exists ff_q_pvs_restrict_sourcetableentrynegative. dst_negative_code_restrict_sourcetable = ff_q_pvs_restrict_sourcetableentrynegative * S ((S (dst_index_restrict_sourcetable)) * dst_negative_scale_restrict_sourcetable) + (dst_negative_restrict_sourcetable))) /\ (exists ge_balance_positive_restrict_sourcetableentryvalue ge_balance_negative_restrict_sourcetableentryvalue. (((((dst_value_restrict_sourcetable) = 2 * (ge_balance_positive_restrict_sourcetableentryvalue) /\ (ge_balance_negative_restrict_sourcetableentryvalue) = 0) \/ exists ge_signed_half_restrict_sourcetableentryvaluedecode. (((dst_value_restrict_sourcetable) = 2 * ge_signed_half_restrict_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_sourcetableentryvalue) = 0) /\ (ge_balance_negative_restrict_sourcetableentryvalue) = S ge_signed_half_restrict_sourcetableentryvaluedecode))) /\ ((dst_positive_restrict_sourcetable) + ge_balance_negative_restrict_sourcetableentryvalue = (dst_negative_restrict_sourcetable) + ge_balance_positive_restrict_sourcetableentryvalue))))))))) /\ (forall dc_index_restrict_source dc_value_restrict_source. (exists pvs_le_gap_restrict_sourcedomain. pvs_le_gap_restrict_sourcedomain + (dc_index_restrict_source) = (l)) -> (exists dst_positive_code_restrict_sourcelookup dst_positive_scale_restrict_sourcelookup dst_negative_code_restrict_sourcelookup dst_negative_scale_restrict_sourcelookup dst_positive_restrict_sourcelookup dst_negative_restrict_sourcelookup. (((M) = (((((dst_positive_code_restrict_sourcelookup) + (dst_positive_scale_restrict_sourcelookup)) * S ((dst_positive_code_restrict_sourcelookup) + (dst_positive_scale_restrict_sourcelookup)) + ((dst_positive_scale_restrict_sourcelookup) + (dst_positive_scale_restrict_sourcelookup))) + (((dst_negative_code_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)) * S ((dst_negative_code_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)) + ((dst_negative_scale_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)))) * S ((((dst_positive_code_restrict_sourcelookup) + (dst_positive_scale_restrict_sourcelookup)) * S ((dst_positive_code_restrict_sourcelookup) + (dst_positive_scale_restrict_sourcelookup)) + ((dst_positive_scale_restrict_sourcelookup) + (dst_positive_scale_restrict_sourcelookup))) + (((dst_negative_code_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)) * S ((dst_negative_code_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)) + ((dst_negative_scale_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)))) + ((((dst_negative_code_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)) * S ((dst_negative_code_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)) + ((dst_negative_scale_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup))) + (((dst_negative_code_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)) * S ((dst_negative_code_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)) + ((dst_negative_scale_restrict_sourcelookup) + (dst_negative_scale_restrict_sourcelookup)))))) /\ (((((exists ff_h_pvs_restrict_sourcelookuppositive. ff_h_pvs_restrict_sourcelookuppositive + S (dst_positive_restrict_sourcelookup) = S ((S (dc_index_restrict_source)) * dst_positive_scale_restrict_sourcelookup)) /\ exists ff_q_pvs_restrict_sourcelookuppositive. dst_positive_code_restrict_sourcelookup = ff_q_pvs_restrict_sourcelookuppositive * S ((S (dc_index_restrict_source)) * dst_positive_scale_restrict_sourcelookup) + (dst_positive_restrict_sourcelookup))) /\ (((((exists ff_h_pvs_restrict_sourcelookupnegative. ff_h_pvs_restrict_sourcelookupnegative + S (dst_negative_restrict_sourcelookup) = S ((S (dc_index_restrict_source)) * dst_negative_scale_restrict_sourcelookup)) /\ exists ff_q_pvs_restrict_sourcelookupnegative. dst_negative_code_restrict_sourcelookup = ff_q_pvs_restrict_sourcelookupnegative * S ((S (dc_index_restrict_source)) * dst_negative_scale_restrict_sourcelookup) + (dst_negative_restrict_sourcelookup))) /\ (exists ge_balance_positive_restrict_sourcelookupvalue ge_balance_negative_restrict_sourcelookupvalue. (((((dc_value_restrict_source) = 2 * (ge_balance_positive_restrict_sourcelookupvalue) /\ (ge_balance_negative_restrict_sourcelookupvalue) = 0) \/ exists ge_signed_half_restrict_sourcelookupvaluedecode. (((dc_value_restrict_source) = 2 * ge_signed_half_restrict_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_restrict_sourcelookupvalue) = 0) /\ (ge_balance_negative_restrict_sourcelookupvalue) = S ge_signed_half_restrict_sourcelookupvaluedecode))) /\ ((dst_positive_restrict_sourcelookup) + ge_balance_negative_restrict_sourcelookupvalue = (dst_negative_restrict_sourcelookup) + ge_balance_positive_restrict_sourcelookupvalue))))))))) -> ((((~((dc_index_restrict_source)=0)) /\ (exists dc_quotient_restrict_sourceentry dc_left_restrict_sourceentry dc_right_restrict_sourceentry. (((n)=(dc_index_restrict_source)*dc_quotient_restrict_sourceentry) /\ (((exists dst_positive_code_restrict_sourceentryleft dst_positive_scale_restrict_sourceentryleft dst_negative_code_restrict_sourceentryleft dst_negative_scale_restrict_sourceentryleft dst_positive_restrict_sourceentryleft dst_negative_restrict_sourceentryleft. (((F) = (((((dst_positive_code_restrict_sourceentryleft) + (dst_positive_scale_restrict_sourceentryleft)) * S ((dst_positive_code_restrict_sourceentryleft) + (dst_positive_scale_restrict_sourceentryleft)) + ((dst_positive_scale_restrict_sourceentryleft) + (dst_positive_scale_restrict_sourceentryleft))) + (((dst_negative_code_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)) * S ((dst_negative_code_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)) + ((dst_negative_scale_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)))) * S ((((dst_positive_code_restrict_sourceentryleft) + (dst_positive_scale_restrict_sourceentryleft)) * S ((dst_positive_code_restrict_sourceentryleft) + (dst_positive_scale_restrict_sourceentryleft)) + ((dst_positive_scale_restrict_sourceentryleft) + (dst_positive_scale_restrict_sourceentryleft))) + (((dst_negative_code_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)) * S ((dst_negative_code_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)) + ((dst_negative_scale_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)))) + ((((dst_negative_code_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)) * S ((dst_negative_code_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)) + ((dst_negative_scale_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft))) + (((dst_negative_code_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)) * S ((dst_negative_code_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)) + ((dst_negative_scale_restrict_sourceentryleft) + (dst_negative_scale_restrict_sourceentryleft)))))) /\ (((((exists ff_h_pvs_restrict_sourceentryleftpositive. ff_h_pvs_restrict_sourceentryleftpositive + S (dst_positive_restrict_sourceentryleft) = S ((S (dc_index_restrict_source)) * dst_positive_scale_restrict_sourceentryleft)) /\ exists ff_q_pvs_restrict_sourceentryleftpositive. dst_positive_code_restrict_sourceentryleft = ff_q_pvs_restrict_sourceentryleftpositive * S ((S (dc_index_restrict_source)) * dst_positive_scale_restrict_sourceentryleft) + (dst_positive_restrict_sourceentryleft))) /\ (((((exists ff_h_pvs_restrict_sourceentryleftnegative. ff_h_pvs_restrict_sourceentryleftnegative + S (dst_negative_restrict_sourceentryleft) = S ((S (dc_index_restrict_source)) * dst_negative_scale_restrict_sourceentryleft)) /\ exists ff_q_pvs_restrict_sourceentryleftnegative. dst_negative_code_restrict_sourceentryleft = ff_q_pvs_restrict_sourceentryleftnegative * S ((S (dc_index_restrict_source)) * dst_negative_scale_restrict_sourceentryleft) + (dst_negative_restrict_sourceentryleft))) /\ (exists ge_balance_positive_restrict_sourceentryleftvalue ge_balance_negative_restrict_sourceentryleftvalue. (((((dc_left_restrict_sourceentry) = 2 * (ge_balance_positive_restrict_sourceentryleftvalue) /\ (ge_balance_negative_restrict_sourceentryleftvalue) = 0) \/ exists ge_signed_half_restrict_sourceentryleftvaluedecode. (((dc_left_restrict_sourceentry) = 2 * ge_signed_half_restrict_sourceentryleftvaluedecode + 1 /\ (ge_balance_positive_restrict_sourceentryleftvalue) = 0) /\ (ge_balance_negative_restrict_sourceentryleftvalue) = S ge_signed_half_restrict_sourceentryleftvaluedecode))) /\ ((dst_positive_restrict_sourceentryleft) + ge_balance_negative_restrict_sourceentryleftvalue = (dst_negative_restrict_sourceentryleft) + ge_balance_positive_restrict_sourceentryleftvalue))))))))) /\ (((exists dst_positive_code_restrict_sourceentryright dst_positive_scale_restrict_sourceentryright dst_negative_code_restrict_sourceentryright dst_negative_scale_restrict_sourceentryright dst_positive_restrict_sourceentryright dst_negative_restrict_sourceentryright. (((G) = (((((dst_positive_code_restrict_sourceentryright) + (dst_positive_scale_restrict_sourceentryright)) * S ((dst_positive_code_restrict_sourceentryright) + (dst_positive_scale_restrict_sourceentryright)) + ((dst_positive_scale_restrict_sourceentryright) + (dst_positive_scale_restrict_sourceentryright))) + (((dst_negative_code_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)) * S ((dst_negative_code_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)) + ((dst_negative_scale_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)))) * S ((((dst_positive_code_restrict_sourceentryright) + (dst_positive_scale_restrict_sourceentryright)) * S ((dst_positive_code_restrict_sourceentryright) + (dst_positive_scale_restrict_sourceentryright)) + ((dst_positive_scale_restrict_sourceentryright) + (dst_positive_scale_restrict_sourceentryright))) + (((dst_negative_code_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)) * S ((dst_negative_code_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)) + ((dst_negative_scale_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)))) + ((((dst_negative_code_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)) * S ((dst_negative_code_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)) + ((dst_negative_scale_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright))) + (((dst_negative_code_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)) * S ((dst_negative_code_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)) + ((dst_negative_scale_restrict_sourceentryright) + (dst_negative_scale_restrict_sourceentryright)))))) /\ (((((exists ff_h_pvs_restrict_sourceentryrightpositive. ff_h_pvs_restrict_sourceentryrightpositive + S (dst_positive_restrict_sourceentryright) = S ((S (dc_quotient_restrict_sourceentry)) * dst_positive_scale_restrict_sourceentryright)) /\ exists ff_q_pvs_restrict_sourceentryrightpositive. dst_positive_code_restrict_sourceentryright = ff_q_pvs_restrict_sourceentryrightpositive * S ((S (dc_quotient_restrict_sourceentry)) * dst_positive_scale_restrict_sourceentryright) + (dst_positive_restrict_sourceentryright))) /\ (((((exists ff_h_pvs_restrict_sourceentryrightnegative. ff_h_pvs_restrict_sourceentryrightnegative + S (dst_negative_restrict_sourceentryright) = S ((S (dc_quotient_restrict_sourceentry)) * dst_negative_scale_restrict_sourceentryright)) /\ exists ff_q_pvs_restrict_sourceentryrightnegative. dst_negative_code_restrict_sourceentryright = ff_q_pvs_restrict_sourceentryrightnegative * S ((S (dc_quotient_restrict_sourceentry)) * dst_negative_scale_restrict_sourceentryright) + (dst_negative_restrict_sourceentryright))) /\ (exists ge_balance_positive_restrict_sourceentryrightvalue ge_balance_negative_restrict_sourceentryrightvalue. (((((dc_right_restrict_sourceentry) = 2 * (ge_balance_positive_restrict_sourceentryrightvalue) /\ (ge_balance_negative_restrict_sourceentryrightvalue) = 0) \/ exists ge_signed_half_restrict_sourceentryrightvaluedecode. (((dc_right_restrict_sourceentry) = 2 * ge_signed_half_restrict_sourceentryrightvaluedecode + 1 /\ (ge_balance_positive_restrict_sourceentryrightvalue) = 0) /\ (ge_balance_negative_restrict_sourceentryrightvalue) = S ge_signed_half_restrict_sourceentryrightvaluedecode))) /\ ((dst_positive_restrict_sourceentryright) + ge_balance_negative_restrict_sourceentryrightvalue = (dst_negative_restrict_sourceentryright) + ge_balance_positive_restrict_sourceentryrightvalue))))))))) /\ (exists sto_ap_restrict_sourceentryproduct sto_an_restrict_sourceentryproduct sto_bp_restrict_sourceentryproduct sto_bn_restrict_sourceentryproduct sto_cp_restrict_sourceentryproduct sto_cn_restrict_sourceentryproduct. (((((dc_left_restrict_sourceentry) = 2 * (sto_ap_restrict_sourceentryproduct) /\ (sto_an_restrict_sourceentryproduct) = 0) \/ exists ge_signed_half_restrict_sourceentryproductleft. (((dc_left_restrict_sourceentry) = 2 * ge_signed_half_restrict_sourceentryproductleft + 1 /\ (sto_ap_restrict_sourceentryproduct) = 0) /\ (sto_an_restrict_sourceentryproduct) = S ge_signed_half_restrict_sourceentryproductleft))) /\ ((((((dc_right_restrict_sourceentry) = 2 * (sto_bp_restrict_sourceentryproduct) /\ (sto_bn_restrict_sourceentryproduct) = 0) \/ exists ge_signed_half_restrict_sourceentryproductright. (((dc_right_restrict_sourceentry) = 2 * ge_signed_half_restrict_sourceentryproductright + 1 /\ (sto_bp_restrict_sourceentryproduct) = 0) /\ (sto_bn_restrict_sourceentryproduct) = S ge_signed_half_restrict_sourceentryproductright))) /\ ((((((dc_value_restrict_source) = 2 * (sto_cp_restrict_sourceentryproduct) /\ (sto_cn_restrict_sourceentryproduct) = 0) \/ exists ge_signed_half_restrict_sourceentryproductoutput. (((dc_value_restrict_source) = 2 * ge_signed_half_restrict_sourceentryproductoutput + 1 /\ (sto_cp_restrict_sourceentryproduct) = 0) /\ (sto_cn_restrict_sourceentryproduct) = S ge_signed_half_restrict_sourceentryproductoutput))) /\ ((sto_ap_restrict_sourceentryproduct * sto_bp_restrict_sourceentryproduct + sto_an_restrict_sourceentryproduct * sto_bn_restrict_sourceentryproduct) + sto_cn_restrict_sourceentryproduct = (sto_ap_restrict_sourceentryproduct * sto_bn_restrict_sourceentryproduct + sto_an_restrict_sourceentryproduct * sto_bp_restrict_sourceentryproduct) + sto_cp_restrict_sourceentryproduct))))))))))))))) \/ ((((dc_index_restrict_source)=0 \/ ~(exists pvs_factor_restrict_sourceentrynondivisor. (n) = (dc_index_restrict_source) * pvs_factor_restrict_sourceentrynondivisor)) /\ ((dc_value_restrict_source)=0))))))) -> (exists pvs_le_gap_restrict_bound. pvs_le_gap_restrict_bound + (k) = (l)) -> (((exists dst_positive_code_restrict_resulttable dst_positive_scale_restrict_resulttable dst_negative_code_restrict_resulttable dst_negative_scale_restrict_resulttable. (((M) = (((((dst_positive_code_restrict_resulttable) + (dst_positive_scale_restrict_resulttable)) * S ((dst_positive_code_restrict_resulttable) + (dst_positive_scale_restrict_resulttable)) + ((dst_positive_scale_restrict_resulttable) + (dst_positive_scale_restrict_resulttable))) + (((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) * S ((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) + ((dst_negative_scale_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)))) * S ((((dst_positive_code_restrict_resulttable) + (dst_positive_scale_restrict_resulttable)) * S ((dst_positive_code_restrict_resulttable) + (dst_positive_scale_restrict_resulttable)) + ((dst_positive_scale_restrict_resulttable) + (dst_positive_scale_restrict_resulttable))) + (((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) * S ((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) + ((dst_negative_scale_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)))) + ((((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) * S ((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) + ((dst_negative_scale_restrict_resulttable) + (dst_negative_scale_restrict_resulttable))) + (((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) * S ((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) + ((dst_negative_scale_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)))))) /\ (forall dst_index_restrict_resulttable. (exists pvs_le_gap_restrict_resulttabledomain. pvs_le_gap_restrict_resulttabledomain + (dst_index_restrict_resulttable) = (k)) -> exists dst_positive_restrict_resulttable dst_negative_restrict_resulttable dst_value_restrict_resulttable. ((((exists ff_h_pvs_restrict_resulttableentrypositive. ff_h_pvs_restrict_resulttableentrypositive + S (dst_positive_restrict_resulttable) = S ((S (dst_index_restrict_resulttable)) * dst_positive_scale_restrict_resulttable)) /\ exists ff_q_pvs_restrict_resulttableentrypositive. dst_positive_code_restrict_resulttable = ff_q_pvs_restrict_resulttableentrypositive * S ((S (dst_index_restrict_resulttable)) * dst_positive_scale_restrict_resulttable) + (dst_positive_restrict_resulttable))) /\ (((((exists ff_h_pvs_restrict_resulttableentrynegative. ff_h_pvs_restrict_resulttableentrynegative + S (dst_negative_restrict_resulttable) = S ((S (dst_index_restrict_resulttable)) * dst_negative_scale_restrict_resulttable)) /\ exists ff_q_pvs_restrict_resulttableentrynegative. dst_negative_code_restrict_resulttable = ff_q_pvs_restrict_resulttableentrynegative * S ((S (dst_index_restrict_resulttable)) * dst_negative_scale_restrict_resulttable) + (dst_negative_restrict_resulttable))) /\ (exists ge_balance_positive_restrict_resulttableentryvalue ge_balance_negative_restrict_resulttableentryvalue. (((((dst_value_restrict_resulttable) = 2 * (ge_balance_positive_restrict_resulttableentryvalue) /\ (ge_balance_negative_restrict_resulttableentryvalue) = 0) \/ exists ge_signed_half_restrict_resulttableentryvaluedecode. (((dst_value_restrict_resulttable) = 2 * ge_signed_half_restrict_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_resulttableentryvalue) = 0) /\ (ge_balance_negative_restrict_resulttableentryvalue) = S ge_signed_half_restrict_resulttableentryvaluedecode))) /\ ((dst_positive_restrict_resulttable) + ge_balance_negative_restrict_resulttableentryvalue = (dst_negative_restrict_resulttable) + ge_balance_positive_restrict_resulttableentryvalue))))))))) /\ (forall dc_index_restrict_result dc_value_restrict_result. (exists pvs_le_gap_restrict_resultdomain. pvs_le_gap_restrict_resultdomain + (dc_index_restrict_result) = (k)) -> (exists dst_positive_code_restrict_resultlookup dst_positive_scale_restrict_resultlookup dst_negative_code_restrict_resultlookup dst_negative_scale_restrict_resultlookup dst_positive_restrict_resultlookup dst_negative_restrict_resultlookup. (((M) = (((((dst_positive_code_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup)) * S ((dst_positive_code_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup)) + ((dst_positive_scale_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup))) + (((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) * S ((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) + ((dst_negative_scale_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)))) * S ((((dst_positive_code_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup)) * S ((dst_positive_code_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup)) + ((dst_positive_scale_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup))) + (((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) * S ((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) + ((dst_negative_scale_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)))) + ((((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) * S ((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) + ((dst_negative_scale_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup))) + (((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) * S ((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) + ((dst_negative_scale_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)))))) /\ (((((exists ff_h_pvs_restrict_resultlookuppositive. ff_h_pvs_restrict_resultlookuppositive + S (dst_positive_restrict_resultlookup) = S ((S (dc_index_restrict_result)) * dst_positive_scale_restrict_resultlookup)) /\ exists ff_q_pvs_restrict_resultlookuppositive. dst_positive_code_restrict_resultlookup = ff_q_pvs_restrict_resultlookuppositive * S ((S (dc_index_restrict_result)) * dst_positive_scale_restrict_resultlookup) + (dst_positive_restrict_resultlookup))) /\ (((((exists ff_h_pvs_restrict_resultlookupnegative. ff_h_pvs_restrict_resultlookupnegative + S (dst_negative_restrict_resultlookup) = S ((S (dc_index_restrict_result)) * dst_negative_scale_restrict_resultlookup)) /\ exists ff_q_pvs_restrict_resultlookupnegative. dst_negative_code_restrict_resultlookup = ff_q_pvs_restrict_resultlookupnegative * S ((S (dc_index_restrict_result)) * dst_negative_scale_restrict_resultlookup) + (dst_negative_restrict_resultlookup))) /\ (exists ge_balance_positive_restrict_resultlookupvalue ge_balance_negative_restrict_resultlookupvalue. (((((dc_value_restrict_result) = 2 * (ge_balance_positive_restrict_resultlookupvalue) /\ (ge_balance_negative_restrict_resultlookupvalue) = 0) \/ exists ge_signed_half_restrict_resultlookupvaluedecode. (((dc_value_restrict_result) = 2 * ge_signed_half_restrict_resultlookupvaluedecode + 1 /\ (ge_balance_positive_restrict_resultlookupvalue) = 0) /\ (ge_balance_negative_restrict_resultlookupvalue) = S ge_signed_half_restrict_resultlookupvaluedecode))) /\ ((dst_positive_restrict_resultlookup) + ge_balance_negative_restrict_resultlookupvalue = (dst_negative_restrict_resultlookup) + ge_balance_positive_restrict_resultlookupvalue))))))))) -> ((((~((dc_index_restrict_result)=0)) /\ (exists dc_quotient_restrict_resultentry dc_left_restrict_resultentry dc_right_restrict_resultentry. (((n)=(dc_index_restrict_result)*dc_quotient_restrict_resultentry) /\ (((exists dst_positive_code_restrict_resultentryleft dst_positive_scale_restrict_resultentryleft dst_negative_code_restrict_resultentryleft dst_negative_scale_restrict_resultentryleft dst_positive_restrict_resultentryleft dst_negative_restrict_resultentryleft. (((F) = (((((dst_positive_code_restrict_resultentryleft) + (dst_positive_scale_restrict_resultentryleft)) * S ((dst_positive_code_restrict_resultentryleft) + (dst_positive_scale_restrict_resultentryleft)) + ((dst_positive_scale_restrict_resultentryleft) + (dst_positive_scale_restrict_resultentryleft))) + (((dst_negative_code_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)) * S ((dst_negative_code_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)) + ((dst_negative_scale_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)))) * S ((((dst_positive_code_restrict_resultentryleft) + (dst_positive_scale_restrict_resultentryleft)) * S ((dst_positive_code_restrict_resultentryleft) + (dst_positive_scale_restrict_resultentryleft)) + ((dst_positive_scale_restrict_resultentryleft) + (dst_positive_scale_restrict_resultentryleft))) + (((dst_negative_code_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)) * S ((dst_negative_code_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)) + ((dst_negative_scale_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)))) + ((((dst_negative_code_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)) * S ((dst_negative_code_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)) + ((dst_negative_scale_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft))) + (((dst_negative_code_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)) * S ((dst_negative_code_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)) + ((dst_negative_scale_restrict_resultentryleft) + (dst_negative_scale_restrict_resultentryleft)))))) /\ (((((exists ff_h_pvs_restrict_resultentryleftpositive. ff_h_pvs_restrict_resultentryleftpositive + S (dst_positive_restrict_resultentryleft) = S ((S (dc_index_restrict_result)) * dst_positive_scale_restrict_resultentryleft)) /\ exists ff_q_pvs_restrict_resultentryleftpositive. dst_positive_code_restrict_resultentryleft = ff_q_pvs_restrict_resultentryleftpositive * S ((S (dc_index_restrict_result)) * dst_positive_scale_restrict_resultentryleft) + (dst_positive_restrict_resultentryleft))) /\ (((((exists ff_h_pvs_restrict_resultentryleftnegative. ff_h_pvs_restrict_resultentryleftnegative + S (dst_negative_restrict_resultentryleft) = S ((S (dc_index_restrict_result)) * dst_negative_scale_restrict_resultentryleft)) /\ exists ff_q_pvs_restrict_resultentryleftnegative. dst_negative_code_restrict_resultentryleft = ff_q_pvs_restrict_resultentryleftnegative * S ((S (dc_index_restrict_result)) * dst_negative_scale_restrict_resultentryleft) + (dst_negative_restrict_resultentryleft))) /\ (exists ge_balance_positive_restrict_resultentryleftvalue ge_balance_negative_restrict_resultentryleftvalue. (((((dc_left_restrict_resultentry) = 2 * (ge_balance_positive_restrict_resultentryleftvalue) /\ (ge_balance_negative_restrict_resultentryleftvalue) = 0) \/ exists ge_signed_half_restrict_resultentryleftvaluedecode. (((dc_left_restrict_resultentry) = 2 * ge_signed_half_restrict_resultentryleftvaluedecode + 1 /\ (ge_balance_positive_restrict_resultentryleftvalue) = 0) /\ (ge_balance_negative_restrict_resultentryleftvalue) = S ge_signed_half_restrict_resultentryleftvaluedecode))) /\ ((dst_positive_restrict_resultentryleft) + ge_balance_negative_restrict_resultentryleftvalue = (dst_negative_restrict_resultentryleft) + ge_balance_positive_restrict_resultentryleftvalue))))))))) /\ (((exists dst_positive_code_restrict_resultentryright dst_positive_scale_restrict_resultentryright dst_negative_code_restrict_resultentryright dst_negative_scale_restrict_resultentryright dst_positive_restrict_resultentryright dst_negative_restrict_resultentryright. (((G) = (((((dst_positive_code_restrict_resultentryright) + (dst_positive_scale_restrict_resultentryright)) * S ((dst_positive_code_restrict_resultentryright) + (dst_positive_scale_restrict_resultentryright)) + ((dst_positive_scale_restrict_resultentryright) + (dst_positive_scale_restrict_resultentryright))) + (((dst_negative_code_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)) * S ((dst_negative_code_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)) + ((dst_negative_scale_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)))) * S ((((dst_positive_code_restrict_resultentryright) + (dst_positive_scale_restrict_resultentryright)) * S ((dst_positive_code_restrict_resultentryright) + (dst_positive_scale_restrict_resultentryright)) + ((dst_positive_scale_restrict_resultentryright) + (dst_positive_scale_restrict_resultentryright))) + (((dst_negative_code_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)) * S ((dst_negative_code_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)) + ((dst_negative_scale_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)))) + ((((dst_negative_code_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)) * S ((dst_negative_code_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)) + ((dst_negative_scale_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright))) + (((dst_negative_code_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)) * S ((dst_negative_code_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)) + ((dst_negative_scale_restrict_resultentryright) + (dst_negative_scale_restrict_resultentryright)))))) /\ (((((exists ff_h_pvs_restrict_resultentryrightpositive. ff_h_pvs_restrict_resultentryrightpositive + S (dst_positive_restrict_resultentryright) = S ((S (dc_quotient_restrict_resultentry)) * dst_positive_scale_restrict_resultentryright)) /\ exists ff_q_pvs_restrict_resultentryrightpositive. dst_positive_code_restrict_resultentryright = ff_q_pvs_restrict_resultentryrightpositive * S ((S (dc_quotient_restrict_resultentry)) * dst_positive_scale_restrict_resultentryright) + (dst_positive_restrict_resultentryright))) /\ (((((exists ff_h_pvs_restrict_resultentryrightnegative. ff_h_pvs_restrict_resultentryrightnegative + S (dst_negative_restrict_resultentryright) = S ((S (dc_quotient_restrict_resultentry)) * dst_negative_scale_restrict_resultentryright)) /\ exists ff_q_pvs_restrict_resultentryrightnegative. dst_negative_code_restrict_resultentryright = ff_q_pvs_restrict_resultentryrightnegative * S ((S (dc_quotient_restrict_resultentry)) * dst_negative_scale_restrict_resultentryright) + (dst_negative_restrict_resultentryright))) /\ (exists ge_balance_positive_restrict_resultentryrightvalue ge_balance_negative_restrict_resultentryrightvalue. (((((dc_right_restrict_resultentry) = 2 * (ge_balance_positive_restrict_resultentryrightvalue) /\ (ge_balance_negative_restrict_resultentryrightvalue) = 0) \/ exists ge_signed_half_restrict_resultentryrightvaluedecode. (((dc_right_restrict_resultentry) = 2 * ge_signed_half_restrict_resultentryrightvaluedecode + 1 /\ (ge_balance_positive_restrict_resultentryrightvalue) = 0) /\ (ge_balance_negative_restrict_resultentryrightvalue) = S ge_signed_half_restrict_resultentryrightvaluedecode))) /\ ((dst_positive_restrict_resultentryright) + ge_balance_negative_restrict_resultentryrightvalue = (dst_negative_restrict_resultentryright) + ge_balance_positive_restrict_resultentryrightvalue))))))))) /\ (exists sto_ap_restrict_resultentryproduct sto_an_restrict_resultentryproduct sto_bp_restrict_resultentryproduct sto_bn_restrict_resultentryproduct sto_cp_restrict_resultentryproduct sto_cn_restrict_resultentryproduct. (((((dc_left_restrict_resultentry) = 2 * (sto_ap_restrict_resultentryproduct) /\ (sto_an_restrict_resultentryproduct) = 0) \/ exists ge_signed_half_restrict_resultentryproductleft. (((dc_left_restrict_resultentry) = 2 * ge_signed_half_restrict_resultentryproductleft + 1 /\ (sto_ap_restrict_resultentryproduct) = 0) /\ (sto_an_restrict_resultentryproduct) = S ge_signed_half_restrict_resultentryproductleft))) /\ ((((((dc_right_restrict_resultentry) = 2 * (sto_bp_restrict_resultentryproduct) /\ (sto_bn_restrict_resultentryproduct) = 0) \/ exists ge_signed_half_restrict_resultentryproductright. (((dc_right_restrict_resultentry) = 2 * ge_signed_half_restrict_resultentryproductright + 1 /\ (sto_bp_restrict_resultentryproduct) = 0) /\ (sto_bn_restrict_resultentryproduct) = S ge_signed_half_restrict_resultentryproductright))) /\ ((((((dc_value_restrict_result) = 2 * (sto_cp_restrict_resultentryproduct) /\ (sto_cn_restrict_resultentryproduct) = 0) \/ exists ge_signed_half_restrict_resultentryproductoutput. (((dc_value_restrict_result) = 2 * ge_signed_half_restrict_resultentryproductoutput + 1 /\ (sto_cp_restrict_resultentryproduct) = 0) /\ (sto_cn_restrict_resultentryproduct) = S ge_signed_half_restrict_resultentryproductoutput))) /\ ((sto_ap_restrict_resultentryproduct * sto_bp_restrict_resultentryproduct + sto_an_restrict_resultentryproduct * sto_bn_restrict_resultentryproduct) + sto_cn_restrict_resultentryproduct = (sto_ap_restrict_resultentryproduct * sto_bn_restrict_resultentryproduct + sto_an_restrict_resultentryproduct * sto_bp_restrict_resultentryproduct) + sto_cp_restrict_resultentryproduct))))))))))))))) \/ ((((dc_index_restrict_result)=0 \/ ~(exists pvs_factor_restrict_resultentrynondivisor. (n) = (dc_index_restrict_result) * pvs_factor_restrict_resultentrynondivisor)) /\ ((dc_value_restrict_result)=0)))))))