dirichlet_constant_one_prefix_to_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 dc_index_one_prefix_source dc_value_one_prefix_source. (exists pvs_le_gap_one_prefix_sourcedomain. pvs_le_gap_one_prefix_sourcedomain + (dc_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 (dc_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 (dc_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 (dc_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 (dc_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. (((((dc_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. (((dc_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))))))))) -> ((((~((dc_index_one_prefix_source)=0)) /\ (exists dc_quotient_one_prefix_sourceentry dc_left_one_prefix_sourceentry dc_right_one_prefix_sourceentry. (((n)=(dc_index_one_prefix_source)*dc_quotient_one_prefix_sourceentry) /\ (((exists dst_positive_code_one_prefix_sourceentryleft dst_positive_scale_one_prefix_sourceentryleft dst_negative_code_one_prefix_sourceentryleft dst_negative_scale_one_prefix_sourceentryleft dst_positive_one_prefix_sourceentryleft dst_negative_one_prefix_sourceentryleft. (((F) = (((((dst_positive_code_one_prefix_sourceentryleft) + (dst_positive_scale_one_prefix_sourceentryleft)) * S ((dst_positive_code_one_prefix_sourceentryleft) + (dst_positive_scale_one_prefix_sourceentryleft)) + ((dst_positive_scale_one_prefix_sourceentryleft) + (dst_positive_scale_one_prefix_sourceentryleft))) + (((dst_negative_code_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)) * S ((dst_negative_code_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)) + ((dst_negative_scale_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)))) * S ((((dst_positive_code_one_prefix_sourceentryleft) + (dst_positive_scale_one_prefix_sourceentryleft)) * S ((dst_positive_code_one_prefix_sourceentryleft) + (dst_positive_scale_one_prefix_sourceentryleft)) + ((dst_positive_scale_one_prefix_sourceentryleft) + (dst_positive_scale_one_prefix_sourceentryleft))) + (((dst_negative_code_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)) * S ((dst_negative_code_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)) + ((dst_negative_scale_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)))) + ((((dst_negative_code_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)) * S ((dst_negative_code_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)) + ((dst_negative_scale_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft))) + (((dst_negative_code_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)) * S ((dst_negative_code_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)) + ((dst_negative_scale_one_prefix_sourceentryleft) + (dst_negative_scale_one_prefix_sourceentryleft)))))) /\ (((((exists ff_h_pvs_one_prefix_sourceentryleftpositive. ff_h_pvs_one_prefix_sourceentryleftpositive + S (dst_positive_one_prefix_sourceentryleft) = S ((S (dc_index_one_prefix_source)) * dst_positive_scale_one_prefix_sourceentryleft)) /\ exists ff_q_pvs_one_prefix_sourceentryleftpositive. dst_positive_code_one_prefix_sourceentryleft = ff_q_pvs_one_prefix_sourceentryleftpositive * S ((S (dc_index_one_prefix_source)) * dst_positive_scale_one_prefix_sourceentryleft) + (dst_positive_one_prefix_sourceentryleft))) /\ (((((exists ff_h_pvs_one_prefix_sourceentryleftnegative. ff_h_pvs_one_prefix_sourceentryleftnegative + S (dst_negative_one_prefix_sourceentryleft) = S ((S (dc_index_one_prefix_source)) * dst_negative_scale_one_prefix_sourceentryleft)) /\ exists ff_q_pvs_one_prefix_sourceentryleftnegative. dst_negative_code_one_prefix_sourceentryleft = ff_q_pvs_one_prefix_sourceentryleftnegative * S ((S (dc_index_one_prefix_source)) * dst_negative_scale_one_prefix_sourceentryleft) + (dst_negative_one_prefix_sourceentryleft))) /\ (exists ge_balance_positive_one_prefix_sourceentryleftvalue ge_balance_negative_one_prefix_sourceentryleftvalue. (((((dc_left_one_prefix_sourceentry) = 2 * (ge_balance_positive_one_prefix_sourceentryleftvalue) /\ (ge_balance_negative_one_prefix_sourceentryleftvalue) = 0) \/ exists ge_signed_half_one_prefix_sourceentryleftvaluedecode. (((dc_left_one_prefix_sourceentry) = 2 * ge_signed_half_one_prefix_sourceentryleftvaluedecode + 1 /\ (ge_balance_positive_one_prefix_sourceentryleftvalue) = 0) /\ (ge_balance_negative_one_prefix_sourceentryleftvalue) = S ge_signed_half_one_prefix_sourceentryleftvaluedecode))) /\ ((dst_positive_one_prefix_sourceentryleft) + ge_balance_negative_one_prefix_sourceentryleftvalue = (dst_negative_one_prefix_sourceentryleft) + ge_balance_positive_one_prefix_sourceentryleftvalue))))))))) /\ (((exists dst_positive_code_one_prefix_sourceentryright dst_positive_scale_one_prefix_sourceentryright dst_negative_code_one_prefix_sourceentryright dst_negative_scale_one_prefix_sourceentryright dst_positive_one_prefix_sourceentryright dst_negative_one_prefix_sourceentryright. (((U) = (((((dst_positive_code_one_prefix_sourceentryright) + (dst_positive_scale_one_prefix_sourceentryright)) * S ((dst_positive_code_one_prefix_sourceentryright) + (dst_positive_scale_one_prefix_sourceentryright)) + ((dst_positive_scale_one_prefix_sourceentryright) + (dst_positive_scale_one_prefix_sourceentryright))) + (((dst_negative_code_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)) * S ((dst_negative_code_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)) + ((dst_negative_scale_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)))) * S ((((dst_positive_code_one_prefix_sourceentryright) + (dst_positive_scale_one_prefix_sourceentryright)) * S ((dst_positive_code_one_prefix_sourceentryright) + (dst_positive_scale_one_prefix_sourceentryright)) + ((dst_positive_scale_one_prefix_sourceentryright) + (dst_positive_scale_one_prefix_sourceentryright))) + (((dst_negative_code_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)) * S ((dst_negative_code_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)) + ((dst_negative_scale_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)))) + ((((dst_negative_code_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)) * S ((dst_negative_code_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)) + ((dst_negative_scale_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright))) + (((dst_negative_code_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)) * S ((dst_negative_code_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)) + ((dst_negative_scale_one_prefix_sourceentryright) + (dst_negative_scale_one_prefix_sourceentryright)))))) /\ (((((exists ff_h_pvs_one_prefix_sourceentryrightpositive. ff_h_pvs_one_prefix_sourceentryrightpositive + S (dst_positive_one_prefix_sourceentryright) = S ((S (dc_quotient_one_prefix_sourceentry)) * dst_positive_scale_one_prefix_sourceentryright)) /\ exists ff_q_pvs_one_prefix_sourceentryrightpositive. dst_positive_code_one_prefix_sourceentryright = ff_q_pvs_one_prefix_sourceentryrightpositive * S ((S (dc_quotient_one_prefix_sourceentry)) * dst_positive_scale_one_prefix_sourceentryright) + (dst_positive_one_prefix_sourceentryright))) /\ (((((exists ff_h_pvs_one_prefix_sourceentryrightnegative. ff_h_pvs_one_prefix_sourceentryrightnegative + S (dst_negative_one_prefix_sourceentryright) = S ((S (dc_quotient_one_prefix_sourceentry)) * dst_negative_scale_one_prefix_sourceentryright)) /\ exists ff_q_pvs_one_prefix_sourceentryrightnegative. dst_negative_code_one_prefix_sourceentryright = ff_q_pvs_one_prefix_sourceentryrightnegative * S ((S (dc_quotient_one_prefix_sourceentry)) * dst_negative_scale_one_prefix_sourceentryright) + (dst_negative_one_prefix_sourceentryright))) /\ (exists ge_balance_positive_one_prefix_sourceentryrightvalue ge_balance_negative_one_prefix_sourceentryrightvalue. (((((dc_right_one_prefix_sourceentry) = 2 * (ge_balance_positive_one_prefix_sourceentryrightvalue) /\ (ge_balance_negative_one_prefix_sourceentryrightvalue) = 0) \/ exists ge_signed_half_one_prefix_sourceentryrightvaluedecode. (((dc_right_one_prefix_sourceentry) = 2 * ge_signed_half_one_prefix_sourceentryrightvaluedecode + 1 /\ (ge_balance_positive_one_prefix_sourceentryrightvalue) = 0) /\ (ge_balance_negative_one_prefix_sourceentryrightvalue) = S ge_signed_half_one_prefix_sourceentryrightvaluedecode))) /\ ((dst_positive_one_prefix_sourceentryright) + ge_balance_negative_one_prefix_sourceentryrightvalue = (dst_negative_one_prefix_sourceentryright) + ge_balance_positive_one_prefix_sourceentryrightvalue))))))))) /\ (exists sto_ap_one_prefix_sourceentryproduct sto_an_one_prefix_sourceentryproduct sto_bp_one_prefix_sourceentryproduct sto_bn_one_prefix_sourceentryproduct sto_cp_one_prefix_sourceentryproduct sto_cn_one_prefix_sourceentryproduct. (((((dc_left_one_prefix_sourceentry) = 2 * (sto_ap_one_prefix_sourceentryproduct) /\ (sto_an_one_prefix_sourceentryproduct) = 0) \/ exists ge_signed_half_one_prefix_sourceentryproductleft. (((dc_left_one_prefix_sourceentry) = 2 * ge_signed_half_one_prefix_sourceentryproductleft + 1 /\ (sto_ap_one_prefix_sourceentryproduct) = 0) /\ (sto_an_one_prefix_sourceentryproduct) = S ge_signed_half_one_prefix_sourceentryproductleft))) /\ ((((((dc_right_one_prefix_sourceentry) = 2 * (sto_bp_one_prefix_sourceentryproduct) /\ (sto_bn_one_prefix_sourceentryproduct) = 0) \/ exists ge_signed_half_one_prefix_sourceentryproductright. (((dc_right_one_prefix_sourceentry) = 2 * ge_signed_half_one_prefix_sourceentryproductright + 1 /\ (sto_bp_one_prefix_sourceentryproduct) = 0) /\ (sto_bn_one_prefix_sourceentryproduct) = S ge_signed_half_one_prefix_sourceentryproductright))) /\ ((((((dc_value_one_prefix_source) = 2 * (sto_cp_one_prefix_sourceentryproduct) /\ (sto_cn_one_prefix_sourceentryproduct) = 0) \/ exists ge_signed_half_one_prefix_sourceentryproductoutput. (((dc_value_one_prefix_source) = 2 * ge_signed_half_one_prefix_sourceentryproductoutput + 1 /\ (sto_cp_one_prefix_sourceentryproduct) = 0) /\ (sto_cn_one_prefix_sourceentryproduct) = S ge_signed_half_one_prefix_sourceentryproductoutput))) /\ ((sto_ap_one_prefix_sourceentryproduct * sto_bp_one_prefix_sourceentryproduct + sto_an_one_prefix_sourceentryproduct * sto_bn_one_prefix_sourceentryproduct) + sto_cn_one_prefix_sourceentryproduct = (sto_ap_one_prefix_sourceentryproduct * sto_bn_one_prefix_sourceentryproduct + sto_an_one_prefix_sourceentryproduct * sto_bp_one_prefix_sourceentryproduct) + sto_cp_one_prefix_sourceentryproduct))))))))))))))) \/ ((((dc_index_one_prefix_source)=0 \/ ~(exists pvs_factor_one_prefix_sourceentrynondivisor. (n) = (dc_index_one_prefix_source) * pvs_factor_one_prefix_sourceentrynondivisor)) /\ ((dc_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 dm_index_one_prefix_result dm_value_one_prefix_result. (exists pvs_le_gap_one_prefix_resultdomain. pvs_le_gap_one_prefix_resultdomain + (dm_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 (dm_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 (dm_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 (dm_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 (dm_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. (((((dm_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. (((dm_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))))))))) -> ((((~((dm_index_one_prefix_result)=0)) /\ (exists dm_quotient_one_prefix_resultentry. (((n)=(dm_index_one_prefix_result)*dm_quotient_one_prefix_resultentry) /\ (exists dst_positive_code_one_prefix_resultentryinput dst_positive_scale_one_prefix_resultentryinput dst_negative_code_one_prefix_resultentryinput dst_negative_scale_one_prefix_resultentryinput dst_positive_one_prefix_resultentryinput dst_negative_one_prefix_resultentryinput. (((F) = (((((dst_positive_code_one_prefix_resultentryinput) + (dst_positive_scale_one_prefix_resultentryinput)) * S ((dst_positive_code_one_prefix_resultentryinput) + (dst_positive_scale_one_prefix_resultentryinput)) + ((dst_positive_scale_one_prefix_resultentryinput) + (dst_positive_scale_one_prefix_resultentryinput))) + (((dst_negative_code_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)) * S ((dst_negative_code_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)) + ((dst_negative_scale_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)))) * S ((((dst_positive_code_one_prefix_resultentryinput) + (dst_positive_scale_one_prefix_resultentryinput)) * S ((dst_positive_code_one_prefix_resultentryinput) + (dst_positive_scale_one_prefix_resultentryinput)) + ((dst_positive_scale_one_prefix_resultentryinput) + (dst_positive_scale_one_prefix_resultentryinput))) + (((dst_negative_code_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)) * S ((dst_negative_code_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)) + ((dst_negative_scale_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)))) + ((((dst_negative_code_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)) * S ((dst_negative_code_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)) + ((dst_negative_scale_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput))) + (((dst_negative_code_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)) * S ((dst_negative_code_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)) + ((dst_negative_scale_one_prefix_resultentryinput) + (dst_negative_scale_one_prefix_resultentryinput)))))) /\ (((((exists ff_h_pvs_one_prefix_resultentryinputpositive. ff_h_pvs_one_prefix_resultentryinputpositive + S (dst_positive_one_prefix_resultentryinput) = S ((S (dm_index_one_prefix_result)) * dst_positive_scale_one_prefix_resultentryinput)) /\ exists ff_q_pvs_one_prefix_resultentryinputpositive. dst_positive_code_one_prefix_resultentryinput = ff_q_pvs_one_prefix_resultentryinputpositive * S ((S (dm_index_one_prefix_result)) * dst_positive_scale_one_prefix_resultentryinput) + (dst_positive_one_prefix_resultentryinput))) /\ (((((exists ff_h_pvs_one_prefix_resultentryinputnegative. ff_h_pvs_one_prefix_resultentryinputnegative + S (dst_negative_one_prefix_resultentryinput) = S ((S (dm_index_one_prefix_result)) * dst_negative_scale_one_prefix_resultentryinput)) /\ exists ff_q_pvs_one_prefix_resultentryinputnegative. dst_negative_code_one_prefix_resultentryinput = ff_q_pvs_one_prefix_resultentryinputnegative * S ((S (dm_index_one_prefix_result)) * dst_negative_scale_one_prefix_resultentryinput) + (dst_negative_one_prefix_resultentryinput))) /\ (exists ge_balance_positive_one_prefix_resultentryinputvalue ge_balance_negative_one_prefix_resultentryinputvalue. (((((dm_value_one_prefix_result) = 2 * (ge_balance_positive_one_prefix_resultentryinputvalue) /\ (ge_balance_negative_one_prefix_resultentryinputvalue) = 0) \/ exists ge_signed_half_one_prefix_resultentryinputvaluedecode. (((dm_value_one_prefix_result) = 2 * ge_signed_half_one_prefix_resultentryinputvaluedecode + 1 /\ (ge_balance_positive_one_prefix_resultentryinputvalue) = 0) /\ (ge_balance_negative_one_prefix_resultentryinputvalue) = S ge_signed_half_one_prefix_resultentryinputvaluedecode))) /\ ((dst_positive_one_prefix_resultentryinput) + ge_balance_negative_one_prefix_resultentryinputvalue = (dst_negative_one_prefix_resultentryinput) + ge_balance_positive_one_prefix_resultentryinputvalue))))))))))))) \/ ((((dm_index_one_prefix_result)=0 \/ ~(exists pvs_factor_one_prefix_resultentrynondivisor. (n) = (dm_index_one_prefix_result) * pvs_factor_one_prefix_resultentrynondivisor)) /\ ((dm_value_one_prefix_result)=0)))))))