divisor_mask_prefix_zero_constructor

Exact expanded first-order arithmetic statement

forall F n M. (exists dst_positive_code_base_table dst_positive_scale_base_table dst_negative_code_base_table dst_negative_scale_base_table. (((M) = (((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) * S ((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) + ((((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))))) /\ (forall dst_index_base_table. (exists pvs_le_gap_base_tabledomain. pvs_le_gap_base_tabledomain + (dst_index_base_table) = (0)) -> exists dst_positive_base_table dst_negative_base_table dst_value_base_table. ((((exists ff_h_pvs_base_tableentrypositive. ff_h_pvs_base_tableentrypositive + S (dst_positive_base_table) = S ((S (dst_index_base_table)) * dst_positive_scale_base_table)) /\ exists ff_q_pvs_base_tableentrypositive. dst_positive_code_base_table = ff_q_pvs_base_tableentrypositive * S ((S (dst_index_base_table)) * dst_positive_scale_base_table) + (dst_positive_base_table))) /\ (((((exists ff_h_pvs_base_tableentrynegative. ff_h_pvs_base_tableentrynegative + S (dst_negative_base_table) = S ((S (dst_index_base_table)) * dst_negative_scale_base_table)) /\ exists ff_q_pvs_base_tableentrynegative. dst_negative_code_base_table = ff_q_pvs_base_tableentrynegative * S ((S (dst_index_base_table)) * dst_negative_scale_base_table) + (dst_negative_base_table))) /\ (exists ge_balance_positive_base_tableentryvalue ge_balance_negative_base_tableentryvalue. (((((dst_value_base_table) = 2 * (ge_balance_positive_base_tableentryvalue) /\ (ge_balance_negative_base_tableentryvalue) = 0) \/ exists ge_signed_half_base_tableentryvaluedecode. (((dst_value_base_table) = 2 * ge_signed_half_base_tableentryvaluedecode + 1 /\ (ge_balance_positive_base_tableentryvalue) = 0) /\ (ge_balance_negative_base_tableentryvalue) = S ge_signed_half_base_tableentryvaluedecode))) /\ ((dst_positive_base_table) + ge_balance_negative_base_tableentryvalue = (dst_negative_base_table) + ge_balance_positive_base_tableentryvalue))))))))) -> (exists dst_positive_code_base_entry dst_positive_scale_base_entry dst_negative_code_base_entry dst_negative_scale_base_entry dst_positive_base_entry dst_negative_base_entry. (((M) = (((((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) * S ((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) + ((dst_positive_scale_base_entry) + (dst_positive_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))) * S ((((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) * S ((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) + ((dst_positive_scale_base_entry) + (dst_positive_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))) + ((((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))))) /\ (((((exists ff_h_pvs_base_entrypositive. ff_h_pvs_base_entrypositive + S (dst_positive_base_entry) = S ((S (0)) * dst_positive_scale_base_entry)) /\ exists ff_q_pvs_base_entrypositive. dst_positive_code_base_entry = ff_q_pvs_base_entrypositive * S ((S (0)) * dst_positive_scale_base_entry) + (dst_positive_base_entry))) /\ (((((exists ff_h_pvs_base_entrynegative. ff_h_pvs_base_entrynegative + S (dst_negative_base_entry) = S ((S (0)) * dst_negative_scale_base_entry)) /\ exists ff_q_pvs_base_entrynegative. dst_negative_code_base_entry = ff_q_pvs_base_entrynegative * S ((S (0)) * dst_negative_scale_base_entry) + (dst_negative_base_entry))) /\ (exists ge_balance_positive_base_entryvalue ge_balance_negative_base_entryvalue. (((((0) = 2 * (ge_balance_positive_base_entryvalue) /\ (ge_balance_negative_base_entryvalue) = 0) \/ exists ge_signed_half_base_entryvaluedecode. (((0) = 2 * ge_signed_half_base_entryvaluedecode + 1 /\ (ge_balance_positive_base_entryvalue) = 0) /\ (ge_balance_negative_base_entryvalue) = S ge_signed_half_base_entryvaluedecode))) /\ ((dst_positive_base_entry) + ge_balance_negative_base_entryvalue = (dst_negative_base_entry) + ge_balance_positive_base_entryvalue))))))))) -> (((exists dst_positive_code_base_resulttable dst_positive_scale_base_resulttable dst_negative_code_base_resulttable dst_negative_scale_base_resulttable. (((M) = (((((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) * S ((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) + ((dst_positive_scale_base_resulttable) + (dst_positive_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))) * S ((((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) * S ((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) + ((dst_positive_scale_base_resulttable) + (dst_positive_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))) + ((((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))))) /\ (forall dst_index_base_resulttable. (exists pvs_le_gap_base_resulttabledomain. pvs_le_gap_base_resulttabledomain + (dst_index_base_resulttable) = (0)) -> exists dst_positive_base_resulttable dst_negative_base_resulttable dst_value_base_resulttable. ((((exists ff_h_pvs_base_resulttableentrypositive. ff_h_pvs_base_resulttableentrypositive + S (dst_positive_base_resulttable) = S ((S (dst_index_base_resulttable)) * dst_positive_scale_base_resulttable)) /\ exists ff_q_pvs_base_resulttableentrypositive. dst_positive_code_base_resulttable = ff_q_pvs_base_resulttableentrypositive * S ((S (dst_index_base_resulttable)) * dst_positive_scale_base_resulttable) + (dst_positive_base_resulttable))) /\ (((((exists ff_h_pvs_base_resulttableentrynegative. ff_h_pvs_base_resulttableentrynegative + S (dst_negative_base_resulttable) = S ((S (dst_index_base_resulttable)) * dst_negative_scale_base_resulttable)) /\ exists ff_q_pvs_base_resulttableentrynegative. dst_negative_code_base_resulttable = ff_q_pvs_base_resulttableentrynegative * S ((S (dst_index_base_resulttable)) * dst_negative_scale_base_resulttable) + (dst_negative_base_resulttable))) /\ (exists ge_balance_positive_base_resulttableentryvalue ge_balance_negative_base_resulttableentryvalue. (((((dst_value_base_resulttable) = 2 * (ge_balance_positive_base_resulttableentryvalue) /\ (ge_balance_negative_base_resulttableentryvalue) = 0) \/ exists ge_signed_half_base_resulttableentryvaluedecode. (((dst_value_base_resulttable) = 2 * ge_signed_half_base_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_base_resulttableentryvalue) = 0) /\ (ge_balance_negative_base_resulttableentryvalue) = S ge_signed_half_base_resulttableentryvaluedecode))) /\ ((dst_positive_base_resulttable) + ge_balance_negative_base_resulttableentryvalue = (dst_negative_base_resulttable) + ge_balance_positive_base_resulttableentryvalue))))))))) /\ (forall dm_index_base_result dm_value_base_result. (exists pvs_le_gap_base_resultdomain. pvs_le_gap_base_resultdomain + (dm_index_base_result) = (0)) -> (exists dst_positive_code_base_resultlookup dst_positive_scale_base_resultlookup dst_negative_code_base_resultlookup dst_negative_scale_base_resultlookup dst_positive_base_resultlookup dst_negative_base_resultlookup. (((M) = (((((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) * S ((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) + ((dst_positive_scale_base_resultlookup) + (dst_positive_scale_base_resultlookup))) + (((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup)))) * S ((((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) * S ((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) + ((dst_positive_scale_base_resultlookup) + (dst_positive_scale_base_resultlookup))) + (((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup)))) + ((((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup))) + (((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup)))))) /\ (((((exists ff_h_pvs_base_resultlookuppositive. ff_h_pvs_base_resultlookuppositive + S (dst_positive_base_resultlookup) = S ((S (dm_index_base_result)) * dst_positive_scale_base_resultlookup)) /\ exists ff_q_pvs_base_resultlookuppositive. dst_positive_code_base_resultlookup = ff_q_pvs_base_resultlookuppositive * S ((S (dm_index_base_result)) * dst_positive_scale_base_resultlookup) + (dst_positive_base_resultlookup))) /\ (((((exists ff_h_pvs_base_resultlookupnegative. ff_h_pvs_base_resultlookupnegative + S (dst_negative_base_resultlookup) = S ((S (dm_index_base_result)) * dst_negative_scale_base_resultlookup)) /\ exists ff_q_pvs_base_resultlookupnegative. dst_negative_code_base_resultlookup = ff_q_pvs_base_resultlookupnegative * S ((S (dm_index_base_result)) * dst_negative_scale_base_resultlookup) + (dst_negative_base_resultlookup))) /\ (exists ge_balance_positive_base_resultlookupvalue ge_balance_negative_base_resultlookupvalue. (((((dm_value_base_result) = 2 * (ge_balance_positive_base_resultlookupvalue) /\ (ge_balance_negative_base_resultlookupvalue) = 0) \/ exists ge_signed_half_base_resultlookupvaluedecode. (((dm_value_base_result) = 2 * ge_signed_half_base_resultlookupvaluedecode + 1 /\ (ge_balance_positive_base_resultlookupvalue) = 0) /\ (ge_balance_negative_base_resultlookupvalue) = S ge_signed_half_base_resultlookupvaluedecode))) /\ ((dst_positive_base_resultlookup) + ge_balance_negative_base_resultlookupvalue = (dst_negative_base_resultlookup) + ge_balance_positive_base_resultlookupvalue))))))))) -> ((((~((dm_index_base_result)=0)) /\ (exists dm_quotient_base_resultentry. (((n)=(dm_index_base_result)*dm_quotient_base_resultentry) /\ (exists dst_positive_code_base_resultentryinput dst_positive_scale_base_resultentryinput dst_negative_code_base_resultentryinput dst_negative_scale_base_resultentryinput dst_positive_base_resultentryinput dst_negative_base_resultentryinput. (((F) = (((((dst_positive_code_base_resultentryinput) + (dst_positive_scale_base_resultentryinput)) * S ((dst_positive_code_base_resultentryinput) + (dst_positive_scale_base_resultentryinput)) + ((dst_positive_scale_base_resultentryinput) + (dst_positive_scale_base_resultentryinput))) + (((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) * S ((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) + ((dst_negative_scale_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)))) * S ((((dst_positive_code_base_resultentryinput) + (dst_positive_scale_base_resultentryinput)) * S ((dst_positive_code_base_resultentryinput) + (dst_positive_scale_base_resultentryinput)) + ((dst_positive_scale_base_resultentryinput) + (dst_positive_scale_base_resultentryinput))) + (((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) * S ((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) + ((dst_negative_scale_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)))) + ((((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) * S ((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) + ((dst_negative_scale_base_resultentryinput) + (dst_negative_scale_base_resultentryinput))) + (((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) * S ((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) + ((dst_negative_scale_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)))))) /\ (((((exists ff_h_pvs_base_resultentryinputpositive. ff_h_pvs_base_resultentryinputpositive + S (dst_positive_base_resultentryinput) = S ((S (dm_index_base_result)) * dst_positive_scale_base_resultentryinput)) /\ exists ff_q_pvs_base_resultentryinputpositive. dst_positive_code_base_resultentryinput = ff_q_pvs_base_resultentryinputpositive * S ((S (dm_index_base_result)) * dst_positive_scale_base_resultentryinput) + (dst_positive_base_resultentryinput))) /\ (((((exists ff_h_pvs_base_resultentryinputnegative. ff_h_pvs_base_resultentryinputnegative + S (dst_negative_base_resultentryinput) = S ((S (dm_index_base_result)) * dst_negative_scale_base_resultentryinput)) /\ exists ff_q_pvs_base_resultentryinputnegative. dst_negative_code_base_resultentryinput = ff_q_pvs_base_resultentryinputnegative * S ((S (dm_index_base_result)) * dst_negative_scale_base_resultentryinput) + (dst_negative_base_resultentryinput))) /\ (exists ge_balance_positive_base_resultentryinputvalue ge_balance_negative_base_resultentryinputvalue. (((((dm_value_base_result) = 2 * (ge_balance_positive_base_resultentryinputvalue) /\ (ge_balance_negative_base_resultentryinputvalue) = 0) \/ exists ge_signed_half_base_resultentryinputvaluedecode. (((dm_value_base_result) = 2 * ge_signed_half_base_resultentryinputvaluedecode + 1 /\ (ge_balance_positive_base_resultentryinputvalue) = 0) /\ (ge_balance_negative_base_resultentryinputvalue) = S ge_signed_half_base_resultentryinputvaluedecode))) /\ ((dst_positive_base_resultentryinput) + ge_balance_negative_base_resultentryinputvalue = (dst_negative_base_resultentryinput) + ge_balance_positive_base_resultentryinputvalue))))))))))))) \/ ((((dm_index_base_result)=0 \/ ~(exists pvs_factor_base_resultentrynondivisor. (n) = (dm_index_base_result) * pvs_factor_base_resultentrynondivisor)) /\ ((dm_value_base_result)=0)))))))