divisor_mask_prefix_extensional

forall F n l M K. (((exists dst_positive_code_unique_first_masktable dst_positive_scale_unique_first_masktable dst_negative_code_unique_first_masktable dst_negative_scale_unique_first_masktable. (((M) = (((((dst_positive_code_unique_first_masktable) + (dst_positive_scale_unique_first_masktable)) * S ((dst_positive_code_unique_first_masktable) + (dst_positive_scale_unique_first_masktable)) + ((dst_positive_scale_unique_first_masktable) + (dst_positive_scale_unique_first_masktable))) + (((dst_negative_code_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)) * S ((dst_negative_code_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)) + ((dst_negative_scale_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)))) * S ((((dst_positive_code_unique_first_masktable) + (dst_positive_scale_unique_first_masktable)) * S ((dst_positive_code_unique_first_masktable) + (dst_positive_scale_unique_first_masktable)) + ((dst_positive_scale_unique_first_masktable) + (dst_positive_scale_unique_first_masktable))) + (((dst_negative_code_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)) * S ((dst_negative_code_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)) + ((dst_negative_scale_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)))) + ((((dst_negative_code_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)) * S ((dst_negative_code_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)) + ((dst_negative_scale_unique_first_masktable) + (dst_negative_scale_unique_first_masktable))) + (((dst_negative_code_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)) * S ((dst_negative_code_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)) + ((dst_negative_scale_unique_first_masktable) + (dst_negative_scale_unique_first_masktable)))))) /\ (forall dst_index_unique_first_masktable. (exists pvs_le_gap_unique_first_masktabledomain. pvs_le_gap_unique_first_masktabledomain + (dst_index_unique_first_masktable) = (l)) -> exists dst_positive_unique_first_masktable dst_negative_unique_first_masktable dst_value_unique_first_masktable. ((((exists ff_h_pvs_unique_first_masktableentrypositive. ff_h_pvs_unique_first_masktableentrypositive + S (dst_positive_unique_first_masktable) = S ((S (dst_index_unique_first_masktable)) * dst_positive_scale_unique_first_masktable)) /\ exists ff_q_pvs_unique_first_masktableentrypositive. dst_positive_code_unique_first_masktable = ff_q_pvs_unique_first_masktableentrypositive * S ((S (dst_index_unique_first_masktable)) * dst_positive_scale_unique_first_masktable) + (dst_positive_unique_first_masktable))) /\ (((((exists ff_h_pvs_unique_first_masktableentrynegative. ff_h_pvs_unique_first_masktableentrynegative + S (dst_negative_unique_first_masktable) = S ((S (dst_index_unique_first_masktable)) * dst_negative_scale_unique_first_masktable)) /\ exists ff_q_pvs_unique_first_masktableentrynegative. dst_negative_code_unique_first_masktable = ff_q_pvs_unique_first_masktableentrynegative * S ((S (dst_index_unique_first_masktable)) * dst_negative_scale_unique_first_masktable) + (dst_negative_unique_first_masktable))) /\ (exists ge_balance_positive_unique_first_masktableentryvalue ge_balance_negative_unique_first_masktableentryvalue. (((((dst_value_unique_first_masktable) = 2 * (ge_balance_positive_unique_first_masktableentryvalue) /\ (ge_balance_negative_unique_first_masktableentryvalue) = 0) \/ exists ge_signed_half_unique_first_masktableentryvaluedecode. (((dst_value_unique_first_masktable) = 2 * ge_signed_half_unique_first_masktableentryvaluedecode + 1 /\ (ge_balance_positive_unique_first_masktableentryvalue) = 0) /\ (ge_balance_negative_unique_first_masktableentryvalue) = S ge_signed_half_unique_first_masktableentryvaluedecode))) /\ ((dst_positive_unique_first_masktable) + ge_balance_negative_unique_first_masktableentryvalue = (dst_negative_unique_first_masktable) + ge_balance_positive_unique_first_masktableentryvalue))))))))) /\ (forall dm_index_unique_first_mask dm_value_unique_first_mask. (exists pvs_le_gap_unique_first_maskdomain. pvs_le_gap_unique_first_maskdomain + (dm_index_unique_first_mask) = (l)) -> (exists dst_positive_code_unique_first_masklookup dst_positive_scale_unique_first_masklookup dst_negative_code_unique_first_masklookup dst_negative_scale_unique_first_masklookup dst_positive_unique_first_masklookup dst_negative_unique_first_masklookup. (((M) = (((((dst_positive_code_unique_first_masklookup) + (dst_positive_scale_unique_first_masklookup)) * S ((dst_positive_code_unique_first_masklookup) + (dst_positive_scale_unique_first_masklookup)) + ((dst_positive_scale_unique_first_masklookup) + (dst_positive_scale_unique_first_masklookup))) + (((dst_negative_code_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)) * S ((dst_negative_code_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)) + ((dst_negative_scale_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)))) * S ((((dst_positive_code_unique_first_masklookup) + (dst_positive_scale_unique_first_masklookup)) * S ((dst_positive_code_unique_first_masklookup) + (dst_positive_scale_unique_first_masklookup)) + ((dst_positive_scale_unique_first_masklookup) + (dst_positive_scale_unique_first_masklookup))) + (((dst_negative_code_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)) * S ((dst_negative_code_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)) + ((dst_negative_scale_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)))) + ((((dst_negative_code_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)) * S ((dst_negative_code_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)) + ((dst_negative_scale_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup))) + (((dst_negative_code_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)) * S ((dst_negative_code_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)) + ((dst_negative_scale_unique_first_masklookup) + (dst_negative_scale_unique_first_masklookup)))))) /\ (((((exists ff_h_pvs_unique_first_masklookuppositive. ff_h_pvs_unique_first_masklookuppositive + S (dst_positive_unique_first_masklookup) = S ((S (dm_index_unique_first_mask)) * dst_positive_scale_unique_first_masklookup)) /\ exists ff_q_pvs_unique_first_masklookuppositive. dst_positive_code_unique_first_masklookup = ff_q_pvs_unique_first_masklookuppositive * S ((S (dm_index_unique_first_mask)) * dst_positive_scale_unique_first_masklookup) + (dst_positive_unique_first_masklookup))) /\ (((((exists ff_h_pvs_unique_first_masklookupnegative. ff_h_pvs_unique_first_masklookupnegative + S (dst_negative_unique_first_masklookup) = S ((S (dm_index_unique_first_mask)) * dst_negative_scale_unique_first_masklookup)) /\ exists ff_q_pvs_unique_first_masklookupnegative. dst_negative_code_unique_first_masklookup = ff_q_pvs_unique_first_masklookupnegative * S ((S (dm_index_unique_first_mask)) * dst_negative_scale_unique_first_masklookup) + (dst_negative_unique_first_masklookup))) /\ (exists ge_balance_positive_unique_first_masklookupvalue ge_balance_negative_unique_first_masklookupvalue. (((((dm_value_unique_first_mask) = 2 * (ge_balance_positive_unique_first_masklookupvalue) /\ (ge_balance_negative_unique_first_masklookupvalue) = 0) \/ exists ge_signed_half_unique_first_masklookupvaluedecode. (((dm_value_unique_first_mask) = 2 * ge_signed_half_unique_first_masklookupvaluedecode + 1 /\ (ge_balance_positive_unique_first_masklookupvalue) = 0) /\ (ge_balance_negative_unique_first_masklookupvalue) = S ge_signed_half_unique_first_masklookupvaluedecode))) /\ ((dst_positive_unique_first_masklookup) + ge_balance_negative_unique_first_masklookupvalue = (dst_negative_unique_first_masklookup) + ge_balance_positive_unique_first_masklookupvalue))))))))) -> ((((~((dm_index_unique_first_mask)=0)) /\ (exists dm_quotient_unique_first_maskentry. (((n)=(dm_index_unique_first_mask)*dm_quotient_unique_first_maskentry) /\ (exists dst_positive_code_unique_first_maskentryinput dst_positive_scale_unique_first_maskentryinput dst_negative_code_unique_first_maskentryinput dst_negative_scale_unique_first_maskentryinput dst_positive_unique_first_maskentryinput dst_negative_unique_first_maskentryinput. (((F) = (((((dst_positive_code_unique_first_maskentryinput) + (dst_positive_scale_unique_first_maskentryinput)) * S ((dst_positive_code_unique_first_maskentryinput) + (dst_positive_scale_unique_first_maskentryinput)) + ((dst_positive_scale_unique_first_maskentryinput) + (dst_positive_scale_unique_first_maskentryinput))) + (((dst_negative_code_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)) * S ((dst_negative_code_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)) + ((dst_negative_scale_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)))) * S ((((dst_positive_code_unique_first_maskentryinput) + (dst_positive_scale_unique_first_maskentryinput)) * S ((dst_positive_code_unique_first_maskentryinput) + (dst_positive_scale_unique_first_maskentryinput)) + ((dst_positive_scale_unique_first_maskentryinput) + (dst_positive_scale_unique_first_maskentryinput))) + (((dst_negative_code_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)) * S ((dst_negative_code_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)) + ((dst_negative_scale_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)))) + ((((dst_negative_code_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)) * S ((dst_negative_code_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)) + ((dst_negative_scale_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput))) + (((dst_negative_code_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)) * S ((dst_negative_code_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)) + ((dst_negative_scale_unique_first_maskentryinput) + (dst_negative_scale_unique_first_maskentryinput)))))) /\ (((((exists ff_h_pvs_unique_first_maskentryinputpositive. ff_h_pvs_unique_first_maskentryinputpositive + S (dst_positive_unique_first_maskentryinput) = S ((S (dm_index_unique_first_mask)) * dst_positive_scale_unique_first_maskentryinput)) /\ exists ff_q_pvs_unique_first_maskentryinputpositive. dst_positive_code_unique_first_maskentryinput = ff_q_pvs_unique_first_maskentryinputpositive * S ((S (dm_index_unique_first_mask)) * dst_positive_scale_unique_first_maskentryinput) + (dst_positive_unique_first_maskentryinput))) /\ (((((exists ff_h_pvs_unique_first_maskentryinputnegative. ff_h_pvs_unique_first_maskentryinputnegative + S (dst_negative_unique_first_maskentryinput) = S ((S (dm_index_unique_first_mask)) * dst_negative_scale_unique_first_maskentryinput)) /\ exists ff_q_pvs_unique_first_maskentryinputnegative. dst_negative_code_unique_first_maskentryinput = ff_q_pvs_unique_first_maskentryinputnegative * S ((S (dm_index_unique_first_mask)) * dst_negative_scale_unique_first_maskentryinput) + (dst_negative_unique_first_maskentryinput))) /\ (exists ge_balance_positive_unique_first_maskentryinputvalue ge_balance_negative_unique_first_maskentryinputvalue. (((((dm_value_unique_first_mask) = 2 * (ge_balance_positive_unique_first_maskentryinputvalue) /\ (ge_balance_negative_unique_first_maskentryinputvalue) = 0) \/ exists ge_signed_half_unique_first_maskentryinputvaluedecode. (((dm_value_unique_first_mask) = 2 * ge_signed_half_unique_first_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_unique_first_maskentryinputvalue) = 0) /\ (ge_balance_negative_unique_first_maskentryinputvalue) = S ge_signed_half_unique_first_maskentryinputvaluedecode))) /\ ((dst_positive_unique_first_maskentryinput) + ge_balance_negative_unique_first_maskentryinputvalue = (dst_negative_unique_first_maskentryinput) + ge_balance_positive_unique_first_maskentryinputvalue))))))))))))) \/ ((((dm_index_unique_first_mask)=0 \/ ~(exists pvs_factor_unique_first_maskentrynondivisor. (n) = (dm_index_unique_first_mask) * pvs_factor_unique_first_maskentrynondivisor)) /\ ((dm_value_unique_first_mask)=0))))))) -> (((exists dst_positive_code_unique_second_masktable dst_positive_scale_unique_second_masktable dst_negative_code_unique_second_masktable dst_negative_scale_unique_second_masktable. (((K) = (((((dst_positive_code_unique_second_masktable) + (dst_positive_scale_unique_second_masktable)) * S ((dst_positive_code_unique_second_masktable) + (dst_positive_scale_unique_second_masktable)) + ((dst_positive_scale_unique_second_masktable) + (dst_positive_scale_unique_second_masktable))) + (((dst_negative_code_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)) * S ((dst_negative_code_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)) + ((dst_negative_scale_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)))) * S ((((dst_positive_code_unique_second_masktable) + (dst_positive_scale_unique_second_masktable)) * S ((dst_positive_code_unique_second_masktable) + (dst_positive_scale_unique_second_masktable)) + ((dst_positive_scale_unique_second_masktable) + (dst_positive_scale_unique_second_masktable))) + (((dst_negative_code_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)) * S ((dst_negative_code_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)) + ((dst_negative_scale_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)))) + ((((dst_negative_code_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)) * S ((dst_negative_code_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)) + ((dst_negative_scale_unique_second_masktable) + (dst_negative_scale_unique_second_masktable))) + (((dst_negative_code_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)) * S ((dst_negative_code_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)) + ((dst_negative_scale_unique_second_masktable) + (dst_negative_scale_unique_second_masktable)))))) /\ (forall dst_index_unique_second_masktable. (exists pvs_le_gap_unique_second_masktabledomain. pvs_le_gap_unique_second_masktabledomain + (dst_index_unique_second_masktable) = (l)) -> exists dst_positive_unique_second_masktable dst_negative_unique_second_masktable dst_value_unique_second_masktable. ((((exists ff_h_pvs_unique_second_masktableentrypositive. ff_h_pvs_unique_second_masktableentrypositive + S (dst_positive_unique_second_masktable) = S ((S (dst_index_unique_second_masktable)) * dst_positive_scale_unique_second_masktable)) /\ exists ff_q_pvs_unique_second_masktableentrypositive. dst_positive_code_unique_second_masktable = ff_q_pvs_unique_second_masktableentrypositive * S ((S (dst_index_unique_second_masktable)) * dst_positive_scale_unique_second_masktable) + (dst_positive_unique_second_masktable))) /\ (((((exists ff_h_pvs_unique_second_masktableentrynegative. ff_h_pvs_unique_second_masktableentrynegative + S (dst_negative_unique_second_masktable) = S ((S (dst_index_unique_second_masktable)) * dst_negative_scale_unique_second_masktable)) /\ exists ff_q_pvs_unique_second_masktableentrynegative. dst_negative_code_unique_second_masktable = ff_q_pvs_unique_second_masktableentrynegative * S ((S (dst_index_unique_second_masktable)) * dst_negative_scale_unique_second_masktable) + (dst_negative_unique_second_masktable))) /\ (exists ge_balance_positive_unique_second_masktableentryvalue ge_balance_negative_unique_second_masktableentryvalue. (((((dst_value_unique_second_masktable) = 2 * (ge_balance_positive_unique_second_masktableentryvalue) /\ (ge_balance_negative_unique_second_masktableentryvalue) = 0) \/ exists ge_signed_half_unique_second_masktableentryvaluedecode. (((dst_value_unique_second_masktable) = 2 * ge_signed_half_unique_second_masktableentryvaluedecode + 1 /\ (ge_balance_positive_unique_second_masktableentryvalue) = 0) /\ (ge_balance_negative_unique_second_masktableentryvalue) = S ge_signed_half_unique_second_masktableentryvaluedecode))) /\ ((dst_positive_unique_second_masktable) + ge_balance_negative_unique_second_masktableentryvalue = (dst_negative_unique_second_masktable) + ge_balance_positive_unique_second_masktableentryvalue))))))))) /\ (forall dm_index_unique_second_mask dm_value_unique_second_mask. (exists pvs_le_gap_unique_second_maskdomain. pvs_le_gap_unique_second_maskdomain + (dm_index_unique_second_mask) = (l)) -> (exists dst_positive_code_unique_second_masklookup dst_positive_scale_unique_second_masklookup dst_negative_code_unique_second_masklookup dst_negative_scale_unique_second_masklookup dst_positive_unique_second_masklookup dst_negative_unique_second_masklookup. (((K) = (((((dst_positive_code_unique_second_masklookup) + (dst_positive_scale_unique_second_masklookup)) * S ((dst_positive_code_unique_second_masklookup) + (dst_positive_scale_unique_second_masklookup)) + ((dst_positive_scale_unique_second_masklookup) + (dst_positive_scale_unique_second_masklookup))) + (((dst_negative_code_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)) * S ((dst_negative_code_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)) + ((dst_negative_scale_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)))) * S ((((dst_positive_code_unique_second_masklookup) + (dst_positive_scale_unique_second_masklookup)) * S ((dst_positive_code_unique_second_masklookup) + (dst_positive_scale_unique_second_masklookup)) + ((dst_positive_scale_unique_second_masklookup) + (dst_positive_scale_unique_second_masklookup))) + (((dst_negative_code_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)) * S ((dst_negative_code_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)) + ((dst_negative_scale_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)))) + ((((dst_negative_code_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)) * S ((dst_negative_code_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)) + ((dst_negative_scale_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup))) + (((dst_negative_code_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)) * S ((dst_negative_code_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)) + ((dst_negative_scale_unique_second_masklookup) + (dst_negative_scale_unique_second_masklookup)))))) /\ (((((exists ff_h_pvs_unique_second_masklookuppositive. ff_h_pvs_unique_second_masklookuppositive + S (dst_positive_unique_second_masklookup) = S ((S (dm_index_unique_second_mask)) * dst_positive_scale_unique_second_masklookup)) /\ exists ff_q_pvs_unique_second_masklookuppositive. dst_positive_code_unique_second_masklookup = ff_q_pvs_unique_second_masklookuppositive * S ((S (dm_index_unique_second_mask)) * dst_positive_scale_unique_second_masklookup) + (dst_positive_unique_second_masklookup))) /\ (((((exists ff_h_pvs_unique_second_masklookupnegative. ff_h_pvs_unique_second_masklookupnegative + S (dst_negative_unique_second_masklookup) = S ((S (dm_index_unique_second_mask)) * dst_negative_scale_unique_second_masklookup)) /\ exists ff_q_pvs_unique_second_masklookupnegative. dst_negative_code_unique_second_masklookup = ff_q_pvs_unique_second_masklookupnegative * S ((S (dm_index_unique_second_mask)) * dst_negative_scale_unique_second_masklookup) + (dst_negative_unique_second_masklookup))) /\ (exists ge_balance_positive_unique_second_masklookupvalue ge_balance_negative_unique_second_masklookupvalue. (((((dm_value_unique_second_mask) = 2 * (ge_balance_positive_unique_second_masklookupvalue) /\ (ge_balance_negative_unique_second_masklookupvalue) = 0) \/ exists ge_signed_half_unique_second_masklookupvaluedecode. (((dm_value_unique_second_mask) = 2 * ge_signed_half_unique_second_masklookupvaluedecode + 1 /\ (ge_balance_positive_unique_second_masklookupvalue) = 0) /\ (ge_balance_negative_unique_second_masklookupvalue) = S ge_signed_half_unique_second_masklookupvaluedecode))) /\ ((dst_positive_unique_second_masklookup) + ge_balance_negative_unique_second_masklookupvalue = (dst_negative_unique_second_masklookup) + ge_balance_positive_unique_second_masklookupvalue))))))))) -> ((((~((dm_index_unique_second_mask)=0)) /\ (exists dm_quotient_unique_second_maskentry. (((n)=(dm_index_unique_second_mask)*dm_quotient_unique_second_maskentry) /\ (exists dst_positive_code_unique_second_maskentryinput dst_positive_scale_unique_second_maskentryinput dst_negative_code_unique_second_maskentryinput dst_negative_scale_unique_second_maskentryinput dst_positive_unique_second_maskentryinput dst_negative_unique_second_maskentryinput. (((F) = (((((dst_positive_code_unique_second_maskentryinput) + (dst_positive_scale_unique_second_maskentryinput)) * S ((dst_positive_code_unique_second_maskentryinput) + (dst_positive_scale_unique_second_maskentryinput)) + ((dst_positive_scale_unique_second_maskentryinput) + (dst_positive_scale_unique_second_maskentryinput))) + (((dst_negative_code_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)) * S ((dst_negative_code_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)) + ((dst_negative_scale_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)))) * S ((((dst_positive_code_unique_second_maskentryinput) + (dst_positive_scale_unique_second_maskentryinput)) * S ((dst_positive_code_unique_second_maskentryinput) + (dst_positive_scale_unique_second_maskentryinput)) + ((dst_positive_scale_unique_second_maskentryinput) + (dst_positive_scale_unique_second_maskentryinput))) + (((dst_negative_code_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)) * S ((dst_negative_code_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)) + ((dst_negative_scale_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)))) + ((((dst_negative_code_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)) * S ((dst_negative_code_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)) + ((dst_negative_scale_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput))) + (((dst_negative_code_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)) * S ((dst_negative_code_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)) + ((dst_negative_scale_unique_second_maskentryinput) + (dst_negative_scale_unique_second_maskentryinput)))))) /\ (((((exists ff_h_pvs_unique_second_maskentryinputpositive. ff_h_pvs_unique_second_maskentryinputpositive + S (dst_positive_unique_second_maskentryinput) = S ((S (dm_index_unique_second_mask)) * dst_positive_scale_unique_second_maskentryinput)) /\ exists ff_q_pvs_unique_second_maskentryinputpositive. dst_positive_code_unique_second_maskentryinput = ff_q_pvs_unique_second_maskentryinputpositive * S ((S (dm_index_unique_second_mask)) * dst_positive_scale_unique_second_maskentryinput) + (dst_positive_unique_second_maskentryinput))) /\ (((((exists ff_h_pvs_unique_second_maskentryinputnegative. ff_h_pvs_unique_second_maskentryinputnegative + S (dst_negative_unique_second_maskentryinput) = S ((S (dm_index_unique_second_mask)) * dst_negative_scale_unique_second_maskentryinput)) /\ exists ff_q_pvs_unique_second_maskentryinputnegative. dst_negative_code_unique_second_maskentryinput = ff_q_pvs_unique_second_maskentryinputnegative * S ((S (dm_index_unique_second_mask)) * dst_negative_scale_unique_second_maskentryinput) + (dst_negative_unique_second_maskentryinput))) /\ (exists ge_balance_positive_unique_second_maskentryinputvalue ge_balance_negative_unique_second_maskentryinputvalue. (((((dm_value_unique_second_mask) = 2 * (ge_balance_positive_unique_second_maskentryinputvalue) /\ (ge_balance_negative_unique_second_maskentryinputvalue) = 0) \/ exists ge_signed_half_unique_second_maskentryinputvaluedecode. (((dm_value_unique_second_mask) = 2 * ge_signed_half_unique_second_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_unique_second_maskentryinputvalue) = 0) /\ (ge_balance_negative_unique_second_maskentryinputvalue) = S ge_signed_half_unique_second_maskentryinputvaluedecode))) /\ ((dst_positive_unique_second_maskentryinput) + ge_balance_negative_unique_second_maskentryinputvalue = (dst_negative_unique_second_maskentryinput) + ge_balance_positive_unique_second_maskentryinputvalue))))))))))))) \/ ((((dm_index_unique_second_mask)=0 \/ ~(exists pvs_factor_unique_second_maskentrynondivisor. (n) = (dm_index_unique_second_mask) * pvs_factor_unique_second_maskentrynondivisor)) /\ ((dm_value_unique_second_mask)=0))))))) -> (forall dst_index_unique_mask_values dst_first_unique_mask_values dst_second_unique_mask_values. (exists pvs_gap_unique_mask_valuesbound. pvs_gap_unique_mask_valuesbound + S (dst_index_unique_mask_values) = (S l)) -> (exists dst_positive_code_unique_mask_valuesfirst dst_positive_scale_unique_mask_valuesfirst dst_negative_code_unique_mask_valuesfirst dst_negative_scale_unique_mask_valuesfirst dst_positive_unique_mask_valuesfirst dst_negative_unique_mask_valuesfirst. (((M) = (((((dst_positive_code_unique_mask_valuesfirst) + (dst_positive_scale_unique_mask_valuesfirst)) * S ((dst_positive_code_unique_mask_valuesfirst) + (dst_positive_scale_unique_mask_valuesfirst)) + ((dst_positive_scale_unique_mask_valuesfirst) + (dst_positive_scale_unique_mask_valuesfirst))) + (((dst_negative_code_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)) * S ((dst_negative_code_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)) + ((dst_negative_scale_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)))) * S ((((dst_positive_code_unique_mask_valuesfirst) + (dst_positive_scale_unique_mask_valuesfirst)) * S ((dst_positive_code_unique_mask_valuesfirst) + (dst_positive_scale_unique_mask_valuesfirst)) + ((dst_positive_scale_unique_mask_valuesfirst) + (dst_positive_scale_unique_mask_valuesfirst))) + (((dst_negative_code_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)) * S ((dst_negative_code_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)) + ((dst_negative_scale_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)))) + ((((dst_negative_code_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)) * S ((dst_negative_code_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)) + ((dst_negative_scale_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst))) + (((dst_negative_code_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)) * S ((dst_negative_code_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)) + ((dst_negative_scale_unique_mask_valuesfirst) + (dst_negative_scale_unique_mask_valuesfirst)))))) /\ (((((exists ff_h_pvs_unique_mask_valuesfirstpositive. ff_h_pvs_unique_mask_valuesfirstpositive + S (dst_positive_unique_mask_valuesfirst) = S ((S (dst_index_unique_mask_values)) * dst_positive_scale_unique_mask_valuesfirst)) /\ exists ff_q_pvs_unique_mask_valuesfirstpositive. dst_positive_code_unique_mask_valuesfirst = ff_q_pvs_unique_mask_valuesfirstpositive * S ((S (dst_index_unique_mask_values)) * dst_positive_scale_unique_mask_valuesfirst) + (dst_positive_unique_mask_valuesfirst))) /\ (((((exists ff_h_pvs_unique_mask_valuesfirstnegative. ff_h_pvs_unique_mask_valuesfirstnegative + S (dst_negative_unique_mask_valuesfirst) = S ((S (dst_index_unique_mask_values)) * dst_negative_scale_unique_mask_valuesfirst)) /\ exists ff_q_pvs_unique_mask_valuesfirstnegative. dst_negative_code_unique_mask_valuesfirst = ff_q_pvs_unique_mask_valuesfirstnegative * S ((S (dst_index_unique_mask_values)) * dst_negative_scale_unique_mask_valuesfirst) + (dst_negative_unique_mask_valuesfirst))) /\ (exists ge_balance_positive_unique_mask_valuesfirstvalue ge_balance_negative_unique_mask_valuesfirstvalue. (((((dst_first_unique_mask_values) = 2 * (ge_balance_positive_unique_mask_valuesfirstvalue) /\ (ge_balance_negative_unique_mask_valuesfirstvalue) = 0) \/ exists ge_signed_half_unique_mask_valuesfirstvaluedecode. (((dst_first_unique_mask_values) = 2 * ge_signed_half_unique_mask_valuesfirstvaluedecode + 1 /\ (ge_balance_positive_unique_mask_valuesfirstvalue) = 0) /\ (ge_balance_negative_unique_mask_valuesfirstvalue) = S ge_signed_half_unique_mask_valuesfirstvaluedecode))) /\ ((dst_positive_unique_mask_valuesfirst) + ge_balance_negative_unique_mask_valuesfirstvalue = (dst_negative_unique_mask_valuesfirst) + ge_balance_positive_unique_mask_valuesfirstvalue))))))))) -> (exists dst_positive_code_unique_mask_valuessecond dst_positive_scale_unique_mask_valuessecond dst_negative_code_unique_mask_valuessecond dst_negative_scale_unique_mask_valuessecond dst_positive_unique_mask_valuessecond dst_negative_unique_mask_valuessecond. (((K) = (((((dst_positive_code_unique_mask_valuessecond) + (dst_positive_scale_unique_mask_valuessecond)) * S ((dst_positive_code_unique_mask_valuessecond) + (dst_positive_scale_unique_mask_valuessecond)) + ((dst_positive_scale_unique_mask_valuessecond) + (dst_positive_scale_unique_mask_valuessecond))) + (((dst_negative_code_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)) * S ((dst_negative_code_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)) + ((dst_negative_scale_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)))) * S ((((dst_positive_code_unique_mask_valuessecond) + (dst_positive_scale_unique_mask_valuessecond)) * S ((dst_positive_code_unique_mask_valuessecond) + (dst_positive_scale_unique_mask_valuessecond)) + ((dst_positive_scale_unique_mask_valuessecond) + (dst_positive_scale_unique_mask_valuessecond))) + (((dst_negative_code_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)) * S ((dst_negative_code_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)) + ((dst_negative_scale_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)))) + ((((dst_negative_code_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)) * S ((dst_negative_code_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)) + ((dst_negative_scale_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond))) + (((dst_negative_code_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)) * S ((dst_negative_code_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)) + ((dst_negative_scale_unique_mask_valuessecond) + (dst_negative_scale_unique_mask_valuessecond)))))) /\ (((((exists ff_h_pvs_unique_mask_valuessecondpositive. ff_h_pvs_unique_mask_valuessecondpositive + S (dst_positive_unique_mask_valuessecond) = S ((S (dst_index_unique_mask_values)) * dst_positive_scale_unique_mask_valuessecond)) /\ exists ff_q_pvs_unique_mask_valuessecondpositive. dst_positive_code_unique_mask_valuessecond = ff_q_pvs_unique_mask_valuessecondpositive * S ((S (dst_index_unique_mask_values)) * dst_positive_scale_unique_mask_valuessecond) + (dst_positive_unique_mask_valuessecond))) /\ (((((exists ff_h_pvs_unique_mask_valuessecondnegative. ff_h_pvs_unique_mask_valuessecondnegative + S (dst_negative_unique_mask_valuessecond) = S ((S (dst_index_unique_mask_values)) * dst_negative_scale_unique_mask_valuessecond)) /\ exists ff_q_pvs_unique_mask_valuessecondnegative. dst_negative_code_unique_mask_valuessecond = ff_q_pvs_unique_mask_valuessecondnegative * S ((S (dst_index_unique_mask_values)) * dst_negative_scale_unique_mask_valuessecond) + (dst_negative_unique_mask_valuessecond))) /\ (exists ge_balance_positive_unique_mask_valuessecondvalue ge_balance_negative_unique_mask_valuessecondvalue. (((((dst_second_unique_mask_values) = 2 * (ge_balance_positive_unique_mask_valuessecondvalue) /\ (ge_balance_negative_unique_mask_valuessecondvalue) = 0) \/ exists ge_signed_half_unique_mask_valuessecondvaluedecode. (((dst_second_unique_mask_values) = 2 * ge_signed_half_unique_mask_valuessecondvaluedecode + 1 /\ (ge_balance_positive_unique_mask_valuessecondvalue) = 0) /\ (ge_balance_negative_unique_mask_valuessecondvalue) = S ge_signed_half_unique_mask_valuessecondvaluedecode))) /\ ((dst_positive_unique_mask_valuessecond) + ge_balance_negative_unique_mask_valuessecondvalue = (dst_negative_unique_mask_valuessecond) + ge_balance_positive_unique_mask_valuessecondvalue))))))))) -> dst_first_unique_mask_values = dst_second_unique_mask_values)