divisor_mask_prefix_restrict

Exact expanded first-order arithmetic statement

forall F n l k M. (((exists dst_positive_code_restrict_masktable dst_positive_scale_restrict_masktable dst_negative_code_restrict_masktable dst_negative_scale_restrict_masktable. (((M) = (((((dst_positive_code_restrict_masktable) + (dst_positive_scale_restrict_masktable)) * S ((dst_positive_code_restrict_masktable) + (dst_positive_scale_restrict_masktable)) + ((dst_positive_scale_restrict_masktable) + (dst_positive_scale_restrict_masktable))) + (((dst_negative_code_restrict_masktable) + (dst_negative_scale_restrict_masktable)) * S ((dst_negative_code_restrict_masktable) + (dst_negative_scale_restrict_masktable)) + ((dst_negative_scale_restrict_masktable) + (dst_negative_scale_restrict_masktable)))) * S ((((dst_positive_code_restrict_masktable) + (dst_positive_scale_restrict_masktable)) * S ((dst_positive_code_restrict_masktable) + (dst_positive_scale_restrict_masktable)) + ((dst_positive_scale_restrict_masktable) + (dst_positive_scale_restrict_masktable))) + (((dst_negative_code_restrict_masktable) + (dst_negative_scale_restrict_masktable)) * S ((dst_negative_code_restrict_masktable) + (dst_negative_scale_restrict_masktable)) + ((dst_negative_scale_restrict_masktable) + (dst_negative_scale_restrict_masktable)))) + ((((dst_negative_code_restrict_masktable) + (dst_negative_scale_restrict_masktable)) * S ((dst_negative_code_restrict_masktable) + (dst_negative_scale_restrict_masktable)) + ((dst_negative_scale_restrict_masktable) + (dst_negative_scale_restrict_masktable))) + (((dst_negative_code_restrict_masktable) + (dst_negative_scale_restrict_masktable)) * S ((dst_negative_code_restrict_masktable) + (dst_negative_scale_restrict_masktable)) + ((dst_negative_scale_restrict_masktable) + (dst_negative_scale_restrict_masktable)))))) /\ (forall dst_index_restrict_masktable. (exists pvs_le_gap_restrict_masktabledomain. pvs_le_gap_restrict_masktabledomain + (dst_index_restrict_masktable) = (l)) -> exists dst_positive_restrict_masktable dst_negative_restrict_masktable dst_value_restrict_masktable. ((((exists ff_h_pvs_restrict_masktableentrypositive. ff_h_pvs_restrict_masktableentrypositive + S (dst_positive_restrict_masktable) = S ((S (dst_index_restrict_masktable)) * dst_positive_scale_restrict_masktable)) /\ exists ff_q_pvs_restrict_masktableentrypositive. dst_positive_code_restrict_masktable = ff_q_pvs_restrict_masktableentrypositive * S ((S (dst_index_restrict_masktable)) * dst_positive_scale_restrict_masktable) + (dst_positive_restrict_masktable))) /\ (((((exists ff_h_pvs_restrict_masktableentrynegative. ff_h_pvs_restrict_masktableentrynegative + S (dst_negative_restrict_masktable) = S ((S (dst_index_restrict_masktable)) * dst_negative_scale_restrict_masktable)) /\ exists ff_q_pvs_restrict_masktableentrynegative. dst_negative_code_restrict_masktable = ff_q_pvs_restrict_masktableentrynegative * S ((S (dst_index_restrict_masktable)) * dst_negative_scale_restrict_masktable) + (dst_negative_restrict_masktable))) /\ (exists ge_balance_positive_restrict_masktableentryvalue ge_balance_negative_restrict_masktableentryvalue. (((((dst_value_restrict_masktable) = 2 * (ge_balance_positive_restrict_masktableentryvalue) /\ (ge_balance_negative_restrict_masktableentryvalue) = 0) \/ exists ge_signed_half_restrict_masktableentryvaluedecode. (((dst_value_restrict_masktable) = 2 * ge_signed_half_restrict_masktableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_masktableentryvalue) = 0) /\ (ge_balance_negative_restrict_masktableentryvalue) = S ge_signed_half_restrict_masktableentryvaluedecode))) /\ ((dst_positive_restrict_masktable) + ge_balance_negative_restrict_masktableentryvalue = (dst_negative_restrict_masktable) + ge_balance_positive_restrict_masktableentryvalue))))))))) /\ (forall dm_index_restrict_mask dm_value_restrict_mask. (exists pvs_le_gap_restrict_maskdomain. pvs_le_gap_restrict_maskdomain + (dm_index_restrict_mask) = (l)) -> (exists dst_positive_code_restrict_masklookup dst_positive_scale_restrict_masklookup dst_negative_code_restrict_masklookup dst_negative_scale_restrict_masklookup dst_positive_restrict_masklookup dst_negative_restrict_masklookup. (((M) = (((((dst_positive_code_restrict_masklookup) + (dst_positive_scale_restrict_masklookup)) * S ((dst_positive_code_restrict_masklookup) + (dst_positive_scale_restrict_masklookup)) + ((dst_positive_scale_restrict_masklookup) + (dst_positive_scale_restrict_masklookup))) + (((dst_negative_code_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)) * S ((dst_negative_code_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)) + ((dst_negative_scale_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)))) * S ((((dst_positive_code_restrict_masklookup) + (dst_positive_scale_restrict_masklookup)) * S ((dst_positive_code_restrict_masklookup) + (dst_positive_scale_restrict_masklookup)) + ((dst_positive_scale_restrict_masklookup) + (dst_positive_scale_restrict_masklookup))) + (((dst_negative_code_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)) * S ((dst_negative_code_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)) + ((dst_negative_scale_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)))) + ((((dst_negative_code_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)) * S ((dst_negative_code_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)) + ((dst_negative_scale_restrict_masklookup) + (dst_negative_scale_restrict_masklookup))) + (((dst_negative_code_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)) * S ((dst_negative_code_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)) + ((dst_negative_scale_restrict_masklookup) + (dst_negative_scale_restrict_masklookup)))))) /\ (((((exists ff_h_pvs_restrict_masklookuppositive. ff_h_pvs_restrict_masklookuppositive + S (dst_positive_restrict_masklookup) = S ((S (dm_index_restrict_mask)) * dst_positive_scale_restrict_masklookup)) /\ exists ff_q_pvs_restrict_masklookuppositive. dst_positive_code_restrict_masklookup = ff_q_pvs_restrict_masklookuppositive * S ((S (dm_index_restrict_mask)) * dst_positive_scale_restrict_masklookup) + (dst_positive_restrict_masklookup))) /\ (((((exists ff_h_pvs_restrict_masklookupnegative. ff_h_pvs_restrict_masklookupnegative + S (dst_negative_restrict_masklookup) = S ((S (dm_index_restrict_mask)) * dst_negative_scale_restrict_masklookup)) /\ exists ff_q_pvs_restrict_masklookupnegative. dst_negative_code_restrict_masklookup = ff_q_pvs_restrict_masklookupnegative * S ((S (dm_index_restrict_mask)) * dst_negative_scale_restrict_masklookup) + (dst_negative_restrict_masklookup))) /\ (exists ge_balance_positive_restrict_masklookupvalue ge_balance_negative_restrict_masklookupvalue. (((((dm_value_restrict_mask) = 2 * (ge_balance_positive_restrict_masklookupvalue) /\ (ge_balance_negative_restrict_masklookupvalue) = 0) \/ exists ge_signed_half_restrict_masklookupvaluedecode. (((dm_value_restrict_mask) = 2 * ge_signed_half_restrict_masklookupvaluedecode + 1 /\ (ge_balance_positive_restrict_masklookupvalue) = 0) /\ (ge_balance_negative_restrict_masklookupvalue) = S ge_signed_half_restrict_masklookupvaluedecode))) /\ ((dst_positive_restrict_masklookup) + ge_balance_negative_restrict_masklookupvalue = (dst_negative_restrict_masklookup) + ge_balance_positive_restrict_masklookupvalue))))))))) -> ((((~((dm_index_restrict_mask)=0)) /\ (exists dm_quotient_restrict_maskentry. (((n)=(dm_index_restrict_mask)*dm_quotient_restrict_maskentry) /\ (exists dst_positive_code_restrict_maskentryinput dst_positive_scale_restrict_maskentryinput dst_negative_code_restrict_maskentryinput dst_negative_scale_restrict_maskentryinput dst_positive_restrict_maskentryinput dst_negative_restrict_maskentryinput. (((F) = (((((dst_positive_code_restrict_maskentryinput) + (dst_positive_scale_restrict_maskentryinput)) * S ((dst_positive_code_restrict_maskentryinput) + (dst_positive_scale_restrict_maskentryinput)) + ((dst_positive_scale_restrict_maskentryinput) + (dst_positive_scale_restrict_maskentryinput))) + (((dst_negative_code_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)) * S ((dst_negative_code_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)) + ((dst_negative_scale_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)))) * S ((((dst_positive_code_restrict_maskentryinput) + (dst_positive_scale_restrict_maskentryinput)) * S ((dst_positive_code_restrict_maskentryinput) + (dst_positive_scale_restrict_maskentryinput)) + ((dst_positive_scale_restrict_maskentryinput) + (dst_positive_scale_restrict_maskentryinput))) + (((dst_negative_code_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)) * S ((dst_negative_code_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)) + ((dst_negative_scale_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)))) + ((((dst_negative_code_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)) * S ((dst_negative_code_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)) + ((dst_negative_scale_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput))) + (((dst_negative_code_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)) * S ((dst_negative_code_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)) + ((dst_negative_scale_restrict_maskentryinput) + (dst_negative_scale_restrict_maskentryinput)))))) /\ (((((exists ff_h_pvs_restrict_maskentryinputpositive. ff_h_pvs_restrict_maskentryinputpositive + S (dst_positive_restrict_maskentryinput) = S ((S (dm_index_restrict_mask)) * dst_positive_scale_restrict_maskentryinput)) /\ exists ff_q_pvs_restrict_maskentryinputpositive. dst_positive_code_restrict_maskentryinput = ff_q_pvs_restrict_maskentryinputpositive * S ((S (dm_index_restrict_mask)) * dst_positive_scale_restrict_maskentryinput) + (dst_positive_restrict_maskentryinput))) /\ (((((exists ff_h_pvs_restrict_maskentryinputnegative. ff_h_pvs_restrict_maskentryinputnegative + S (dst_negative_restrict_maskentryinput) = S ((S (dm_index_restrict_mask)) * dst_negative_scale_restrict_maskentryinput)) /\ exists ff_q_pvs_restrict_maskentryinputnegative. dst_negative_code_restrict_maskentryinput = ff_q_pvs_restrict_maskentryinputnegative * S ((S (dm_index_restrict_mask)) * dst_negative_scale_restrict_maskentryinput) + (dst_negative_restrict_maskentryinput))) /\ (exists ge_balance_positive_restrict_maskentryinputvalue ge_balance_negative_restrict_maskentryinputvalue. (((((dm_value_restrict_mask) = 2 * (ge_balance_positive_restrict_maskentryinputvalue) /\ (ge_balance_negative_restrict_maskentryinputvalue) = 0) \/ exists ge_signed_half_restrict_maskentryinputvaluedecode. (((dm_value_restrict_mask) = 2 * ge_signed_half_restrict_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_restrict_maskentryinputvalue) = 0) /\ (ge_balance_negative_restrict_maskentryinputvalue) = S ge_signed_half_restrict_maskentryinputvaluedecode))) /\ ((dst_positive_restrict_maskentryinput) + ge_balance_negative_restrict_maskentryinputvalue = (dst_negative_restrict_maskentryinput) + ge_balance_positive_restrict_maskentryinputvalue))))))))))))) \/ ((((dm_index_restrict_mask)=0 \/ ~(exists pvs_factor_restrict_maskentrynondivisor. (n) = (dm_index_restrict_mask) * pvs_factor_restrict_maskentrynondivisor)) /\ ((dm_value_restrict_mask)=0))))))) -> (exists pvs_le_gap_restrict_bound. pvs_le_gap_restrict_bound + (k) = (l)) -> (((exists dst_positive_code_restrict_resulttable dst_positive_scale_restrict_resulttable dst_negative_code_restrict_resulttable dst_negative_scale_restrict_resulttable. (((M) = (((((dst_positive_code_restrict_resulttable) + (dst_positive_scale_restrict_resulttable)) * S ((dst_positive_code_restrict_resulttable) + (dst_positive_scale_restrict_resulttable)) + ((dst_positive_scale_restrict_resulttable) + (dst_positive_scale_restrict_resulttable))) + (((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) * S ((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) + ((dst_negative_scale_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)))) * S ((((dst_positive_code_restrict_resulttable) + (dst_positive_scale_restrict_resulttable)) * S ((dst_positive_code_restrict_resulttable) + (dst_positive_scale_restrict_resulttable)) + ((dst_positive_scale_restrict_resulttable) + (dst_positive_scale_restrict_resulttable))) + (((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) * S ((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) + ((dst_negative_scale_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)))) + ((((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) * S ((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) + ((dst_negative_scale_restrict_resulttable) + (dst_negative_scale_restrict_resulttable))) + (((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) * S ((dst_negative_code_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)) + ((dst_negative_scale_restrict_resulttable) + (dst_negative_scale_restrict_resulttable)))))) /\ (forall dst_index_restrict_resulttable. (exists pvs_le_gap_restrict_resulttabledomain. pvs_le_gap_restrict_resulttabledomain + (dst_index_restrict_resulttable) = (k)) -> exists dst_positive_restrict_resulttable dst_negative_restrict_resulttable dst_value_restrict_resulttable. ((((exists ff_h_pvs_restrict_resulttableentrypositive. ff_h_pvs_restrict_resulttableentrypositive + S (dst_positive_restrict_resulttable) = S ((S (dst_index_restrict_resulttable)) * dst_positive_scale_restrict_resulttable)) /\ exists ff_q_pvs_restrict_resulttableentrypositive. dst_positive_code_restrict_resulttable = ff_q_pvs_restrict_resulttableentrypositive * S ((S (dst_index_restrict_resulttable)) * dst_positive_scale_restrict_resulttable) + (dst_positive_restrict_resulttable))) /\ (((((exists ff_h_pvs_restrict_resulttableentrynegative. ff_h_pvs_restrict_resulttableentrynegative + S (dst_negative_restrict_resulttable) = S ((S (dst_index_restrict_resulttable)) * dst_negative_scale_restrict_resulttable)) /\ exists ff_q_pvs_restrict_resulttableentrynegative. dst_negative_code_restrict_resulttable = ff_q_pvs_restrict_resulttableentrynegative * S ((S (dst_index_restrict_resulttable)) * dst_negative_scale_restrict_resulttable) + (dst_negative_restrict_resulttable))) /\ (exists ge_balance_positive_restrict_resulttableentryvalue ge_balance_negative_restrict_resulttableentryvalue. (((((dst_value_restrict_resulttable) = 2 * (ge_balance_positive_restrict_resulttableentryvalue) /\ (ge_balance_negative_restrict_resulttableentryvalue) = 0) \/ exists ge_signed_half_restrict_resulttableentryvaluedecode. (((dst_value_restrict_resulttable) = 2 * ge_signed_half_restrict_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_resulttableentryvalue) = 0) /\ (ge_balance_negative_restrict_resulttableentryvalue) = S ge_signed_half_restrict_resulttableentryvaluedecode))) /\ ((dst_positive_restrict_resulttable) + ge_balance_negative_restrict_resulttableentryvalue = (dst_negative_restrict_resulttable) + ge_balance_positive_restrict_resulttableentryvalue))))))))) /\ (forall dm_index_restrict_result dm_value_restrict_result. (exists pvs_le_gap_restrict_resultdomain. pvs_le_gap_restrict_resultdomain + (dm_index_restrict_result) = (k)) -> (exists dst_positive_code_restrict_resultlookup dst_positive_scale_restrict_resultlookup dst_negative_code_restrict_resultlookup dst_negative_scale_restrict_resultlookup dst_positive_restrict_resultlookup dst_negative_restrict_resultlookup. (((M) = (((((dst_positive_code_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup)) * S ((dst_positive_code_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup)) + ((dst_positive_scale_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup))) + (((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) * S ((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) + ((dst_negative_scale_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)))) * S ((((dst_positive_code_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup)) * S ((dst_positive_code_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup)) + ((dst_positive_scale_restrict_resultlookup) + (dst_positive_scale_restrict_resultlookup))) + (((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) * S ((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) + ((dst_negative_scale_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)))) + ((((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) * S ((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) + ((dst_negative_scale_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup))) + (((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) * S ((dst_negative_code_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)) + ((dst_negative_scale_restrict_resultlookup) + (dst_negative_scale_restrict_resultlookup)))))) /\ (((((exists ff_h_pvs_restrict_resultlookuppositive. ff_h_pvs_restrict_resultlookuppositive + S (dst_positive_restrict_resultlookup) = S ((S (dm_index_restrict_result)) * dst_positive_scale_restrict_resultlookup)) /\ exists ff_q_pvs_restrict_resultlookuppositive. dst_positive_code_restrict_resultlookup = ff_q_pvs_restrict_resultlookuppositive * S ((S (dm_index_restrict_result)) * dst_positive_scale_restrict_resultlookup) + (dst_positive_restrict_resultlookup))) /\ (((((exists ff_h_pvs_restrict_resultlookupnegative. ff_h_pvs_restrict_resultlookupnegative + S (dst_negative_restrict_resultlookup) = S ((S (dm_index_restrict_result)) * dst_negative_scale_restrict_resultlookup)) /\ exists ff_q_pvs_restrict_resultlookupnegative. dst_negative_code_restrict_resultlookup = ff_q_pvs_restrict_resultlookupnegative * S ((S (dm_index_restrict_result)) * dst_negative_scale_restrict_resultlookup) + (dst_negative_restrict_resultlookup))) /\ (exists ge_balance_positive_restrict_resultlookupvalue ge_balance_negative_restrict_resultlookupvalue. (((((dm_value_restrict_result) = 2 * (ge_balance_positive_restrict_resultlookupvalue) /\ (ge_balance_negative_restrict_resultlookupvalue) = 0) \/ exists ge_signed_half_restrict_resultlookupvaluedecode. (((dm_value_restrict_result) = 2 * ge_signed_half_restrict_resultlookupvaluedecode + 1 /\ (ge_balance_positive_restrict_resultlookupvalue) = 0) /\ (ge_balance_negative_restrict_resultlookupvalue) = S ge_signed_half_restrict_resultlookupvaluedecode))) /\ ((dst_positive_restrict_resultlookup) + ge_balance_negative_restrict_resultlookupvalue = (dst_negative_restrict_resultlookup) + ge_balance_positive_restrict_resultlookupvalue))))))))) -> ((((~((dm_index_restrict_result)=0)) /\ (exists dm_quotient_restrict_resultentry. (((n)=(dm_index_restrict_result)*dm_quotient_restrict_resultentry) /\ (exists dst_positive_code_restrict_resultentryinput dst_positive_scale_restrict_resultentryinput dst_negative_code_restrict_resultentryinput dst_negative_scale_restrict_resultentryinput dst_positive_restrict_resultentryinput dst_negative_restrict_resultentryinput. (((F) = (((((dst_positive_code_restrict_resultentryinput) + (dst_positive_scale_restrict_resultentryinput)) * S ((dst_positive_code_restrict_resultentryinput) + (dst_positive_scale_restrict_resultentryinput)) + ((dst_positive_scale_restrict_resultentryinput) + (dst_positive_scale_restrict_resultentryinput))) + (((dst_negative_code_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)) * S ((dst_negative_code_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)) + ((dst_negative_scale_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)))) * S ((((dst_positive_code_restrict_resultentryinput) + (dst_positive_scale_restrict_resultentryinput)) * S ((dst_positive_code_restrict_resultentryinput) + (dst_positive_scale_restrict_resultentryinput)) + ((dst_positive_scale_restrict_resultentryinput) + (dst_positive_scale_restrict_resultentryinput))) + (((dst_negative_code_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)) * S ((dst_negative_code_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)) + ((dst_negative_scale_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)))) + ((((dst_negative_code_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)) * S ((dst_negative_code_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)) + ((dst_negative_scale_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput))) + (((dst_negative_code_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)) * S ((dst_negative_code_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)) + ((dst_negative_scale_restrict_resultentryinput) + (dst_negative_scale_restrict_resultentryinput)))))) /\ (((((exists ff_h_pvs_restrict_resultentryinputpositive. ff_h_pvs_restrict_resultentryinputpositive + S (dst_positive_restrict_resultentryinput) = S ((S (dm_index_restrict_result)) * dst_positive_scale_restrict_resultentryinput)) /\ exists ff_q_pvs_restrict_resultentryinputpositive. dst_positive_code_restrict_resultentryinput = ff_q_pvs_restrict_resultentryinputpositive * S ((S (dm_index_restrict_result)) * dst_positive_scale_restrict_resultentryinput) + (dst_positive_restrict_resultentryinput))) /\ (((((exists ff_h_pvs_restrict_resultentryinputnegative. ff_h_pvs_restrict_resultentryinputnegative + S (dst_negative_restrict_resultentryinput) = S ((S (dm_index_restrict_result)) * dst_negative_scale_restrict_resultentryinput)) /\ exists ff_q_pvs_restrict_resultentryinputnegative. dst_negative_code_restrict_resultentryinput = ff_q_pvs_restrict_resultentryinputnegative * S ((S (dm_index_restrict_result)) * dst_negative_scale_restrict_resultentryinput) + (dst_negative_restrict_resultentryinput))) /\ (exists ge_balance_positive_restrict_resultentryinputvalue ge_balance_negative_restrict_resultentryinputvalue. (((((dm_value_restrict_result) = 2 * (ge_balance_positive_restrict_resultentryinputvalue) /\ (ge_balance_negative_restrict_resultentryinputvalue) = 0) \/ exists ge_signed_half_restrict_resultentryinputvaluedecode. (((dm_value_restrict_result) = 2 * ge_signed_half_restrict_resultentryinputvaluedecode + 1 /\ (ge_balance_positive_restrict_resultentryinputvalue) = 0) /\ (ge_balance_negative_restrict_resultentryinputvalue) = S ge_signed_half_restrict_resultentryinputvaluedecode))) /\ ((dst_positive_restrict_resultentryinput) + ge_balance_negative_restrict_resultentryinputvalue = (dst_negative_restrict_resultentryinput) + ge_balance_positive_restrict_resultentryinputvalue))))))))))))) \/ ((((dm_index_restrict_result)=0 \/ ~(exists pvs_factor_restrict_resultentrynondivisor. (n) = (dm_index_restrict_result) * pvs_factor_restrict_resultentrynondivisor)) /\ ((dm_value_restrict_result)=0)))))))