dirichlet_constant_one_prefix_from_divisor_mask

Exact expanded first-order arithmetic statement

forall N F U n l M. (((exists dst_positive_code_one_prefix_onestable dst_positive_scale_one_prefix_onestable dst_negative_code_one_prefix_onestable dst_negative_scale_one_prefix_onestable. (((U) = (((((dst_positive_code_one_prefix_onestable) + (dst_positive_scale_one_prefix_onestable)) * S ((dst_positive_code_one_prefix_onestable) + (dst_positive_scale_one_prefix_onestable)) + ((dst_positive_scale_one_prefix_onestable) + (dst_positive_scale_one_prefix_onestable))) + (((dst_negative_code_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)) * S ((dst_negative_code_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)) + ((dst_negative_scale_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)))) * S ((((dst_positive_code_one_prefix_onestable) + (dst_positive_scale_one_prefix_onestable)) * S ((dst_positive_code_one_prefix_onestable) + (dst_positive_scale_one_prefix_onestable)) + ((dst_positive_scale_one_prefix_onestable) + (dst_positive_scale_one_prefix_onestable))) + (((dst_negative_code_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)) * S ((dst_negative_code_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)) + ((dst_negative_scale_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)))) + ((((dst_negative_code_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)) * S ((dst_negative_code_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)) + ((dst_negative_scale_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable))) + (((dst_negative_code_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)) * S ((dst_negative_code_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)) + ((dst_negative_scale_one_prefix_onestable) + (dst_negative_scale_one_prefix_onestable)))))) /\ (forall dst_index_one_prefix_onestable. (exists pvs_le_gap_one_prefix_onestabledomain. pvs_le_gap_one_prefix_onestabledomain + (dst_index_one_prefix_onestable) = (N)) -> exists dst_positive_one_prefix_onestable dst_negative_one_prefix_onestable dst_value_one_prefix_onestable. ((((exists ff_h_pvs_one_prefix_onestableentrypositive. ff_h_pvs_one_prefix_onestableentrypositive + S (dst_positive_one_prefix_onestable) = S ((S (dst_index_one_prefix_onestable)) * dst_positive_scale_one_prefix_onestable)) /\ exists ff_q_pvs_one_prefix_onestableentrypositive. dst_positive_code_one_prefix_onestable = ff_q_pvs_one_prefix_onestableentrypositive * S ((S (dst_index_one_prefix_onestable)) * dst_positive_scale_one_prefix_onestable) + (dst_positive_one_prefix_onestable))) /\ (((((exists ff_h_pvs_one_prefix_onestableentrynegative. ff_h_pvs_one_prefix_onestableentrynegative + S (dst_negative_one_prefix_onestable) = S ((S (dst_index_one_prefix_onestable)) * dst_negative_scale_one_prefix_onestable)) /\ exists ff_q_pvs_one_prefix_onestableentrynegative. dst_negative_code_one_prefix_onestable = ff_q_pvs_one_prefix_onestableentrynegative * S ((S (dst_index_one_prefix_onestable)) * dst_negative_scale_one_prefix_onestable) + (dst_negative_one_prefix_onestable))) /\ (exists ge_balance_positive_one_prefix_onestableentryvalue ge_balance_negative_one_prefix_onestableentryvalue. (((((dst_value_one_prefix_onestable) = 2 * (ge_balance_positive_one_prefix_onestableentryvalue) /\ (ge_balance_negative_one_prefix_onestableentryvalue) = 0) \/ exists ge_signed_half_one_prefix_onestableentryvaluedecode. (((dst_value_one_prefix_onestable) = 2 * ge_signed_half_one_prefix_onestableentryvaluedecode + 1 /\ (ge_balance_positive_one_prefix_onestableentryvalue) = 0) /\ (ge_balance_negative_one_prefix_onestableentryvalue) = S ge_signed_half_one_prefix_onestableentryvaluedecode))) /\ ((dst_positive_one_prefix_onestable) + ge_balance_negative_one_prefix_onestableentryvalue = (dst_negative_one_prefix_onestable) + ge_balance_positive_one_prefix_onestableentryvalue))))))))) /\ (forall du_index_one_prefix_ones du_value_one_prefix_ones. ~(du_index_one_prefix_ones=0) -> (exists pvs_le_gap_one_prefix_onesbound. pvs_le_gap_one_prefix_onesbound + (du_index_one_prefix_ones) = (N)) -> (exists dst_positive_code_one_prefix_onesentry dst_positive_scale_one_prefix_onesentry dst_negative_code_one_prefix_onesentry dst_negative_scale_one_prefix_onesentry dst_positive_one_prefix_onesentry dst_negative_one_prefix_onesentry. (((U) = (((((dst_positive_code_one_prefix_onesentry) + (dst_positive_scale_one_prefix_onesentry)) * S ((dst_positive_code_one_prefix_onesentry) + (dst_positive_scale_one_prefix_onesentry)) + ((dst_positive_scale_one_prefix_onesentry) + (dst_positive_scale_one_prefix_onesentry))) + (((dst_negative_code_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)) * S ((dst_negative_code_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)) + ((dst_negative_scale_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)))) * S ((((dst_positive_code_one_prefix_onesentry) + (dst_positive_scale_one_prefix_onesentry)) * S ((dst_positive_code_one_prefix_onesentry) + (dst_positive_scale_one_prefix_onesentry)) + ((dst_positive_scale_one_prefix_onesentry) + (dst_positive_scale_one_prefix_onesentry))) + (((dst_negative_code_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)) * S ((dst_negative_code_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)) + ((dst_negative_scale_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)))) + ((((dst_negative_code_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)) * S ((dst_negative_code_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)) + ((dst_negative_scale_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry))) + (((dst_negative_code_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)) * S ((dst_negative_code_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)) + ((dst_negative_scale_one_prefix_onesentry) + (dst_negative_scale_one_prefix_onesentry)))))) /\ (((((exists ff_h_pvs_one_prefix_onesentrypositive. ff_h_pvs_one_prefix_onesentrypositive + S (dst_positive_one_prefix_onesentry) = S ((S (du_index_one_prefix_ones)) * dst_positive_scale_one_prefix_onesentry)) /\ exists ff_q_pvs_one_prefix_onesentrypositive. dst_positive_code_one_prefix_onesentry = ff_q_pvs_one_prefix_onesentrypositive * S ((S (du_index_one_prefix_ones)) * dst_positive_scale_one_prefix_onesentry) + (dst_positive_one_prefix_onesentry))) /\ (((((exists ff_h_pvs_one_prefix_onesentrynegative. ff_h_pvs_one_prefix_onesentrynegative + S (dst_negative_one_prefix_onesentry) = S ((S (du_index_one_prefix_ones)) * dst_negative_scale_one_prefix_onesentry)) /\ exists ff_q_pvs_one_prefix_onesentrynegative. dst_negative_code_one_prefix_onesentry = ff_q_pvs_one_prefix_onesentrynegative * S ((S (du_index_one_prefix_ones)) * dst_negative_scale_one_prefix_onesentry) + (dst_negative_one_prefix_onesentry))) /\ (exists ge_balance_positive_one_prefix_onesentryvalue ge_balance_negative_one_prefix_onesentryvalue. (((((du_value_one_prefix_ones) = 2 * (ge_balance_positive_one_prefix_onesentryvalue) /\ (ge_balance_negative_one_prefix_onesentryvalue) = 0) \/ exists ge_signed_half_one_prefix_onesentryvaluedecode. (((du_value_one_prefix_ones) = 2 * ge_signed_half_one_prefix_onesentryvaluedecode + 1 /\ (ge_balance_positive_one_prefix_onesentryvalue) = 0) /\ (ge_balance_negative_one_prefix_onesentryvalue) = S ge_signed_half_one_prefix_onesentryvaluedecode))) /\ ((dst_positive_one_prefix_onesentry) + ge_balance_negative_one_prefix_onesentryvalue = (dst_negative_one_prefix_onesentry) + ge_balance_positive_one_prefix_onesentryvalue))))))))) -> du_value_one_prefix_ones=2))) -> ~(n=0) -> (exists pvs_le_gap_one_prefix_bound. pvs_le_gap_one_prefix_bound + (n) = (N)) -> (((exists dst_positive_code_one_prefix_sourcetable dst_positive_scale_one_prefix_sourcetable dst_negative_code_one_prefix_sourcetable dst_negative_scale_one_prefix_sourcetable. (((M) = (((((dst_positive_code_one_prefix_sourcetable) + (dst_positive_scale_one_prefix_sourcetable)) * S ((dst_positive_code_one_prefix_sourcetable) + (dst_positive_scale_one_prefix_sourcetable)) + ((dst_positive_scale_one_prefix_sourcetable) + (dst_positive_scale_one_prefix_sourcetable))) + (((dst_negative_code_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)) * S ((dst_negative_code_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)) + ((dst_negative_scale_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)))) * S ((((dst_positive_code_one_prefix_sourcetable) + (dst_positive_scale_one_prefix_sourcetable)) * S ((dst_positive_code_one_prefix_sourcetable) + (dst_positive_scale_one_prefix_sourcetable)) + ((dst_positive_scale_one_prefix_sourcetable) + (dst_positive_scale_one_prefix_sourcetable))) + (((dst_negative_code_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)) * S ((dst_negative_code_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)) + ((dst_negative_scale_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)))) + ((((dst_negative_code_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)) * S ((dst_negative_code_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)) + ((dst_negative_scale_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable))) + (((dst_negative_code_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)) * S ((dst_negative_code_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)) + ((dst_negative_scale_one_prefix_sourcetable) + (dst_negative_scale_one_prefix_sourcetable)))))) /\ (forall dst_index_one_prefix_sourcetable. (exists pvs_le_gap_one_prefix_sourcetabledomain. pvs_le_gap_one_prefix_sourcetabledomain + (dst_index_one_prefix_sourcetable) = (l)) -> exists dst_positive_one_prefix_sourcetable dst_negative_one_prefix_sourcetable dst_value_one_prefix_sourcetable. ((((exists ff_h_pvs_one_prefix_sourcetableentrypositive. ff_h_pvs_one_prefix_sourcetableentrypositive + S (dst_positive_one_prefix_sourcetable) = S ((S (dst_index_one_prefix_sourcetable)) * dst_positive_scale_one_prefix_sourcetable)) /\ exists ff_q_pvs_one_prefix_sourcetableentrypositive. dst_positive_code_one_prefix_sourcetable = ff_q_pvs_one_prefix_sourcetableentrypositive * S ((S (dst_index_one_prefix_sourcetable)) * dst_positive_scale_one_prefix_sourcetable) + (dst_positive_one_prefix_sourcetable))) /\ (((((exists ff_h_pvs_one_prefix_sourcetableentrynegative. ff_h_pvs_one_prefix_sourcetableentrynegative + S (dst_negative_one_prefix_sourcetable) = S ((S (dst_index_one_prefix_sourcetable)) * dst_negative_scale_one_prefix_sourcetable)) /\ exists ff_q_pvs_one_prefix_sourcetableentrynegative. dst_negative_code_one_prefix_sourcetable = ff_q_pvs_one_prefix_sourcetableentrynegative * S ((S (dst_index_one_prefix_sourcetable)) * dst_negative_scale_one_prefix_sourcetable) + (dst_negative_one_prefix_sourcetable))) /\ (exists ge_balance_positive_one_prefix_sourcetableentryvalue ge_balance_negative_one_prefix_sourcetableentryvalue. (((((dst_value_one_prefix_sourcetable) = 2 * (ge_balance_positive_one_prefix_sourcetableentryvalue) /\ (ge_balance_negative_one_prefix_sourcetableentryvalue) = 0) \/ exists ge_signed_half_one_prefix_sourcetableentryvaluedecode. (((dst_value_one_prefix_sourcetable) = 2 * ge_signed_half_one_prefix_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_one_prefix_sourcetableentryvalue) = 0) /\ (ge_balance_negative_one_prefix_sourcetableentryvalue) = S ge_signed_half_one_prefix_sourcetableentryvaluedecode))) /\ ((dst_positive_one_prefix_sourcetable) + ge_balance_negative_one_prefix_sourcetableentryvalue = (dst_negative_one_prefix_sourcetable) + ge_balance_positive_one_prefix_sourcetableentryvalue))))))))) /\ (forall dm_index_one_prefix_source dm_value_one_prefix_source. (exists pvs_le_gap_one_prefix_sourcedomain. pvs_le_gap_one_prefix_sourcedomain + (dm_index_one_prefix_source) = (l)) -> (exists dst_positive_code_one_prefix_sourcelookup dst_positive_scale_one_prefix_sourcelookup dst_negative_code_one_prefix_sourcelookup dst_negative_scale_one_prefix_sourcelookup dst_positive_one_prefix_sourcelookup dst_negative_one_prefix_sourcelookup. (((M) = (((((dst_positive_code_one_prefix_sourcelookup) + (dst_positive_scale_one_prefix_sourcelookup)) * S ((dst_positive_code_one_prefix_sourcelookup) + (dst_positive_scale_one_prefix_sourcelookup)) + ((dst_positive_scale_one_prefix_sourcelookup) + (dst_positive_scale_one_prefix_sourcelookup))) + (((dst_negative_code_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)) * S ((dst_negative_code_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)) + ((dst_negative_scale_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)))) * S ((((dst_positive_code_one_prefix_sourcelookup) + (dst_positive_scale_one_prefix_sourcelookup)) * S ((dst_positive_code_one_prefix_sourcelookup) + (dst_positive_scale_one_prefix_sourcelookup)) + ((dst_positive_scale_one_prefix_sourcelookup) + (dst_positive_scale_one_prefix_sourcelookup))) + (((dst_negative_code_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)) * S ((dst_negative_code_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)) + ((dst_negative_scale_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)))) + ((((dst_negative_code_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)) * S ((dst_negative_code_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)) + ((dst_negative_scale_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup))) + (((dst_negative_code_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)) * S ((dst_negative_code_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)) + ((dst_negative_scale_one_prefix_sourcelookup) + (dst_negative_scale_one_prefix_sourcelookup)))))) /\ (((((exists ff_h_pvs_one_prefix_sourcelookuppositive. ff_h_pvs_one_prefix_sourcelookuppositive + S (dst_positive_one_prefix_sourcelookup) = S ((S (dm_index_one_prefix_source)) * dst_positive_scale_one_prefix_sourcelookup)) /\ exists ff_q_pvs_one_prefix_sourcelookuppositive. dst_positive_code_one_prefix_sourcelookup = ff_q_pvs_one_prefix_sourcelookuppositive * S ((S (dm_index_one_prefix_source)) * dst_positive_scale_one_prefix_sourcelookup) + (dst_positive_one_prefix_sourcelookup))) /\ (((((exists ff_h_pvs_one_prefix_sourcelookupnegative. ff_h_pvs_one_prefix_sourcelookupnegative + S (dst_negative_one_prefix_sourcelookup) = S ((S (dm_index_one_prefix_source)) * dst_negative_scale_one_prefix_sourcelookup)) /\ exists ff_q_pvs_one_prefix_sourcelookupnegative. dst_negative_code_one_prefix_sourcelookup = ff_q_pvs_one_prefix_sourcelookupnegative * S ((S (dm_index_one_prefix_source)) * dst_negative_scale_one_prefix_sourcelookup) + (dst_negative_one_prefix_sourcelookup))) /\ (exists ge_balance_positive_one_prefix_sourcelookupvalue ge_balance_negative_one_prefix_sourcelookupvalue. (((((dm_value_one_prefix_source) = 2 * (ge_balance_positive_one_prefix_sourcelookupvalue) /\ (ge_balance_negative_one_prefix_sourcelookupvalue) = 0) \/ exists ge_signed_half_one_prefix_sourcelookupvaluedecode. (((dm_value_one_prefix_source) = 2 * ge_signed_half_one_prefix_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_one_prefix_sourcelookupvalue) = 0) /\ (ge_balance_negative_one_prefix_sourcelookupvalue) = S ge_signed_half_one_prefix_sourcelookupvaluedecode))) /\ ((dst_positive_one_prefix_sourcelookup) + ge_balance_negative_one_prefix_sourcelookupvalue = (dst_negative_one_prefix_sourcelookup) + ge_balance_positive_one_prefix_sourcelookupvalue))))))))) -> ((((~((dm_index_one_prefix_source)=0)) /\ (exists dm_quotient_one_prefix_sourceentry. (((n)=(dm_index_one_prefix_source)*dm_quotient_one_prefix_sourceentry) /\ (exists dst_positive_code_one_prefix_sourceentryinput dst_positive_scale_one_prefix_sourceentryinput dst_negative_code_one_prefix_sourceentryinput dst_negative_scale_one_prefix_sourceentryinput dst_positive_one_prefix_sourceentryinput dst_negative_one_prefix_sourceentryinput. (((F) = (((((dst_positive_code_one_prefix_sourceentryinput) + (dst_positive_scale_one_prefix_sourceentryinput)) * S ((dst_positive_code_one_prefix_sourceentryinput) + (dst_positive_scale_one_prefix_sourceentryinput)) + ((dst_positive_scale_one_prefix_sourceentryinput) + (dst_positive_scale_one_prefix_sourceentryinput))) + (((dst_negative_code_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)) * S ((dst_negative_code_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)) + ((dst_negative_scale_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)))) * S ((((dst_positive_code_one_prefix_sourceentryinput) + (dst_positive_scale_one_prefix_sourceentryinput)) * S ((dst_positive_code_one_prefix_sourceentryinput) + (dst_positive_scale_one_prefix_sourceentryinput)) + ((dst_positive_scale_one_prefix_sourceentryinput) + (dst_positive_scale_one_prefix_sourceentryinput))) + (((dst_negative_code_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)) * S ((dst_negative_code_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)) + ((dst_negative_scale_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)))) + ((((dst_negative_code_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)) * S ((dst_negative_code_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)) + ((dst_negative_scale_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput))) + (((dst_negative_code_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)) * S ((dst_negative_code_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)) + ((dst_negative_scale_one_prefix_sourceentryinput) + (dst_negative_scale_one_prefix_sourceentryinput)))))) /\ (((((exists ff_h_pvs_one_prefix_sourceentryinputpositive. ff_h_pvs_one_prefix_sourceentryinputpositive + S (dst_positive_one_prefix_sourceentryinput) = S ((S (dm_index_one_prefix_source)) * dst_positive_scale_one_prefix_sourceentryinput)) /\ exists ff_q_pvs_one_prefix_sourceentryinputpositive. dst_positive_code_one_prefix_sourceentryinput = ff_q_pvs_one_prefix_sourceentryinputpositive * S ((S (dm_index_one_prefix_source)) * dst_positive_scale_one_prefix_sourceentryinput) + (dst_positive_one_prefix_sourceentryinput))) /\ (((((exists ff_h_pvs_one_prefix_sourceentryinputnegative. ff_h_pvs_one_prefix_sourceentryinputnegative + S (dst_negative_one_prefix_sourceentryinput) = S ((S (dm_index_one_prefix_source)) * dst_negative_scale_one_prefix_sourceentryinput)) /\ exists ff_q_pvs_one_prefix_sourceentryinputnegative. dst_negative_code_one_prefix_sourceentryinput = ff_q_pvs_one_prefix_sourceentryinputnegative * S ((S (dm_index_one_prefix_source)) * dst_negative_scale_one_prefix_sourceentryinput) + (dst_negative_one_prefix_sourceentryinput))) /\ (exists ge_balance_positive_one_prefix_sourceentryinputvalue ge_balance_negative_one_prefix_sourceentryinputvalue. (((((dm_value_one_prefix_source) = 2 * (ge_balance_positive_one_prefix_sourceentryinputvalue) /\ (ge_balance_negative_one_prefix_sourceentryinputvalue) = 0) \/ exists ge_signed_half_one_prefix_sourceentryinputvaluedecode. (((dm_value_one_prefix_source) = 2 * ge_signed_half_one_prefix_sourceentryinputvaluedecode + 1 /\ (ge_balance_positive_one_prefix_sourceentryinputvalue) = 0) /\ (ge_balance_negative_one_prefix_sourceentryinputvalue) = S ge_signed_half_one_prefix_sourceentryinputvaluedecode))) /\ ((dst_positive_one_prefix_sourceentryinput) + ge_balance_negative_one_prefix_sourceentryinputvalue = (dst_negative_one_prefix_sourceentryinput) + ge_balance_positive_one_prefix_sourceentryinputvalue))))))))))))) \/ ((((dm_index_one_prefix_source)=0 \/ ~(exists pvs_factor_one_prefix_sourceentrynondivisor. (n) = (dm_index_one_prefix_source) * pvs_factor_one_prefix_sourceentrynondivisor)) /\ ((dm_value_one_prefix_source)=0))))))) -> (((exists dst_positive_code_one_prefix_resulttable dst_positive_scale_one_prefix_resulttable dst_negative_code_one_prefix_resulttable dst_negative_scale_one_prefix_resulttable. (((M) = (((((dst_positive_code_one_prefix_resulttable) + (dst_positive_scale_one_prefix_resulttable)) * S ((dst_positive_code_one_prefix_resulttable) + (dst_positive_scale_one_prefix_resulttable)) + ((dst_positive_scale_one_prefix_resulttable) + (dst_positive_scale_one_prefix_resulttable))) + (((dst_negative_code_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)) * S ((dst_negative_code_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)) + ((dst_negative_scale_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)))) * S ((((dst_positive_code_one_prefix_resulttable) + (dst_positive_scale_one_prefix_resulttable)) * S ((dst_positive_code_one_prefix_resulttable) + (dst_positive_scale_one_prefix_resulttable)) + ((dst_positive_scale_one_prefix_resulttable) + (dst_positive_scale_one_prefix_resulttable))) + (((dst_negative_code_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)) * S ((dst_negative_code_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)) + ((dst_negative_scale_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)))) + ((((dst_negative_code_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)) * S ((dst_negative_code_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)) + ((dst_negative_scale_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable))) + (((dst_negative_code_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)) * S ((dst_negative_code_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)) + ((dst_negative_scale_one_prefix_resulttable) + (dst_negative_scale_one_prefix_resulttable)))))) /\ (forall dst_index_one_prefix_resulttable. (exists pvs_le_gap_one_prefix_resulttabledomain. pvs_le_gap_one_prefix_resulttabledomain + (dst_index_one_prefix_resulttable) = (l)) -> exists dst_positive_one_prefix_resulttable dst_negative_one_prefix_resulttable dst_value_one_prefix_resulttable. ((((exists ff_h_pvs_one_prefix_resulttableentrypositive. ff_h_pvs_one_prefix_resulttableentrypositive + S (dst_positive_one_prefix_resulttable) = S ((S (dst_index_one_prefix_resulttable)) * dst_positive_scale_one_prefix_resulttable)) /\ exists ff_q_pvs_one_prefix_resulttableentrypositive. dst_positive_code_one_prefix_resulttable = ff_q_pvs_one_prefix_resulttableentrypositive * S ((S (dst_index_one_prefix_resulttable)) * dst_positive_scale_one_prefix_resulttable) + (dst_positive_one_prefix_resulttable))) /\ (((((exists ff_h_pvs_one_prefix_resulttableentrynegative. ff_h_pvs_one_prefix_resulttableentrynegative + S (dst_negative_one_prefix_resulttable) = S ((S (dst_index_one_prefix_resulttable)) * dst_negative_scale_one_prefix_resulttable)) /\ exists ff_q_pvs_one_prefix_resulttableentrynegative. dst_negative_code_one_prefix_resulttable = ff_q_pvs_one_prefix_resulttableentrynegative * S ((S (dst_index_one_prefix_resulttable)) * dst_negative_scale_one_prefix_resulttable) + (dst_negative_one_prefix_resulttable))) /\ (exists ge_balance_positive_one_prefix_resulttableentryvalue ge_balance_negative_one_prefix_resulttableentryvalue. (((((dst_value_one_prefix_resulttable) = 2 * (ge_balance_positive_one_prefix_resulttableentryvalue) /\ (ge_balance_negative_one_prefix_resulttableentryvalue) = 0) \/ exists ge_signed_half_one_prefix_resulttableentryvaluedecode. (((dst_value_one_prefix_resulttable) = 2 * ge_signed_half_one_prefix_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_one_prefix_resulttableentryvalue) = 0) /\ (ge_balance_negative_one_prefix_resulttableentryvalue) = S ge_signed_half_one_prefix_resulttableentryvaluedecode))) /\ ((dst_positive_one_prefix_resulttable) + ge_balance_negative_one_prefix_resulttableentryvalue = (dst_negative_one_prefix_resulttable) + ge_balance_positive_one_prefix_resulttableentryvalue))))))))) /\ (forall dc_index_one_prefix_result dc_value_one_prefix_result. (exists pvs_le_gap_one_prefix_resultdomain. pvs_le_gap_one_prefix_resultdomain + (dc_index_one_prefix_result) = (l)) -> (exists dst_positive_code_one_prefix_resultlookup dst_positive_scale_one_prefix_resultlookup dst_negative_code_one_prefix_resultlookup dst_negative_scale_one_prefix_resultlookup dst_positive_one_prefix_resultlookup dst_negative_one_prefix_resultlookup. (((M) = (((((dst_positive_code_one_prefix_resultlookup) + (dst_positive_scale_one_prefix_resultlookup)) * S ((dst_positive_code_one_prefix_resultlookup) + (dst_positive_scale_one_prefix_resultlookup)) + ((dst_positive_scale_one_prefix_resultlookup) + (dst_positive_scale_one_prefix_resultlookup))) + (((dst_negative_code_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)) * S ((dst_negative_code_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)) + ((dst_negative_scale_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)))) * S ((((dst_positive_code_one_prefix_resultlookup) + (dst_positive_scale_one_prefix_resultlookup)) * S ((dst_positive_code_one_prefix_resultlookup) + (dst_positive_scale_one_prefix_resultlookup)) + ((dst_positive_scale_one_prefix_resultlookup) + (dst_positive_scale_one_prefix_resultlookup))) + (((dst_negative_code_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)) * S ((dst_negative_code_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)) + ((dst_negative_scale_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)))) + ((((dst_negative_code_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)) * S ((dst_negative_code_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)) + ((dst_negative_scale_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup))) + (((dst_negative_code_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)) * S ((dst_negative_code_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)) + ((dst_negative_scale_one_prefix_resultlookup) + (dst_negative_scale_one_prefix_resultlookup)))))) /\ (((((exists ff_h_pvs_one_prefix_resultlookuppositive. ff_h_pvs_one_prefix_resultlookuppositive + S (dst_positive_one_prefix_resultlookup) = S ((S (dc_index_one_prefix_result)) * dst_positive_scale_one_prefix_resultlookup)) /\ exists ff_q_pvs_one_prefix_resultlookuppositive. dst_positive_code_one_prefix_resultlookup = ff_q_pvs_one_prefix_resultlookuppositive * S ((S (dc_index_one_prefix_result)) * dst_positive_scale_one_prefix_resultlookup) + (dst_positive_one_prefix_resultlookup))) /\ (((((exists ff_h_pvs_one_prefix_resultlookupnegative. ff_h_pvs_one_prefix_resultlookupnegative + S (dst_negative_one_prefix_resultlookup) = S ((S (dc_index_one_prefix_result)) * dst_negative_scale_one_prefix_resultlookup)) /\ exists ff_q_pvs_one_prefix_resultlookupnegative. dst_negative_code_one_prefix_resultlookup = ff_q_pvs_one_prefix_resultlookupnegative * S ((S (dc_index_one_prefix_result)) * dst_negative_scale_one_prefix_resultlookup) + (dst_negative_one_prefix_resultlookup))) /\ (exists ge_balance_positive_one_prefix_resultlookupvalue ge_balance_negative_one_prefix_resultlookupvalue. (((((dc_value_one_prefix_result) = 2 * (ge_balance_positive_one_prefix_resultlookupvalue) /\ (ge_balance_negative_one_prefix_resultlookupvalue) = 0) \/ exists ge_signed_half_one_prefix_resultlookupvaluedecode. (((dc_value_one_prefix_result) = 2 * ge_signed_half_one_prefix_resultlookupvaluedecode + 1 /\ (ge_balance_positive_one_prefix_resultlookupvalue) = 0) /\ (ge_balance_negative_one_prefix_resultlookupvalue) = S ge_signed_half_one_prefix_resultlookupvaluedecode))) /\ ((dst_positive_one_prefix_resultlookup) + ge_balance_negative_one_prefix_resultlookupvalue = (dst_negative_one_prefix_resultlookup) + ge_balance_positive_one_prefix_resultlookupvalue))))))))) -> ((((~((dc_index_one_prefix_result)=0)) /\ (exists dc_quotient_one_prefix_resultentry dc_left_one_prefix_resultentry dc_right_one_prefix_resultentry. (((n)=(dc_index_one_prefix_result)*dc_quotient_one_prefix_resultentry) /\ (((exists dst_positive_code_one_prefix_resultentryleft dst_positive_scale_one_prefix_resultentryleft dst_negative_code_one_prefix_resultentryleft dst_negative_scale_one_prefix_resultentryleft dst_positive_one_prefix_resultentryleft dst_negative_one_prefix_resultentryleft. (((F) = (((((dst_positive_code_one_prefix_resultentryleft) + (dst_positive_scale_one_prefix_resultentryleft)) * S ((dst_positive_code_one_prefix_resultentryleft) + (dst_positive_scale_one_prefix_resultentryleft)) + ((dst_positive_scale_one_prefix_resultentryleft) + (dst_positive_scale_one_prefix_resultentryleft))) + (((dst_negative_code_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)) * S ((dst_negative_code_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)) + ((dst_negative_scale_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)))) * S ((((dst_positive_code_one_prefix_resultentryleft) + (dst_positive_scale_one_prefix_resultentryleft)) * S ((dst_positive_code_one_prefix_resultentryleft) + (dst_positive_scale_one_prefix_resultentryleft)) + ((dst_positive_scale_one_prefix_resultentryleft) + (dst_positive_scale_one_prefix_resultentryleft))) + (((dst_negative_code_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)) * S ((dst_negative_code_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)) + ((dst_negative_scale_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)))) + ((((dst_negative_code_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)) * S ((dst_negative_code_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)) + ((dst_negative_scale_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft))) + (((dst_negative_code_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)) * S ((dst_negative_code_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)) + ((dst_negative_scale_one_prefix_resultentryleft) + (dst_negative_scale_one_prefix_resultentryleft)))))) /\ (((((exists ff_h_pvs_one_prefix_resultentryleftpositive. ff_h_pvs_one_prefix_resultentryleftpositive + S (dst_positive_one_prefix_resultentryleft) = S ((S (dc_index_one_prefix_result)) * dst_positive_scale_one_prefix_resultentryleft)) /\ exists ff_q_pvs_one_prefix_resultentryleftpositive. dst_positive_code_one_prefix_resultentryleft = ff_q_pvs_one_prefix_resultentryleftpositive * S ((S (dc_index_one_prefix_result)) * dst_positive_scale_one_prefix_resultentryleft) + (dst_positive_one_prefix_resultentryleft))) /\ (((((exists ff_h_pvs_one_prefix_resultentryleftnegative. ff_h_pvs_one_prefix_resultentryleftnegative + S (dst_negative_one_prefix_resultentryleft) = S ((S (dc_index_one_prefix_result)) * dst_negative_scale_one_prefix_resultentryleft)) /\ exists ff_q_pvs_one_prefix_resultentryleftnegative. dst_negative_code_one_prefix_resultentryleft = ff_q_pvs_one_prefix_resultentryleftnegative * S ((S (dc_index_one_prefix_result)) * dst_negative_scale_one_prefix_resultentryleft) + (dst_negative_one_prefix_resultentryleft))) /\ (exists ge_balance_positive_one_prefix_resultentryleftvalue ge_balance_negative_one_prefix_resultentryleftvalue. (((((dc_left_one_prefix_resultentry) = 2 * (ge_balance_positive_one_prefix_resultentryleftvalue) /\ (ge_balance_negative_one_prefix_resultentryleftvalue) = 0) \/ exists ge_signed_half_one_prefix_resultentryleftvaluedecode. (((dc_left_one_prefix_resultentry) = 2 * ge_signed_half_one_prefix_resultentryleftvaluedecode + 1 /\ (ge_balance_positive_one_prefix_resultentryleftvalue) = 0) /\ (ge_balance_negative_one_prefix_resultentryleftvalue) = S ge_signed_half_one_prefix_resultentryleftvaluedecode))) /\ ((dst_positive_one_prefix_resultentryleft) + ge_balance_negative_one_prefix_resultentryleftvalue = (dst_negative_one_prefix_resultentryleft) + ge_balance_positive_one_prefix_resultentryleftvalue))))))))) /\ (((exists dst_positive_code_one_prefix_resultentryright dst_positive_scale_one_prefix_resultentryright dst_negative_code_one_prefix_resultentryright dst_negative_scale_one_prefix_resultentryright dst_positive_one_prefix_resultentryright dst_negative_one_prefix_resultentryright. (((U) = (((((dst_positive_code_one_prefix_resultentryright) + (dst_positive_scale_one_prefix_resultentryright)) * S ((dst_positive_code_one_prefix_resultentryright) + (dst_positive_scale_one_prefix_resultentryright)) + ((dst_positive_scale_one_prefix_resultentryright) + (dst_positive_scale_one_prefix_resultentryright))) + (((dst_negative_code_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)) * S ((dst_negative_code_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)) + ((dst_negative_scale_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)))) * S ((((dst_positive_code_one_prefix_resultentryright) + (dst_positive_scale_one_prefix_resultentryright)) * S ((dst_positive_code_one_prefix_resultentryright) + (dst_positive_scale_one_prefix_resultentryright)) + ((dst_positive_scale_one_prefix_resultentryright) + (dst_positive_scale_one_prefix_resultentryright))) + (((dst_negative_code_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)) * S ((dst_negative_code_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)) + ((dst_negative_scale_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)))) + ((((dst_negative_code_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)) * S ((dst_negative_code_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)) + ((dst_negative_scale_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright))) + (((dst_negative_code_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)) * S ((dst_negative_code_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)) + ((dst_negative_scale_one_prefix_resultentryright) + (dst_negative_scale_one_prefix_resultentryright)))))) /\ (((((exists ff_h_pvs_one_prefix_resultentryrightpositive. ff_h_pvs_one_prefix_resultentryrightpositive + S (dst_positive_one_prefix_resultentryright) = S ((S (dc_quotient_one_prefix_resultentry)) * dst_positive_scale_one_prefix_resultentryright)) /\ exists ff_q_pvs_one_prefix_resultentryrightpositive. dst_positive_code_one_prefix_resultentryright = ff_q_pvs_one_prefix_resultentryrightpositive * S ((S (dc_quotient_one_prefix_resultentry)) * dst_positive_scale_one_prefix_resultentryright) + (dst_positive_one_prefix_resultentryright))) /\ (((((exists ff_h_pvs_one_prefix_resultentryrightnegative. ff_h_pvs_one_prefix_resultentryrightnegative + S (dst_negative_one_prefix_resultentryright) = S ((S (dc_quotient_one_prefix_resultentry)) * dst_negative_scale_one_prefix_resultentryright)) /\ exists ff_q_pvs_one_prefix_resultentryrightnegative. dst_negative_code_one_prefix_resultentryright = ff_q_pvs_one_prefix_resultentryrightnegative * S ((S (dc_quotient_one_prefix_resultentry)) * dst_negative_scale_one_prefix_resultentryright) + (dst_negative_one_prefix_resultentryright))) /\ (exists ge_balance_positive_one_prefix_resultentryrightvalue ge_balance_negative_one_prefix_resultentryrightvalue. (((((dc_right_one_prefix_resultentry) = 2 * (ge_balance_positive_one_prefix_resultentryrightvalue) /\ (ge_balance_negative_one_prefix_resultentryrightvalue) = 0) \/ exists ge_signed_half_one_prefix_resultentryrightvaluedecode. (((dc_right_one_prefix_resultentry) = 2 * ge_signed_half_one_prefix_resultentryrightvaluedecode + 1 /\ (ge_balance_positive_one_prefix_resultentryrightvalue) = 0) /\ (ge_balance_negative_one_prefix_resultentryrightvalue) = S ge_signed_half_one_prefix_resultentryrightvaluedecode))) /\ ((dst_positive_one_prefix_resultentryright) + ge_balance_negative_one_prefix_resultentryrightvalue = (dst_negative_one_prefix_resultentryright) + ge_balance_positive_one_prefix_resultentryrightvalue))))))))) /\ (exists sto_ap_one_prefix_resultentryproduct sto_an_one_prefix_resultentryproduct sto_bp_one_prefix_resultentryproduct sto_bn_one_prefix_resultentryproduct sto_cp_one_prefix_resultentryproduct sto_cn_one_prefix_resultentryproduct. (((((dc_left_one_prefix_resultentry) = 2 * (sto_ap_one_prefix_resultentryproduct) /\ (sto_an_one_prefix_resultentryproduct) = 0) \/ exists ge_signed_half_one_prefix_resultentryproductleft. (((dc_left_one_prefix_resultentry) = 2 * ge_signed_half_one_prefix_resultentryproductleft + 1 /\ (sto_ap_one_prefix_resultentryproduct) = 0) /\ (sto_an_one_prefix_resultentryproduct) = S ge_signed_half_one_prefix_resultentryproductleft))) /\ ((((((dc_right_one_prefix_resultentry) = 2 * (sto_bp_one_prefix_resultentryproduct) /\ (sto_bn_one_prefix_resultentryproduct) = 0) \/ exists ge_signed_half_one_prefix_resultentryproductright. (((dc_right_one_prefix_resultentry) = 2 * ge_signed_half_one_prefix_resultentryproductright + 1 /\ (sto_bp_one_prefix_resultentryproduct) = 0) /\ (sto_bn_one_prefix_resultentryproduct) = S ge_signed_half_one_prefix_resultentryproductright))) /\ ((((((dc_value_one_prefix_result) = 2 * (sto_cp_one_prefix_resultentryproduct) /\ (sto_cn_one_prefix_resultentryproduct) = 0) \/ exists ge_signed_half_one_prefix_resultentryproductoutput. (((dc_value_one_prefix_result) = 2 * ge_signed_half_one_prefix_resultentryproductoutput + 1 /\ (sto_cp_one_prefix_resultentryproduct) = 0) /\ (sto_cn_one_prefix_resultentryproduct) = S ge_signed_half_one_prefix_resultentryproductoutput))) /\ ((sto_ap_one_prefix_resultentryproduct * sto_bp_one_prefix_resultentryproduct + sto_an_one_prefix_resultentryproduct * sto_bn_one_prefix_resultentryproduct) + sto_cn_one_prefix_resultentryproduct = (sto_ap_one_prefix_resultentryproduct * sto_bn_one_prefix_resultentryproduct + sto_an_one_prefix_resultentryproduct * sto_bp_one_prefix_resultentryproduct) + sto_cp_one_prefix_resultentryproduct))))))))))))))) \/ ((((dc_index_one_prefix_result)=0 \/ ~(exists pvs_factor_one_prefix_resultentrynondivisor. (n) = (dc_index_one_prefix_result) * pvs_factor_one_prefix_resultentrynondivisor)) /\ ((dc_value_one_prefix_result)=0)))))))