divisor_mask_positive_source_extensional

forall F G n M K. (forall dm_index_mask_source_equal dm_first_value_mask_source_equal dm_second_value_mask_source_equal. ~(dm_index_mask_source_equal=0) -> (exists pvs_le_gap_mask_source_equaldomain. pvs_le_gap_mask_source_equaldomain + (dm_index_mask_source_equal) = (n)) -> (exists dst_positive_code_mask_source_equalfirst dst_positive_scale_mask_source_equalfirst dst_negative_code_mask_source_equalfirst dst_negative_scale_mask_source_equalfirst dst_positive_mask_source_equalfirst dst_negative_mask_source_equalfirst. (((F) = (((((dst_positive_code_mask_source_equalfirst) + (dst_positive_scale_mask_source_equalfirst)) * S ((dst_positive_code_mask_source_equalfirst) + (dst_positive_scale_mask_source_equalfirst)) + ((dst_positive_scale_mask_source_equalfirst) + (dst_positive_scale_mask_source_equalfirst))) + (((dst_negative_code_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)) * S ((dst_negative_code_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)) + ((dst_negative_scale_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)))) * S ((((dst_positive_code_mask_source_equalfirst) + (dst_positive_scale_mask_source_equalfirst)) * S ((dst_positive_code_mask_source_equalfirst) + (dst_positive_scale_mask_source_equalfirst)) + ((dst_positive_scale_mask_source_equalfirst) + (dst_positive_scale_mask_source_equalfirst))) + (((dst_negative_code_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)) * S ((dst_negative_code_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)) + ((dst_negative_scale_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)))) + ((((dst_negative_code_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)) * S ((dst_negative_code_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)) + ((dst_negative_scale_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst))) + (((dst_negative_code_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)) * S ((dst_negative_code_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)) + ((dst_negative_scale_mask_source_equalfirst) + (dst_negative_scale_mask_source_equalfirst)))))) /\ (((((exists ff_h_pvs_mask_source_equalfirstpositive. ff_h_pvs_mask_source_equalfirstpositive + S (dst_positive_mask_source_equalfirst) = S ((S (dm_index_mask_source_equal)) * dst_positive_scale_mask_source_equalfirst)) /\ exists ff_q_pvs_mask_source_equalfirstpositive. dst_positive_code_mask_source_equalfirst = ff_q_pvs_mask_source_equalfirstpositive * S ((S (dm_index_mask_source_equal)) * dst_positive_scale_mask_source_equalfirst) + (dst_positive_mask_source_equalfirst))) /\ (((((exists ff_h_pvs_mask_source_equalfirstnegative. ff_h_pvs_mask_source_equalfirstnegative + S (dst_negative_mask_source_equalfirst) = S ((S (dm_index_mask_source_equal)) * dst_negative_scale_mask_source_equalfirst)) /\ exists ff_q_pvs_mask_source_equalfirstnegative. dst_negative_code_mask_source_equalfirst = ff_q_pvs_mask_source_equalfirstnegative * S ((S (dm_index_mask_source_equal)) * dst_negative_scale_mask_source_equalfirst) + (dst_negative_mask_source_equalfirst))) /\ (exists ge_balance_positive_mask_source_equalfirstvalue ge_balance_negative_mask_source_equalfirstvalue. (((((dm_first_value_mask_source_equal) = 2 * (ge_balance_positive_mask_source_equalfirstvalue) /\ (ge_balance_negative_mask_source_equalfirstvalue) = 0) \/ exists ge_signed_half_mask_source_equalfirstvaluedecode. (((dm_first_value_mask_source_equal) = 2 * ge_signed_half_mask_source_equalfirstvaluedecode + 1 /\ (ge_balance_positive_mask_source_equalfirstvalue) = 0) /\ (ge_balance_negative_mask_source_equalfirstvalue) = S ge_signed_half_mask_source_equalfirstvaluedecode))) /\ ((dst_positive_mask_source_equalfirst) + ge_balance_negative_mask_source_equalfirstvalue = (dst_negative_mask_source_equalfirst) + ge_balance_positive_mask_source_equalfirstvalue))))))))) -> (exists dst_positive_code_mask_source_equalsecond dst_positive_scale_mask_source_equalsecond dst_negative_code_mask_source_equalsecond dst_negative_scale_mask_source_equalsecond dst_positive_mask_source_equalsecond dst_negative_mask_source_equalsecond. (((G) = (((((dst_positive_code_mask_source_equalsecond) + (dst_positive_scale_mask_source_equalsecond)) * S ((dst_positive_code_mask_source_equalsecond) + (dst_positive_scale_mask_source_equalsecond)) + ((dst_positive_scale_mask_source_equalsecond) + (dst_positive_scale_mask_source_equalsecond))) + (((dst_negative_code_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)) * S ((dst_negative_code_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)) + ((dst_negative_scale_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)))) * S ((((dst_positive_code_mask_source_equalsecond) + (dst_positive_scale_mask_source_equalsecond)) * S ((dst_positive_code_mask_source_equalsecond) + (dst_positive_scale_mask_source_equalsecond)) + ((dst_positive_scale_mask_source_equalsecond) + (dst_positive_scale_mask_source_equalsecond))) + (((dst_negative_code_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)) * S ((dst_negative_code_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)) + ((dst_negative_scale_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)))) + ((((dst_negative_code_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)) * S ((dst_negative_code_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)) + ((dst_negative_scale_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond))) + (((dst_negative_code_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)) * S ((dst_negative_code_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)) + ((dst_negative_scale_mask_source_equalsecond) + (dst_negative_scale_mask_source_equalsecond)))))) /\ (((((exists ff_h_pvs_mask_source_equalsecondpositive. ff_h_pvs_mask_source_equalsecondpositive + S (dst_positive_mask_source_equalsecond) = S ((S (dm_index_mask_source_equal)) * dst_positive_scale_mask_source_equalsecond)) /\ exists ff_q_pvs_mask_source_equalsecondpositive. dst_positive_code_mask_source_equalsecond = ff_q_pvs_mask_source_equalsecondpositive * S ((S (dm_index_mask_source_equal)) * dst_positive_scale_mask_source_equalsecond) + (dst_positive_mask_source_equalsecond))) /\ (((((exists ff_h_pvs_mask_source_equalsecondnegative. ff_h_pvs_mask_source_equalsecondnegative + S (dst_negative_mask_source_equalsecond) = S ((S (dm_index_mask_source_equal)) * dst_negative_scale_mask_source_equalsecond)) /\ exists ff_q_pvs_mask_source_equalsecondnegative. dst_negative_code_mask_source_equalsecond = ff_q_pvs_mask_source_equalsecondnegative * S ((S (dm_index_mask_source_equal)) * dst_negative_scale_mask_source_equalsecond) + (dst_negative_mask_source_equalsecond))) /\ (exists ge_balance_positive_mask_source_equalsecondvalue ge_balance_negative_mask_source_equalsecondvalue. (((((dm_second_value_mask_source_equal) = 2 * (ge_balance_positive_mask_source_equalsecondvalue) /\ (ge_balance_negative_mask_source_equalsecondvalue) = 0) \/ exists ge_signed_half_mask_source_equalsecondvaluedecode. (((dm_second_value_mask_source_equal) = 2 * ge_signed_half_mask_source_equalsecondvaluedecode + 1 /\ (ge_balance_positive_mask_source_equalsecondvalue) = 0) /\ (ge_balance_negative_mask_source_equalsecondvalue) = S ge_signed_half_mask_source_equalsecondvaluedecode))) /\ ((dst_positive_mask_source_equalsecond) + ge_balance_negative_mask_source_equalsecondvalue = (dst_negative_mask_source_equalsecond) + ge_balance_positive_mask_source_equalsecondvalue))))))))) -> dm_first_value_mask_source_equal=dm_second_value_mask_source_equal) -> (((exists dst_positive_code_mask_source_firsttable dst_positive_scale_mask_source_firsttable dst_negative_code_mask_source_firsttable dst_negative_scale_mask_source_firsttable. (((M) = (((((dst_positive_code_mask_source_firsttable) + (dst_positive_scale_mask_source_firsttable)) * S ((dst_positive_code_mask_source_firsttable) + (dst_positive_scale_mask_source_firsttable)) + ((dst_positive_scale_mask_source_firsttable) + (dst_positive_scale_mask_source_firsttable))) + (((dst_negative_code_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)) * S ((dst_negative_code_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)) + ((dst_negative_scale_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)))) * S ((((dst_positive_code_mask_source_firsttable) + (dst_positive_scale_mask_source_firsttable)) * S ((dst_positive_code_mask_source_firsttable) + (dst_positive_scale_mask_source_firsttable)) + ((dst_positive_scale_mask_source_firsttable) + (dst_positive_scale_mask_source_firsttable))) + (((dst_negative_code_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)) * S ((dst_negative_code_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)) + ((dst_negative_scale_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)))) + ((((dst_negative_code_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)) * S ((dst_negative_code_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)) + ((dst_negative_scale_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable))) + (((dst_negative_code_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)) * S ((dst_negative_code_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)) + ((dst_negative_scale_mask_source_firsttable) + (dst_negative_scale_mask_source_firsttable)))))) /\ (forall dst_index_mask_source_firsttable. (exists pvs_le_gap_mask_source_firsttabledomain. pvs_le_gap_mask_source_firsttabledomain + (dst_index_mask_source_firsttable) = (n)) -> exists dst_positive_mask_source_firsttable dst_negative_mask_source_firsttable dst_value_mask_source_firsttable. ((((exists ff_h_pvs_mask_source_firsttableentrypositive. ff_h_pvs_mask_source_firsttableentrypositive + S (dst_positive_mask_source_firsttable) = S ((S (dst_index_mask_source_firsttable)) * dst_positive_scale_mask_source_firsttable)) /\ exists ff_q_pvs_mask_source_firsttableentrypositive. dst_positive_code_mask_source_firsttable = ff_q_pvs_mask_source_firsttableentrypositive * S ((S (dst_index_mask_source_firsttable)) * dst_positive_scale_mask_source_firsttable) + (dst_positive_mask_source_firsttable))) /\ (((((exists ff_h_pvs_mask_source_firsttableentrynegative. ff_h_pvs_mask_source_firsttableentrynegative + S (dst_negative_mask_source_firsttable) = S ((S (dst_index_mask_source_firsttable)) * dst_negative_scale_mask_source_firsttable)) /\ exists ff_q_pvs_mask_source_firsttableentrynegative. dst_negative_code_mask_source_firsttable = ff_q_pvs_mask_source_firsttableentrynegative * S ((S (dst_index_mask_source_firsttable)) * dst_negative_scale_mask_source_firsttable) + (dst_negative_mask_source_firsttable))) /\ (exists ge_balance_positive_mask_source_firsttableentryvalue ge_balance_negative_mask_source_firsttableentryvalue. (((((dst_value_mask_source_firsttable) = 2 * (ge_balance_positive_mask_source_firsttableentryvalue) /\ (ge_balance_negative_mask_source_firsttableentryvalue) = 0) \/ exists ge_signed_half_mask_source_firsttableentryvaluedecode. (((dst_value_mask_source_firsttable) = 2 * ge_signed_half_mask_source_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_mask_source_firsttableentryvalue) = 0) /\ (ge_balance_negative_mask_source_firsttableentryvalue) = S ge_signed_half_mask_source_firsttableentryvaluedecode))) /\ ((dst_positive_mask_source_firsttable) + ge_balance_negative_mask_source_firsttableentryvalue = (dst_negative_mask_source_firsttable) + ge_balance_positive_mask_source_firsttableentryvalue))))))))) /\ (forall dm_index_mask_source_first dm_value_mask_source_first. (exists pvs_le_gap_mask_source_firstdomain. pvs_le_gap_mask_source_firstdomain + (dm_index_mask_source_first) = (n)) -> (exists dst_positive_code_mask_source_firstlookup dst_positive_scale_mask_source_firstlookup dst_negative_code_mask_source_firstlookup dst_negative_scale_mask_source_firstlookup dst_positive_mask_source_firstlookup dst_negative_mask_source_firstlookup. (((M) = (((((dst_positive_code_mask_source_firstlookup) + (dst_positive_scale_mask_source_firstlookup)) * S ((dst_positive_code_mask_source_firstlookup) + (dst_positive_scale_mask_source_firstlookup)) + ((dst_positive_scale_mask_source_firstlookup) + (dst_positive_scale_mask_source_firstlookup))) + (((dst_negative_code_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)) * S ((dst_negative_code_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)) + ((dst_negative_scale_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)))) * S ((((dst_positive_code_mask_source_firstlookup) + (dst_positive_scale_mask_source_firstlookup)) * S ((dst_positive_code_mask_source_firstlookup) + (dst_positive_scale_mask_source_firstlookup)) + ((dst_positive_scale_mask_source_firstlookup) + (dst_positive_scale_mask_source_firstlookup))) + (((dst_negative_code_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)) * S ((dst_negative_code_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)) + ((dst_negative_scale_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)))) + ((((dst_negative_code_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)) * S ((dst_negative_code_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)) + ((dst_negative_scale_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup))) + (((dst_negative_code_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)) * S ((dst_negative_code_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)) + ((dst_negative_scale_mask_source_firstlookup) + (dst_negative_scale_mask_source_firstlookup)))))) /\ (((((exists ff_h_pvs_mask_source_firstlookuppositive. ff_h_pvs_mask_source_firstlookuppositive + S (dst_positive_mask_source_firstlookup) = S ((S (dm_index_mask_source_first)) * dst_positive_scale_mask_source_firstlookup)) /\ exists ff_q_pvs_mask_source_firstlookuppositive. dst_positive_code_mask_source_firstlookup = ff_q_pvs_mask_source_firstlookuppositive * S ((S (dm_index_mask_source_first)) * dst_positive_scale_mask_source_firstlookup) + (dst_positive_mask_source_firstlookup))) /\ (((((exists ff_h_pvs_mask_source_firstlookupnegative. ff_h_pvs_mask_source_firstlookupnegative + S (dst_negative_mask_source_firstlookup) = S ((S (dm_index_mask_source_first)) * dst_negative_scale_mask_source_firstlookup)) /\ exists ff_q_pvs_mask_source_firstlookupnegative. dst_negative_code_mask_source_firstlookup = ff_q_pvs_mask_source_firstlookupnegative * S ((S (dm_index_mask_source_first)) * dst_negative_scale_mask_source_firstlookup) + (dst_negative_mask_source_firstlookup))) /\ (exists ge_balance_positive_mask_source_firstlookupvalue ge_balance_negative_mask_source_firstlookupvalue. (((((dm_value_mask_source_first) = 2 * (ge_balance_positive_mask_source_firstlookupvalue) /\ (ge_balance_negative_mask_source_firstlookupvalue) = 0) \/ exists ge_signed_half_mask_source_firstlookupvaluedecode. (((dm_value_mask_source_first) = 2 * ge_signed_half_mask_source_firstlookupvaluedecode + 1 /\ (ge_balance_positive_mask_source_firstlookupvalue) = 0) /\ (ge_balance_negative_mask_source_firstlookupvalue) = S ge_signed_half_mask_source_firstlookupvaluedecode))) /\ ((dst_positive_mask_source_firstlookup) + ge_balance_negative_mask_source_firstlookupvalue = (dst_negative_mask_source_firstlookup) + ge_balance_positive_mask_source_firstlookupvalue))))))))) -> ((((~((dm_index_mask_source_first)=0)) /\ (exists dm_quotient_mask_source_firstentry. (((n)=(dm_index_mask_source_first)*dm_quotient_mask_source_firstentry) /\ (exists dst_positive_code_mask_source_firstentryinput dst_positive_scale_mask_source_firstentryinput dst_negative_code_mask_source_firstentryinput dst_negative_scale_mask_source_firstentryinput dst_positive_mask_source_firstentryinput dst_negative_mask_source_firstentryinput. (((F) = (((((dst_positive_code_mask_source_firstentryinput) + (dst_positive_scale_mask_source_firstentryinput)) * S ((dst_positive_code_mask_source_firstentryinput) + (dst_positive_scale_mask_source_firstentryinput)) + ((dst_positive_scale_mask_source_firstentryinput) + (dst_positive_scale_mask_source_firstentryinput))) + (((dst_negative_code_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)) * S ((dst_negative_code_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)) + ((dst_negative_scale_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)))) * S ((((dst_positive_code_mask_source_firstentryinput) + (dst_positive_scale_mask_source_firstentryinput)) * S ((dst_positive_code_mask_source_firstentryinput) + (dst_positive_scale_mask_source_firstentryinput)) + ((dst_positive_scale_mask_source_firstentryinput) + (dst_positive_scale_mask_source_firstentryinput))) + (((dst_negative_code_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)) * S ((dst_negative_code_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)) + ((dst_negative_scale_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)))) + ((((dst_negative_code_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)) * S ((dst_negative_code_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)) + ((dst_negative_scale_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput))) + (((dst_negative_code_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)) * S ((dst_negative_code_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)) + ((dst_negative_scale_mask_source_firstentryinput) + (dst_negative_scale_mask_source_firstentryinput)))))) /\ (((((exists ff_h_pvs_mask_source_firstentryinputpositive. ff_h_pvs_mask_source_firstentryinputpositive + S (dst_positive_mask_source_firstentryinput) = S ((S (dm_index_mask_source_first)) * dst_positive_scale_mask_source_firstentryinput)) /\ exists ff_q_pvs_mask_source_firstentryinputpositive. dst_positive_code_mask_source_firstentryinput = ff_q_pvs_mask_source_firstentryinputpositive * S ((S (dm_index_mask_source_first)) * dst_positive_scale_mask_source_firstentryinput) + (dst_positive_mask_source_firstentryinput))) /\ (((((exists ff_h_pvs_mask_source_firstentryinputnegative. ff_h_pvs_mask_source_firstentryinputnegative + S (dst_negative_mask_source_firstentryinput) = S ((S (dm_index_mask_source_first)) * dst_negative_scale_mask_source_firstentryinput)) /\ exists ff_q_pvs_mask_source_firstentryinputnegative. dst_negative_code_mask_source_firstentryinput = ff_q_pvs_mask_source_firstentryinputnegative * S ((S (dm_index_mask_source_first)) * dst_negative_scale_mask_source_firstentryinput) + (dst_negative_mask_source_firstentryinput))) /\ (exists ge_balance_positive_mask_source_firstentryinputvalue ge_balance_negative_mask_source_firstentryinputvalue. (((((dm_value_mask_source_first) = 2 * (ge_balance_positive_mask_source_firstentryinputvalue) /\ (ge_balance_negative_mask_source_firstentryinputvalue) = 0) \/ exists ge_signed_half_mask_source_firstentryinputvaluedecode. (((dm_value_mask_source_first) = 2 * ge_signed_half_mask_source_firstentryinputvaluedecode + 1 /\ (ge_balance_positive_mask_source_firstentryinputvalue) = 0) /\ (ge_balance_negative_mask_source_firstentryinputvalue) = S ge_signed_half_mask_source_firstentryinputvaluedecode))) /\ ((dst_positive_mask_source_firstentryinput) + ge_balance_negative_mask_source_firstentryinputvalue = (dst_negative_mask_source_firstentryinput) + ge_balance_positive_mask_source_firstentryinputvalue))))))))))))) \/ ((((dm_index_mask_source_first)=0 \/ ~(exists pvs_factor_mask_source_firstentrynondivisor. (n) = (dm_index_mask_source_first) * pvs_factor_mask_source_firstentrynondivisor)) /\ ((dm_value_mask_source_first)=0))))))) -> (((exists dst_positive_code_mask_source_secondtable dst_positive_scale_mask_source_secondtable dst_negative_code_mask_source_secondtable dst_negative_scale_mask_source_secondtable. (((K) = (((((dst_positive_code_mask_source_secondtable) + (dst_positive_scale_mask_source_secondtable)) * S ((dst_positive_code_mask_source_secondtable) + (dst_positive_scale_mask_source_secondtable)) + ((dst_positive_scale_mask_source_secondtable) + (dst_positive_scale_mask_source_secondtable))) + (((dst_negative_code_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)) * S ((dst_negative_code_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)) + ((dst_negative_scale_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)))) * S ((((dst_positive_code_mask_source_secondtable) + (dst_positive_scale_mask_source_secondtable)) * S ((dst_positive_code_mask_source_secondtable) + (dst_positive_scale_mask_source_secondtable)) + ((dst_positive_scale_mask_source_secondtable) + (dst_positive_scale_mask_source_secondtable))) + (((dst_negative_code_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)) * S ((dst_negative_code_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)) + ((dst_negative_scale_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)))) + ((((dst_negative_code_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)) * S ((dst_negative_code_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)) + ((dst_negative_scale_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable))) + (((dst_negative_code_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)) * S ((dst_negative_code_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)) + ((dst_negative_scale_mask_source_secondtable) + (dst_negative_scale_mask_source_secondtable)))))) /\ (forall dst_index_mask_source_secondtable. (exists pvs_le_gap_mask_source_secondtabledomain. pvs_le_gap_mask_source_secondtabledomain + (dst_index_mask_source_secondtable) = (n)) -> exists dst_positive_mask_source_secondtable dst_negative_mask_source_secondtable dst_value_mask_source_secondtable. ((((exists ff_h_pvs_mask_source_secondtableentrypositive. ff_h_pvs_mask_source_secondtableentrypositive + S (dst_positive_mask_source_secondtable) = S ((S (dst_index_mask_source_secondtable)) * dst_positive_scale_mask_source_secondtable)) /\ exists ff_q_pvs_mask_source_secondtableentrypositive. dst_positive_code_mask_source_secondtable = ff_q_pvs_mask_source_secondtableentrypositive * S ((S (dst_index_mask_source_secondtable)) * dst_positive_scale_mask_source_secondtable) + (dst_positive_mask_source_secondtable))) /\ (((((exists ff_h_pvs_mask_source_secondtableentrynegative. ff_h_pvs_mask_source_secondtableentrynegative + S (dst_negative_mask_source_secondtable) = S ((S (dst_index_mask_source_secondtable)) * dst_negative_scale_mask_source_secondtable)) /\ exists ff_q_pvs_mask_source_secondtableentrynegative. dst_negative_code_mask_source_secondtable = ff_q_pvs_mask_source_secondtableentrynegative * S ((S (dst_index_mask_source_secondtable)) * dst_negative_scale_mask_source_secondtable) + (dst_negative_mask_source_secondtable))) /\ (exists ge_balance_positive_mask_source_secondtableentryvalue ge_balance_negative_mask_source_secondtableentryvalue. (((((dst_value_mask_source_secondtable) = 2 * (ge_balance_positive_mask_source_secondtableentryvalue) /\ (ge_balance_negative_mask_source_secondtableentryvalue) = 0) \/ exists ge_signed_half_mask_source_secondtableentryvaluedecode. (((dst_value_mask_source_secondtable) = 2 * ge_signed_half_mask_source_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_mask_source_secondtableentryvalue) = 0) /\ (ge_balance_negative_mask_source_secondtableentryvalue) = S ge_signed_half_mask_source_secondtableentryvaluedecode))) /\ ((dst_positive_mask_source_secondtable) + ge_balance_negative_mask_source_secondtableentryvalue = (dst_negative_mask_source_secondtable) + ge_balance_positive_mask_source_secondtableentryvalue))))))))) /\ (forall dm_index_mask_source_second dm_value_mask_source_second. (exists pvs_le_gap_mask_source_seconddomain. pvs_le_gap_mask_source_seconddomain + (dm_index_mask_source_second) = (n)) -> (exists dst_positive_code_mask_source_secondlookup dst_positive_scale_mask_source_secondlookup dst_negative_code_mask_source_secondlookup dst_negative_scale_mask_source_secondlookup dst_positive_mask_source_secondlookup dst_negative_mask_source_secondlookup. (((K) = (((((dst_positive_code_mask_source_secondlookup) + (dst_positive_scale_mask_source_secondlookup)) * S ((dst_positive_code_mask_source_secondlookup) + (dst_positive_scale_mask_source_secondlookup)) + ((dst_positive_scale_mask_source_secondlookup) + (dst_positive_scale_mask_source_secondlookup))) + (((dst_negative_code_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)) * S ((dst_negative_code_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)) + ((dst_negative_scale_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)))) * S ((((dst_positive_code_mask_source_secondlookup) + (dst_positive_scale_mask_source_secondlookup)) * S ((dst_positive_code_mask_source_secondlookup) + (dst_positive_scale_mask_source_secondlookup)) + ((dst_positive_scale_mask_source_secondlookup) + (dst_positive_scale_mask_source_secondlookup))) + (((dst_negative_code_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)) * S ((dst_negative_code_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)) + ((dst_negative_scale_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)))) + ((((dst_negative_code_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)) * S ((dst_negative_code_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)) + ((dst_negative_scale_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup))) + (((dst_negative_code_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)) * S ((dst_negative_code_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)) + ((dst_negative_scale_mask_source_secondlookup) + (dst_negative_scale_mask_source_secondlookup)))))) /\ (((((exists ff_h_pvs_mask_source_secondlookuppositive. ff_h_pvs_mask_source_secondlookuppositive + S (dst_positive_mask_source_secondlookup) = S ((S (dm_index_mask_source_second)) * dst_positive_scale_mask_source_secondlookup)) /\ exists ff_q_pvs_mask_source_secondlookuppositive. dst_positive_code_mask_source_secondlookup = ff_q_pvs_mask_source_secondlookuppositive * S ((S (dm_index_mask_source_second)) * dst_positive_scale_mask_source_secondlookup) + (dst_positive_mask_source_secondlookup))) /\ (((((exists ff_h_pvs_mask_source_secondlookupnegative. ff_h_pvs_mask_source_secondlookupnegative + S (dst_negative_mask_source_secondlookup) = S ((S (dm_index_mask_source_second)) * dst_negative_scale_mask_source_secondlookup)) /\ exists ff_q_pvs_mask_source_secondlookupnegative. dst_negative_code_mask_source_secondlookup = ff_q_pvs_mask_source_secondlookupnegative * S ((S (dm_index_mask_source_second)) * dst_negative_scale_mask_source_secondlookup) + (dst_negative_mask_source_secondlookup))) /\ (exists ge_balance_positive_mask_source_secondlookupvalue ge_balance_negative_mask_source_secondlookupvalue. (((((dm_value_mask_source_second) = 2 * (ge_balance_positive_mask_source_secondlookupvalue) /\ (ge_balance_negative_mask_source_secondlookupvalue) = 0) \/ exists ge_signed_half_mask_source_secondlookupvaluedecode. (((dm_value_mask_source_second) = 2 * ge_signed_half_mask_source_secondlookupvaluedecode + 1 /\ (ge_balance_positive_mask_source_secondlookupvalue) = 0) /\ (ge_balance_negative_mask_source_secondlookupvalue) = S ge_signed_half_mask_source_secondlookupvaluedecode))) /\ ((dst_positive_mask_source_secondlookup) + ge_balance_negative_mask_source_secondlookupvalue = (dst_negative_mask_source_secondlookup) + ge_balance_positive_mask_source_secondlookupvalue))))))))) -> ((((~((dm_index_mask_source_second)=0)) /\ (exists dm_quotient_mask_source_secondentry. (((n)=(dm_index_mask_source_second)*dm_quotient_mask_source_secondentry) /\ (exists dst_positive_code_mask_source_secondentryinput dst_positive_scale_mask_source_secondentryinput dst_negative_code_mask_source_secondentryinput dst_negative_scale_mask_source_secondentryinput dst_positive_mask_source_secondentryinput dst_negative_mask_source_secondentryinput. (((G) = (((((dst_positive_code_mask_source_secondentryinput) + (dst_positive_scale_mask_source_secondentryinput)) * S ((dst_positive_code_mask_source_secondentryinput) + (dst_positive_scale_mask_source_secondentryinput)) + ((dst_positive_scale_mask_source_secondentryinput) + (dst_positive_scale_mask_source_secondentryinput))) + (((dst_negative_code_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)) * S ((dst_negative_code_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)) + ((dst_negative_scale_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)))) * S ((((dst_positive_code_mask_source_secondentryinput) + (dst_positive_scale_mask_source_secondentryinput)) * S ((dst_positive_code_mask_source_secondentryinput) + (dst_positive_scale_mask_source_secondentryinput)) + ((dst_positive_scale_mask_source_secondentryinput) + (dst_positive_scale_mask_source_secondentryinput))) + (((dst_negative_code_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)) * S ((dst_negative_code_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)) + ((dst_negative_scale_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)))) + ((((dst_negative_code_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)) * S ((dst_negative_code_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)) + ((dst_negative_scale_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput))) + (((dst_negative_code_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)) * S ((dst_negative_code_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)) + ((dst_negative_scale_mask_source_secondentryinput) + (dst_negative_scale_mask_source_secondentryinput)))))) /\ (((((exists ff_h_pvs_mask_source_secondentryinputpositive. ff_h_pvs_mask_source_secondentryinputpositive + S (dst_positive_mask_source_secondentryinput) = S ((S (dm_index_mask_source_second)) * dst_positive_scale_mask_source_secondentryinput)) /\ exists ff_q_pvs_mask_source_secondentryinputpositive. dst_positive_code_mask_source_secondentryinput = ff_q_pvs_mask_source_secondentryinputpositive * S ((S (dm_index_mask_source_second)) * dst_positive_scale_mask_source_secondentryinput) + (dst_positive_mask_source_secondentryinput))) /\ (((((exists ff_h_pvs_mask_source_secondentryinputnegative. ff_h_pvs_mask_source_secondentryinputnegative + S (dst_negative_mask_source_secondentryinput) = S ((S (dm_index_mask_source_second)) * dst_negative_scale_mask_source_secondentryinput)) /\ exists ff_q_pvs_mask_source_secondentryinputnegative. dst_negative_code_mask_source_secondentryinput = ff_q_pvs_mask_source_secondentryinputnegative * S ((S (dm_index_mask_source_second)) * dst_negative_scale_mask_source_secondentryinput) + (dst_negative_mask_source_secondentryinput))) /\ (exists ge_balance_positive_mask_source_secondentryinputvalue ge_balance_negative_mask_source_secondentryinputvalue. (((((dm_value_mask_source_second) = 2 * (ge_balance_positive_mask_source_secondentryinputvalue) /\ (ge_balance_negative_mask_source_secondentryinputvalue) = 0) \/ exists ge_signed_half_mask_source_secondentryinputvaluedecode. (((dm_value_mask_source_second) = 2 * ge_signed_half_mask_source_secondentryinputvaluedecode + 1 /\ (ge_balance_positive_mask_source_secondentryinputvalue) = 0) /\ (ge_balance_negative_mask_source_secondentryinputvalue) = S ge_signed_half_mask_source_secondentryinputvaluedecode))) /\ ((dst_positive_mask_source_secondentryinput) + ge_balance_negative_mask_source_secondentryinputvalue = (dst_negative_mask_source_secondentryinput) + ge_balance_positive_mask_source_secondentryinputvalue))))))))))))) \/ ((((dm_index_mask_source_second)=0 \/ ~(exists pvs_factor_mask_source_secondentrynondivisor. (n) = (dm_index_mask_source_second) * pvs_factor_mask_source_secondentrynondivisor)) /\ ((dm_value_mask_source_second)=0))))))) -> (forall dst_index_mask_source_result dst_first_mask_source_result dst_second_mask_source_result. (exists pvs_gap_mask_source_resultbound. pvs_gap_mask_source_resultbound + S (dst_index_mask_source_result) = (S n)) -> (exists dst_positive_code_mask_source_resultfirst dst_positive_scale_mask_source_resultfirst dst_negative_code_mask_source_resultfirst dst_negative_scale_mask_source_resultfirst dst_positive_mask_source_resultfirst dst_negative_mask_source_resultfirst. (((M) = (((((dst_positive_code_mask_source_resultfirst) + (dst_positive_scale_mask_source_resultfirst)) * S ((dst_positive_code_mask_source_resultfirst) + (dst_positive_scale_mask_source_resultfirst)) + ((dst_positive_scale_mask_source_resultfirst) + (dst_positive_scale_mask_source_resultfirst))) + (((dst_negative_code_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)) * S ((dst_negative_code_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)) + ((dst_negative_scale_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)))) * S ((((dst_positive_code_mask_source_resultfirst) + (dst_positive_scale_mask_source_resultfirst)) * S ((dst_positive_code_mask_source_resultfirst) + (dst_positive_scale_mask_source_resultfirst)) + ((dst_positive_scale_mask_source_resultfirst) + (dst_positive_scale_mask_source_resultfirst))) + (((dst_negative_code_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)) * S ((dst_negative_code_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)) + ((dst_negative_scale_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)))) + ((((dst_negative_code_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)) * S ((dst_negative_code_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)) + ((dst_negative_scale_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst))) + (((dst_negative_code_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)) * S ((dst_negative_code_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)) + ((dst_negative_scale_mask_source_resultfirst) + (dst_negative_scale_mask_source_resultfirst)))))) /\ (((((exists ff_h_pvs_mask_source_resultfirstpositive. ff_h_pvs_mask_source_resultfirstpositive + S (dst_positive_mask_source_resultfirst) = S ((S (dst_index_mask_source_result)) * dst_positive_scale_mask_source_resultfirst)) /\ exists ff_q_pvs_mask_source_resultfirstpositive. dst_positive_code_mask_source_resultfirst = ff_q_pvs_mask_source_resultfirstpositive * S ((S (dst_index_mask_source_result)) * dst_positive_scale_mask_source_resultfirst) + (dst_positive_mask_source_resultfirst))) /\ (((((exists ff_h_pvs_mask_source_resultfirstnegative. ff_h_pvs_mask_source_resultfirstnegative + S (dst_negative_mask_source_resultfirst) = S ((S (dst_index_mask_source_result)) * dst_negative_scale_mask_source_resultfirst)) /\ exists ff_q_pvs_mask_source_resultfirstnegative. dst_negative_code_mask_source_resultfirst = ff_q_pvs_mask_source_resultfirstnegative * S ((S (dst_index_mask_source_result)) * dst_negative_scale_mask_source_resultfirst) + (dst_negative_mask_source_resultfirst))) /\ (exists ge_balance_positive_mask_source_resultfirstvalue ge_balance_negative_mask_source_resultfirstvalue. (((((dst_first_mask_source_result) = 2 * (ge_balance_positive_mask_source_resultfirstvalue) /\ (ge_balance_negative_mask_source_resultfirstvalue) = 0) \/ exists ge_signed_half_mask_source_resultfirstvaluedecode. (((dst_first_mask_source_result) = 2 * ge_signed_half_mask_source_resultfirstvaluedecode + 1 /\ (ge_balance_positive_mask_source_resultfirstvalue) = 0) /\ (ge_balance_negative_mask_source_resultfirstvalue) = S ge_signed_half_mask_source_resultfirstvaluedecode))) /\ ((dst_positive_mask_source_resultfirst) + ge_balance_negative_mask_source_resultfirstvalue = (dst_negative_mask_source_resultfirst) + ge_balance_positive_mask_source_resultfirstvalue))))))))) -> (exists dst_positive_code_mask_source_resultsecond dst_positive_scale_mask_source_resultsecond dst_negative_code_mask_source_resultsecond dst_negative_scale_mask_source_resultsecond dst_positive_mask_source_resultsecond dst_negative_mask_source_resultsecond. (((K) = (((((dst_positive_code_mask_source_resultsecond) + (dst_positive_scale_mask_source_resultsecond)) * S ((dst_positive_code_mask_source_resultsecond) + (dst_positive_scale_mask_source_resultsecond)) + ((dst_positive_scale_mask_source_resultsecond) + (dst_positive_scale_mask_source_resultsecond))) + (((dst_negative_code_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)) * S ((dst_negative_code_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)) + ((dst_negative_scale_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)))) * S ((((dst_positive_code_mask_source_resultsecond) + (dst_positive_scale_mask_source_resultsecond)) * S ((dst_positive_code_mask_source_resultsecond) + (dst_positive_scale_mask_source_resultsecond)) + ((dst_positive_scale_mask_source_resultsecond) + (dst_positive_scale_mask_source_resultsecond))) + (((dst_negative_code_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)) * S ((dst_negative_code_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)) + ((dst_negative_scale_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)))) + ((((dst_negative_code_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)) * S ((dst_negative_code_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)) + ((dst_negative_scale_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond))) + (((dst_negative_code_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)) * S ((dst_negative_code_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)) + ((dst_negative_scale_mask_source_resultsecond) + (dst_negative_scale_mask_source_resultsecond)))))) /\ (((((exists ff_h_pvs_mask_source_resultsecondpositive. ff_h_pvs_mask_source_resultsecondpositive + S (dst_positive_mask_source_resultsecond) = S ((S (dst_index_mask_source_result)) * dst_positive_scale_mask_source_resultsecond)) /\ exists ff_q_pvs_mask_source_resultsecondpositive. dst_positive_code_mask_source_resultsecond = ff_q_pvs_mask_source_resultsecondpositive * S ((S (dst_index_mask_source_result)) * dst_positive_scale_mask_source_resultsecond) + (dst_positive_mask_source_resultsecond))) /\ (((((exists ff_h_pvs_mask_source_resultsecondnegative. ff_h_pvs_mask_source_resultsecondnegative + S (dst_negative_mask_source_resultsecond) = S ((S (dst_index_mask_source_result)) * dst_negative_scale_mask_source_resultsecond)) /\ exists ff_q_pvs_mask_source_resultsecondnegative. dst_negative_code_mask_source_resultsecond = ff_q_pvs_mask_source_resultsecondnegative * S ((S (dst_index_mask_source_result)) * dst_negative_scale_mask_source_resultsecond) + (dst_negative_mask_source_resultsecond))) /\ (exists ge_balance_positive_mask_source_resultsecondvalue ge_balance_negative_mask_source_resultsecondvalue. (((((dst_second_mask_source_result) = 2 * (ge_balance_positive_mask_source_resultsecondvalue) /\ (ge_balance_negative_mask_source_resultsecondvalue) = 0) \/ exists ge_signed_half_mask_source_resultsecondvaluedecode. (((dst_second_mask_source_result) = 2 * ge_signed_half_mask_source_resultsecondvaluedecode + 1 /\ (ge_balance_positive_mask_source_resultsecondvalue) = 0) /\ (ge_balance_negative_mask_source_resultsecondvalue) = S ge_signed_half_mask_source_resultsecondvaluedecode))) /\ ((dst_positive_mask_source_resultsecond) + ge_balance_negative_mask_source_resultsecondvalue = (dst_negative_mask_source_resultsecond) + ge_balance_positive_mask_source_resultsecondvalue))))))))) -> dst_first_mask_source_result = dst_second_mask_source_result)