dirichlet_convolution_prefix_positive_source_extensional

forall F G H K n M P. ~(n=0) -> (forall dm_index_prefix_source_left dm_first_value_prefix_source_left dm_second_value_prefix_source_left. ~(dm_index_prefix_source_left=0) -> (exists pvs_le_gap_prefix_source_leftdomain. pvs_le_gap_prefix_source_leftdomain + (dm_index_prefix_source_left) = (n)) -> (exists dst_positive_code_prefix_source_leftfirst dst_positive_scale_prefix_source_leftfirst dst_negative_code_prefix_source_leftfirst dst_negative_scale_prefix_source_leftfirst dst_positive_prefix_source_leftfirst dst_negative_prefix_source_leftfirst. (((F) = (((((dst_positive_code_prefix_source_leftfirst) + (dst_positive_scale_prefix_source_leftfirst)) * S ((dst_positive_code_prefix_source_leftfirst) + (dst_positive_scale_prefix_source_leftfirst)) + ((dst_positive_scale_prefix_source_leftfirst) + (dst_positive_scale_prefix_source_leftfirst))) + (((dst_negative_code_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)) * S ((dst_negative_code_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)) + ((dst_negative_scale_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)))) * S ((((dst_positive_code_prefix_source_leftfirst) + (dst_positive_scale_prefix_source_leftfirst)) * S ((dst_positive_code_prefix_source_leftfirst) + (dst_positive_scale_prefix_source_leftfirst)) + ((dst_positive_scale_prefix_source_leftfirst) + (dst_positive_scale_prefix_source_leftfirst))) + (((dst_negative_code_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)) * S ((dst_negative_code_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)) + ((dst_negative_scale_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)))) + ((((dst_negative_code_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)) * S ((dst_negative_code_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)) + ((dst_negative_scale_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst))) + (((dst_negative_code_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)) * S ((dst_negative_code_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)) + ((dst_negative_scale_prefix_source_leftfirst) + (dst_negative_scale_prefix_source_leftfirst)))))) /\ (((((exists ff_h_pvs_prefix_source_leftfirstpositive. ff_h_pvs_prefix_source_leftfirstpositive + S (dst_positive_prefix_source_leftfirst) = S ((S (dm_index_prefix_source_left)) * dst_positive_scale_prefix_source_leftfirst)) /\ exists ff_q_pvs_prefix_source_leftfirstpositive. dst_positive_code_prefix_source_leftfirst = ff_q_pvs_prefix_source_leftfirstpositive * S ((S (dm_index_prefix_source_left)) * dst_positive_scale_prefix_source_leftfirst) + (dst_positive_prefix_source_leftfirst))) /\ (((((exists ff_h_pvs_prefix_source_leftfirstnegative. ff_h_pvs_prefix_source_leftfirstnegative + S (dst_negative_prefix_source_leftfirst) = S ((S (dm_index_prefix_source_left)) * dst_negative_scale_prefix_source_leftfirst)) /\ exists ff_q_pvs_prefix_source_leftfirstnegative. dst_negative_code_prefix_source_leftfirst = ff_q_pvs_prefix_source_leftfirstnegative * S ((S (dm_index_prefix_source_left)) * dst_negative_scale_prefix_source_leftfirst) + (dst_negative_prefix_source_leftfirst))) /\ (exists ge_balance_positive_prefix_source_leftfirstvalue ge_balance_negative_prefix_source_leftfirstvalue. (((((dm_first_value_prefix_source_left) = 2 * (ge_balance_positive_prefix_source_leftfirstvalue) /\ (ge_balance_negative_prefix_source_leftfirstvalue) = 0) \/ exists ge_signed_half_prefix_source_leftfirstvaluedecode. (((dm_first_value_prefix_source_left) = 2 * ge_signed_half_prefix_source_leftfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_source_leftfirstvalue) = 0) /\ (ge_balance_negative_prefix_source_leftfirstvalue) = S ge_signed_half_prefix_source_leftfirstvaluedecode))) /\ ((dst_positive_prefix_source_leftfirst) + ge_balance_negative_prefix_source_leftfirstvalue = (dst_negative_prefix_source_leftfirst) + ge_balance_positive_prefix_source_leftfirstvalue))))))))) -> (exists dst_positive_code_prefix_source_leftsecond dst_positive_scale_prefix_source_leftsecond dst_negative_code_prefix_source_leftsecond dst_negative_scale_prefix_source_leftsecond dst_positive_prefix_source_leftsecond dst_negative_prefix_source_leftsecond. (((H) = (((((dst_positive_code_prefix_source_leftsecond) + (dst_positive_scale_prefix_source_leftsecond)) * S ((dst_positive_code_prefix_source_leftsecond) + (dst_positive_scale_prefix_source_leftsecond)) + ((dst_positive_scale_prefix_source_leftsecond) + (dst_positive_scale_prefix_source_leftsecond))) + (((dst_negative_code_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)) * S ((dst_negative_code_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)) + ((dst_negative_scale_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)))) * S ((((dst_positive_code_prefix_source_leftsecond) + (dst_positive_scale_prefix_source_leftsecond)) * S ((dst_positive_code_prefix_source_leftsecond) + (dst_positive_scale_prefix_source_leftsecond)) + ((dst_positive_scale_prefix_source_leftsecond) + (dst_positive_scale_prefix_source_leftsecond))) + (((dst_negative_code_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)) * S ((dst_negative_code_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)) + ((dst_negative_scale_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)))) + ((((dst_negative_code_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)) * S ((dst_negative_code_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)) + ((dst_negative_scale_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond))) + (((dst_negative_code_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)) * S ((dst_negative_code_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)) + ((dst_negative_scale_prefix_source_leftsecond) + (dst_negative_scale_prefix_source_leftsecond)))))) /\ (((((exists ff_h_pvs_prefix_source_leftsecondpositive. ff_h_pvs_prefix_source_leftsecondpositive + S (dst_positive_prefix_source_leftsecond) = S ((S (dm_index_prefix_source_left)) * dst_positive_scale_prefix_source_leftsecond)) /\ exists ff_q_pvs_prefix_source_leftsecondpositive. dst_positive_code_prefix_source_leftsecond = ff_q_pvs_prefix_source_leftsecondpositive * S ((S (dm_index_prefix_source_left)) * dst_positive_scale_prefix_source_leftsecond) + (dst_positive_prefix_source_leftsecond))) /\ (((((exists ff_h_pvs_prefix_source_leftsecondnegative. ff_h_pvs_prefix_source_leftsecondnegative + S (dst_negative_prefix_source_leftsecond) = S ((S (dm_index_prefix_source_left)) * dst_negative_scale_prefix_source_leftsecond)) /\ exists ff_q_pvs_prefix_source_leftsecondnegative. dst_negative_code_prefix_source_leftsecond = ff_q_pvs_prefix_source_leftsecondnegative * S ((S (dm_index_prefix_source_left)) * dst_negative_scale_prefix_source_leftsecond) + (dst_negative_prefix_source_leftsecond))) /\ (exists ge_balance_positive_prefix_source_leftsecondvalue ge_balance_negative_prefix_source_leftsecondvalue. (((((dm_second_value_prefix_source_left) = 2 * (ge_balance_positive_prefix_source_leftsecondvalue) /\ (ge_balance_negative_prefix_source_leftsecondvalue) = 0) \/ exists ge_signed_half_prefix_source_leftsecondvaluedecode. (((dm_second_value_prefix_source_left) = 2 * ge_signed_half_prefix_source_leftsecondvaluedecode + 1 /\ (ge_balance_positive_prefix_source_leftsecondvalue) = 0) /\ (ge_balance_negative_prefix_source_leftsecondvalue) = S ge_signed_half_prefix_source_leftsecondvaluedecode))) /\ ((dst_positive_prefix_source_leftsecond) + ge_balance_negative_prefix_source_leftsecondvalue = (dst_negative_prefix_source_leftsecond) + ge_balance_positive_prefix_source_leftsecondvalue))))))))) -> dm_first_value_prefix_source_left=dm_second_value_prefix_source_left) -> (forall dm_index_prefix_source_right dm_first_value_prefix_source_right dm_second_value_prefix_source_right. ~(dm_index_prefix_source_right=0) -> (exists pvs_le_gap_prefix_source_rightdomain. pvs_le_gap_prefix_source_rightdomain + (dm_index_prefix_source_right) = (n)) -> (exists dst_positive_code_prefix_source_rightfirst dst_positive_scale_prefix_source_rightfirst dst_negative_code_prefix_source_rightfirst dst_negative_scale_prefix_source_rightfirst dst_positive_prefix_source_rightfirst dst_negative_prefix_source_rightfirst. (((G) = (((((dst_positive_code_prefix_source_rightfirst) + (dst_positive_scale_prefix_source_rightfirst)) * S ((dst_positive_code_prefix_source_rightfirst) + (dst_positive_scale_prefix_source_rightfirst)) + ((dst_positive_scale_prefix_source_rightfirst) + (dst_positive_scale_prefix_source_rightfirst))) + (((dst_negative_code_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)) * S ((dst_negative_code_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)) + ((dst_negative_scale_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)))) * S ((((dst_positive_code_prefix_source_rightfirst) + (dst_positive_scale_prefix_source_rightfirst)) * S ((dst_positive_code_prefix_source_rightfirst) + (dst_positive_scale_prefix_source_rightfirst)) + ((dst_positive_scale_prefix_source_rightfirst) + (dst_positive_scale_prefix_source_rightfirst))) + (((dst_negative_code_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)) * S ((dst_negative_code_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)) + ((dst_negative_scale_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)))) + ((((dst_negative_code_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)) * S ((dst_negative_code_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)) + ((dst_negative_scale_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst))) + (((dst_negative_code_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)) * S ((dst_negative_code_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)) + ((dst_negative_scale_prefix_source_rightfirst) + (dst_negative_scale_prefix_source_rightfirst)))))) /\ (((((exists ff_h_pvs_prefix_source_rightfirstpositive. ff_h_pvs_prefix_source_rightfirstpositive + S (dst_positive_prefix_source_rightfirst) = S ((S (dm_index_prefix_source_right)) * dst_positive_scale_prefix_source_rightfirst)) /\ exists ff_q_pvs_prefix_source_rightfirstpositive. dst_positive_code_prefix_source_rightfirst = ff_q_pvs_prefix_source_rightfirstpositive * S ((S (dm_index_prefix_source_right)) * dst_positive_scale_prefix_source_rightfirst) + (dst_positive_prefix_source_rightfirst))) /\ (((((exists ff_h_pvs_prefix_source_rightfirstnegative. ff_h_pvs_prefix_source_rightfirstnegative + S (dst_negative_prefix_source_rightfirst) = S ((S (dm_index_prefix_source_right)) * dst_negative_scale_prefix_source_rightfirst)) /\ exists ff_q_pvs_prefix_source_rightfirstnegative. dst_negative_code_prefix_source_rightfirst = ff_q_pvs_prefix_source_rightfirstnegative * S ((S (dm_index_prefix_source_right)) * dst_negative_scale_prefix_source_rightfirst) + (dst_negative_prefix_source_rightfirst))) /\ (exists ge_balance_positive_prefix_source_rightfirstvalue ge_balance_negative_prefix_source_rightfirstvalue. (((((dm_first_value_prefix_source_right) = 2 * (ge_balance_positive_prefix_source_rightfirstvalue) /\ (ge_balance_negative_prefix_source_rightfirstvalue) = 0) \/ exists ge_signed_half_prefix_source_rightfirstvaluedecode. (((dm_first_value_prefix_source_right) = 2 * ge_signed_half_prefix_source_rightfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_source_rightfirstvalue) = 0) /\ (ge_balance_negative_prefix_source_rightfirstvalue) = S ge_signed_half_prefix_source_rightfirstvaluedecode))) /\ ((dst_positive_prefix_source_rightfirst) + ge_balance_negative_prefix_source_rightfirstvalue = (dst_negative_prefix_source_rightfirst) + ge_balance_positive_prefix_source_rightfirstvalue))))))))) -> (exists dst_positive_code_prefix_source_rightsecond dst_positive_scale_prefix_source_rightsecond dst_negative_code_prefix_source_rightsecond dst_negative_scale_prefix_source_rightsecond dst_positive_prefix_source_rightsecond dst_negative_prefix_source_rightsecond. (((K) = (((((dst_positive_code_prefix_source_rightsecond) + (dst_positive_scale_prefix_source_rightsecond)) * S ((dst_positive_code_prefix_source_rightsecond) + (dst_positive_scale_prefix_source_rightsecond)) + ((dst_positive_scale_prefix_source_rightsecond) + (dst_positive_scale_prefix_source_rightsecond))) + (((dst_negative_code_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)) * S ((dst_negative_code_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)) + ((dst_negative_scale_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)))) * S ((((dst_positive_code_prefix_source_rightsecond) + (dst_positive_scale_prefix_source_rightsecond)) * S ((dst_positive_code_prefix_source_rightsecond) + (dst_positive_scale_prefix_source_rightsecond)) + ((dst_positive_scale_prefix_source_rightsecond) + (dst_positive_scale_prefix_source_rightsecond))) + (((dst_negative_code_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)) * S ((dst_negative_code_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)) + ((dst_negative_scale_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)))) + ((((dst_negative_code_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)) * S ((dst_negative_code_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)) + ((dst_negative_scale_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond))) + (((dst_negative_code_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)) * S ((dst_negative_code_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)) + ((dst_negative_scale_prefix_source_rightsecond) + (dst_negative_scale_prefix_source_rightsecond)))))) /\ (((((exists ff_h_pvs_prefix_source_rightsecondpositive. ff_h_pvs_prefix_source_rightsecondpositive + S (dst_positive_prefix_source_rightsecond) = S ((S (dm_index_prefix_source_right)) * dst_positive_scale_prefix_source_rightsecond)) /\ exists ff_q_pvs_prefix_source_rightsecondpositive. dst_positive_code_prefix_source_rightsecond = ff_q_pvs_prefix_source_rightsecondpositive * S ((S (dm_index_prefix_source_right)) * dst_positive_scale_prefix_source_rightsecond) + (dst_positive_prefix_source_rightsecond))) /\ (((((exists ff_h_pvs_prefix_source_rightsecondnegative. ff_h_pvs_prefix_source_rightsecondnegative + S (dst_negative_prefix_source_rightsecond) = S ((S (dm_index_prefix_source_right)) * dst_negative_scale_prefix_source_rightsecond)) /\ exists ff_q_pvs_prefix_source_rightsecondnegative. dst_negative_code_prefix_source_rightsecond = ff_q_pvs_prefix_source_rightsecondnegative * S ((S (dm_index_prefix_source_right)) * dst_negative_scale_prefix_source_rightsecond) + (dst_negative_prefix_source_rightsecond))) /\ (exists ge_balance_positive_prefix_source_rightsecondvalue ge_balance_negative_prefix_source_rightsecondvalue. (((((dm_second_value_prefix_source_right) = 2 * (ge_balance_positive_prefix_source_rightsecondvalue) /\ (ge_balance_negative_prefix_source_rightsecondvalue) = 0) \/ exists ge_signed_half_prefix_source_rightsecondvaluedecode. (((dm_second_value_prefix_source_right) = 2 * ge_signed_half_prefix_source_rightsecondvaluedecode + 1 /\ (ge_balance_positive_prefix_source_rightsecondvalue) = 0) /\ (ge_balance_negative_prefix_source_rightsecondvalue) = S ge_signed_half_prefix_source_rightsecondvaluedecode))) /\ ((dst_positive_prefix_source_rightsecond) + ge_balance_negative_prefix_source_rightsecondvalue = (dst_negative_prefix_source_rightsecond) + ge_balance_positive_prefix_source_rightsecondvalue))))))))) -> dm_first_value_prefix_source_right=dm_second_value_prefix_source_right) -> (((exists dst_positive_code_prefix_source_firsttable dst_positive_scale_prefix_source_firsttable dst_negative_code_prefix_source_firsttable dst_negative_scale_prefix_source_firsttable. (((M) = (((((dst_positive_code_prefix_source_firsttable) + (dst_positive_scale_prefix_source_firsttable)) * S ((dst_positive_code_prefix_source_firsttable) + (dst_positive_scale_prefix_source_firsttable)) + ((dst_positive_scale_prefix_source_firsttable) + (dst_positive_scale_prefix_source_firsttable))) + (((dst_negative_code_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)) * S ((dst_negative_code_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)) + ((dst_negative_scale_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)))) * S ((((dst_positive_code_prefix_source_firsttable) + (dst_positive_scale_prefix_source_firsttable)) * S ((dst_positive_code_prefix_source_firsttable) + (dst_positive_scale_prefix_source_firsttable)) + ((dst_positive_scale_prefix_source_firsttable) + (dst_positive_scale_prefix_source_firsttable))) + (((dst_negative_code_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)) * S ((dst_negative_code_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)) + ((dst_negative_scale_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)))) + ((((dst_negative_code_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)) * S ((dst_negative_code_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)) + ((dst_negative_scale_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable))) + (((dst_negative_code_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)) * S ((dst_negative_code_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)) + ((dst_negative_scale_prefix_source_firsttable) + (dst_negative_scale_prefix_source_firsttable)))))) /\ (forall dst_index_prefix_source_firsttable. (exists pvs_le_gap_prefix_source_firsttabledomain. pvs_le_gap_prefix_source_firsttabledomain + (dst_index_prefix_source_firsttable) = (n)) -> exists dst_positive_prefix_source_firsttable dst_negative_prefix_source_firsttable dst_value_prefix_source_firsttable. ((((exists ff_h_pvs_prefix_source_firsttableentrypositive. ff_h_pvs_prefix_source_firsttableentrypositive + S (dst_positive_prefix_source_firsttable) = S ((S (dst_index_prefix_source_firsttable)) * dst_positive_scale_prefix_source_firsttable)) /\ exists ff_q_pvs_prefix_source_firsttableentrypositive. dst_positive_code_prefix_source_firsttable = ff_q_pvs_prefix_source_firsttableentrypositive * S ((S (dst_index_prefix_source_firsttable)) * dst_positive_scale_prefix_source_firsttable) + (dst_positive_prefix_source_firsttable))) /\ (((((exists ff_h_pvs_prefix_source_firsttableentrynegative. ff_h_pvs_prefix_source_firsttableentrynegative + S (dst_negative_prefix_source_firsttable) = S ((S (dst_index_prefix_source_firsttable)) * dst_negative_scale_prefix_source_firsttable)) /\ exists ff_q_pvs_prefix_source_firsttableentrynegative. dst_negative_code_prefix_source_firsttable = ff_q_pvs_prefix_source_firsttableentrynegative * S ((S (dst_index_prefix_source_firsttable)) * dst_negative_scale_prefix_source_firsttable) + (dst_negative_prefix_source_firsttable))) /\ (exists ge_balance_positive_prefix_source_firsttableentryvalue ge_balance_negative_prefix_source_firsttableentryvalue. (((((dst_value_prefix_source_firsttable) = 2 * (ge_balance_positive_prefix_source_firsttableentryvalue) /\ (ge_balance_negative_prefix_source_firsttableentryvalue) = 0) \/ exists ge_signed_half_prefix_source_firsttableentryvaluedecode. (((dst_value_prefix_source_firsttable) = 2 * ge_signed_half_prefix_source_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_source_firsttableentryvalue) = 0) /\ (ge_balance_negative_prefix_source_firsttableentryvalue) = S ge_signed_half_prefix_source_firsttableentryvaluedecode))) /\ ((dst_positive_prefix_source_firsttable) + ge_balance_negative_prefix_source_firsttableentryvalue = (dst_negative_prefix_source_firsttable) + ge_balance_positive_prefix_source_firsttableentryvalue))))))))) /\ (forall dc_index_prefix_source_first dc_value_prefix_source_first. (exists pvs_le_gap_prefix_source_firstdomain. pvs_le_gap_prefix_source_firstdomain + (dc_index_prefix_source_first) = (n)) -> (exists dst_positive_code_prefix_source_firstlookup dst_positive_scale_prefix_source_firstlookup dst_negative_code_prefix_source_firstlookup dst_negative_scale_prefix_source_firstlookup dst_positive_prefix_source_firstlookup dst_negative_prefix_source_firstlookup. (((M) = (((((dst_positive_code_prefix_source_firstlookup) + (dst_positive_scale_prefix_source_firstlookup)) * S ((dst_positive_code_prefix_source_firstlookup) + (dst_positive_scale_prefix_source_firstlookup)) + ((dst_positive_scale_prefix_source_firstlookup) + (dst_positive_scale_prefix_source_firstlookup))) + (((dst_negative_code_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)) * S ((dst_negative_code_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)) + ((dst_negative_scale_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)))) * S ((((dst_positive_code_prefix_source_firstlookup) + (dst_positive_scale_prefix_source_firstlookup)) * S ((dst_positive_code_prefix_source_firstlookup) + (dst_positive_scale_prefix_source_firstlookup)) + ((dst_positive_scale_prefix_source_firstlookup) + (dst_positive_scale_prefix_source_firstlookup))) + (((dst_negative_code_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)) * S ((dst_negative_code_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)) + ((dst_negative_scale_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)))) + ((((dst_negative_code_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)) * S ((dst_negative_code_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)) + ((dst_negative_scale_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup))) + (((dst_negative_code_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)) * S ((dst_negative_code_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)) + ((dst_negative_scale_prefix_source_firstlookup) + (dst_negative_scale_prefix_source_firstlookup)))))) /\ (((((exists ff_h_pvs_prefix_source_firstlookuppositive. ff_h_pvs_prefix_source_firstlookuppositive + S (dst_positive_prefix_source_firstlookup) = S ((S (dc_index_prefix_source_first)) * dst_positive_scale_prefix_source_firstlookup)) /\ exists ff_q_pvs_prefix_source_firstlookuppositive. dst_positive_code_prefix_source_firstlookup = ff_q_pvs_prefix_source_firstlookuppositive * S ((S (dc_index_prefix_source_first)) * dst_positive_scale_prefix_source_firstlookup) + (dst_positive_prefix_source_firstlookup))) /\ (((((exists ff_h_pvs_prefix_source_firstlookupnegative. ff_h_pvs_prefix_source_firstlookupnegative + S (dst_negative_prefix_source_firstlookup) = S ((S (dc_index_prefix_source_first)) * dst_negative_scale_prefix_source_firstlookup)) /\ exists ff_q_pvs_prefix_source_firstlookupnegative. dst_negative_code_prefix_source_firstlookup = ff_q_pvs_prefix_source_firstlookupnegative * S ((S (dc_index_prefix_source_first)) * dst_negative_scale_prefix_source_firstlookup) + (dst_negative_prefix_source_firstlookup))) /\ (exists ge_balance_positive_prefix_source_firstlookupvalue ge_balance_negative_prefix_source_firstlookupvalue. (((((dc_value_prefix_source_first) = 2 * (ge_balance_positive_prefix_source_firstlookupvalue) /\ (ge_balance_negative_prefix_source_firstlookupvalue) = 0) \/ exists ge_signed_half_prefix_source_firstlookupvaluedecode. (((dc_value_prefix_source_first) = 2 * ge_signed_half_prefix_source_firstlookupvaluedecode + 1 /\ (ge_balance_positive_prefix_source_firstlookupvalue) = 0) /\ (ge_balance_negative_prefix_source_firstlookupvalue) = S ge_signed_half_prefix_source_firstlookupvaluedecode))) /\ ((dst_positive_prefix_source_firstlookup) + ge_balance_negative_prefix_source_firstlookupvalue = (dst_negative_prefix_source_firstlookup) + ge_balance_positive_prefix_source_firstlookupvalue))))))))) -> ((((~((dc_index_prefix_source_first)=0)) /\ (exists dc_quotient_prefix_source_firstentry dc_left_prefix_source_firstentry dc_right_prefix_source_firstentry. (((n)=(dc_index_prefix_source_first)*dc_quotient_prefix_source_firstentry) /\ (((exists dst_positive_code_prefix_source_firstentryleft dst_positive_scale_prefix_source_firstentryleft dst_negative_code_prefix_source_firstentryleft dst_negative_scale_prefix_source_firstentryleft dst_positive_prefix_source_firstentryleft dst_negative_prefix_source_firstentryleft. (((F) = (((((dst_positive_code_prefix_source_firstentryleft) + (dst_positive_scale_prefix_source_firstentryleft)) * S ((dst_positive_code_prefix_source_firstentryleft) + (dst_positive_scale_prefix_source_firstentryleft)) + ((dst_positive_scale_prefix_source_firstentryleft) + (dst_positive_scale_prefix_source_firstentryleft))) + (((dst_negative_code_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)) * S ((dst_negative_code_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)) + ((dst_negative_scale_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)))) * S ((((dst_positive_code_prefix_source_firstentryleft) + (dst_positive_scale_prefix_source_firstentryleft)) * S ((dst_positive_code_prefix_source_firstentryleft) + (dst_positive_scale_prefix_source_firstentryleft)) + ((dst_positive_scale_prefix_source_firstentryleft) + (dst_positive_scale_prefix_source_firstentryleft))) + (((dst_negative_code_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)) * S ((dst_negative_code_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)) + ((dst_negative_scale_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)))) + ((((dst_negative_code_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)) * S ((dst_negative_code_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)) + ((dst_negative_scale_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft))) + (((dst_negative_code_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)) * S ((dst_negative_code_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)) + ((dst_negative_scale_prefix_source_firstentryleft) + (dst_negative_scale_prefix_source_firstentryleft)))))) /\ (((((exists ff_h_pvs_prefix_source_firstentryleftpositive. ff_h_pvs_prefix_source_firstentryleftpositive + S (dst_positive_prefix_source_firstentryleft) = S ((S (dc_index_prefix_source_first)) * dst_positive_scale_prefix_source_firstentryleft)) /\ exists ff_q_pvs_prefix_source_firstentryleftpositive. dst_positive_code_prefix_source_firstentryleft = ff_q_pvs_prefix_source_firstentryleftpositive * S ((S (dc_index_prefix_source_first)) * dst_positive_scale_prefix_source_firstentryleft) + (dst_positive_prefix_source_firstentryleft))) /\ (((((exists ff_h_pvs_prefix_source_firstentryleftnegative. ff_h_pvs_prefix_source_firstentryleftnegative + S (dst_negative_prefix_source_firstentryleft) = S ((S (dc_index_prefix_source_first)) * dst_negative_scale_prefix_source_firstentryleft)) /\ exists ff_q_pvs_prefix_source_firstentryleftnegative. dst_negative_code_prefix_source_firstentryleft = ff_q_pvs_prefix_source_firstentryleftnegative * S ((S (dc_index_prefix_source_first)) * dst_negative_scale_prefix_source_firstentryleft) + (dst_negative_prefix_source_firstentryleft))) /\ (exists ge_balance_positive_prefix_source_firstentryleftvalue ge_balance_negative_prefix_source_firstentryleftvalue. (((((dc_left_prefix_source_firstentry) = 2 * (ge_balance_positive_prefix_source_firstentryleftvalue) /\ (ge_balance_negative_prefix_source_firstentryleftvalue) = 0) \/ exists ge_signed_half_prefix_source_firstentryleftvaluedecode. (((dc_left_prefix_source_firstentry) = 2 * ge_signed_half_prefix_source_firstentryleftvaluedecode + 1 /\ (ge_balance_positive_prefix_source_firstentryleftvalue) = 0) /\ (ge_balance_negative_prefix_source_firstentryleftvalue) = S ge_signed_half_prefix_source_firstentryleftvaluedecode))) /\ ((dst_positive_prefix_source_firstentryleft) + ge_balance_negative_prefix_source_firstentryleftvalue = (dst_negative_prefix_source_firstentryleft) + ge_balance_positive_prefix_source_firstentryleftvalue))))))))) /\ (((exists dst_positive_code_prefix_source_firstentryright dst_positive_scale_prefix_source_firstentryright dst_negative_code_prefix_source_firstentryright dst_negative_scale_prefix_source_firstentryright dst_positive_prefix_source_firstentryright dst_negative_prefix_source_firstentryright. (((G) = (((((dst_positive_code_prefix_source_firstentryright) + (dst_positive_scale_prefix_source_firstentryright)) * S ((dst_positive_code_prefix_source_firstentryright) + (dst_positive_scale_prefix_source_firstentryright)) + ((dst_positive_scale_prefix_source_firstentryright) + (dst_positive_scale_prefix_source_firstentryright))) + (((dst_negative_code_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)) * S ((dst_negative_code_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)) + ((dst_negative_scale_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)))) * S ((((dst_positive_code_prefix_source_firstentryright) + (dst_positive_scale_prefix_source_firstentryright)) * S ((dst_positive_code_prefix_source_firstentryright) + (dst_positive_scale_prefix_source_firstentryright)) + ((dst_positive_scale_prefix_source_firstentryright) + (dst_positive_scale_prefix_source_firstentryright))) + (((dst_negative_code_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)) * S ((dst_negative_code_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)) + ((dst_negative_scale_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)))) + ((((dst_negative_code_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)) * S ((dst_negative_code_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)) + ((dst_negative_scale_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright))) + (((dst_negative_code_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)) * S ((dst_negative_code_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)) + ((dst_negative_scale_prefix_source_firstentryright) + (dst_negative_scale_prefix_source_firstentryright)))))) /\ (((((exists ff_h_pvs_prefix_source_firstentryrightpositive. ff_h_pvs_prefix_source_firstentryrightpositive + S (dst_positive_prefix_source_firstentryright) = S ((S (dc_quotient_prefix_source_firstentry)) * dst_positive_scale_prefix_source_firstentryright)) /\ exists ff_q_pvs_prefix_source_firstentryrightpositive. dst_positive_code_prefix_source_firstentryright = ff_q_pvs_prefix_source_firstentryrightpositive * S ((S (dc_quotient_prefix_source_firstentry)) * dst_positive_scale_prefix_source_firstentryright) + (dst_positive_prefix_source_firstentryright))) /\ (((((exists ff_h_pvs_prefix_source_firstentryrightnegative. ff_h_pvs_prefix_source_firstentryrightnegative + S (dst_negative_prefix_source_firstentryright) = S ((S (dc_quotient_prefix_source_firstentry)) * dst_negative_scale_prefix_source_firstentryright)) /\ exists ff_q_pvs_prefix_source_firstentryrightnegative. dst_negative_code_prefix_source_firstentryright = ff_q_pvs_prefix_source_firstentryrightnegative * S ((S (dc_quotient_prefix_source_firstentry)) * dst_negative_scale_prefix_source_firstentryright) + (dst_negative_prefix_source_firstentryright))) /\ (exists ge_balance_positive_prefix_source_firstentryrightvalue ge_balance_negative_prefix_source_firstentryrightvalue. (((((dc_right_prefix_source_firstentry) = 2 * (ge_balance_positive_prefix_source_firstentryrightvalue) /\ (ge_balance_negative_prefix_source_firstentryrightvalue) = 0) \/ exists ge_signed_half_prefix_source_firstentryrightvaluedecode. (((dc_right_prefix_source_firstentry) = 2 * ge_signed_half_prefix_source_firstentryrightvaluedecode + 1 /\ (ge_balance_positive_prefix_source_firstentryrightvalue) = 0) /\ (ge_balance_negative_prefix_source_firstentryrightvalue) = S ge_signed_half_prefix_source_firstentryrightvaluedecode))) /\ ((dst_positive_prefix_source_firstentryright) + ge_balance_negative_prefix_source_firstentryrightvalue = (dst_negative_prefix_source_firstentryright) + ge_balance_positive_prefix_source_firstentryrightvalue))))))))) /\ (exists sto_ap_prefix_source_firstentryproduct sto_an_prefix_source_firstentryproduct sto_bp_prefix_source_firstentryproduct sto_bn_prefix_source_firstentryproduct sto_cp_prefix_source_firstentryproduct sto_cn_prefix_source_firstentryproduct. (((((dc_left_prefix_source_firstentry) = 2 * (sto_ap_prefix_source_firstentryproduct) /\ (sto_an_prefix_source_firstentryproduct) = 0) \/ exists ge_signed_half_prefix_source_firstentryproductleft. (((dc_left_prefix_source_firstentry) = 2 * ge_signed_half_prefix_source_firstentryproductleft + 1 /\ (sto_ap_prefix_source_firstentryproduct) = 0) /\ (sto_an_prefix_source_firstentryproduct) = S ge_signed_half_prefix_source_firstentryproductleft))) /\ ((((((dc_right_prefix_source_firstentry) = 2 * (sto_bp_prefix_source_firstentryproduct) /\ (sto_bn_prefix_source_firstentryproduct) = 0) \/ exists ge_signed_half_prefix_source_firstentryproductright. (((dc_right_prefix_source_firstentry) = 2 * ge_signed_half_prefix_source_firstentryproductright + 1 /\ (sto_bp_prefix_source_firstentryproduct) = 0) /\ (sto_bn_prefix_source_firstentryproduct) = S ge_signed_half_prefix_source_firstentryproductright))) /\ ((((((dc_value_prefix_source_first) = 2 * (sto_cp_prefix_source_firstentryproduct) /\ (sto_cn_prefix_source_firstentryproduct) = 0) \/ exists ge_signed_half_prefix_source_firstentryproductoutput. (((dc_value_prefix_source_first) = 2 * ge_signed_half_prefix_source_firstentryproductoutput + 1 /\ (sto_cp_prefix_source_firstentryproduct) = 0) /\ (sto_cn_prefix_source_firstentryproduct) = S ge_signed_half_prefix_source_firstentryproductoutput))) /\ ((sto_ap_prefix_source_firstentryproduct * sto_bp_prefix_source_firstentryproduct + sto_an_prefix_source_firstentryproduct * sto_bn_prefix_source_firstentryproduct) + sto_cn_prefix_source_firstentryproduct = (sto_ap_prefix_source_firstentryproduct * sto_bn_prefix_source_firstentryproduct + sto_an_prefix_source_firstentryproduct * sto_bp_prefix_source_firstentryproduct) + sto_cp_prefix_source_firstentryproduct))))))))))))))) \/ ((((dc_index_prefix_source_first)=0 \/ ~(exists pvs_factor_prefix_source_firstentrynondivisor. (n) = (dc_index_prefix_source_first) * pvs_factor_prefix_source_firstentrynondivisor)) /\ ((dc_value_prefix_source_first)=0))))))) -> (((exists dst_positive_code_prefix_source_secondtable dst_positive_scale_prefix_source_secondtable dst_negative_code_prefix_source_secondtable dst_negative_scale_prefix_source_secondtable. (((P) = (((((dst_positive_code_prefix_source_secondtable) + (dst_positive_scale_prefix_source_secondtable)) * S ((dst_positive_code_prefix_source_secondtable) + (dst_positive_scale_prefix_source_secondtable)) + ((dst_positive_scale_prefix_source_secondtable) + (dst_positive_scale_prefix_source_secondtable))) + (((dst_negative_code_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)) * S ((dst_negative_code_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)) + ((dst_negative_scale_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)))) * S ((((dst_positive_code_prefix_source_secondtable) + (dst_positive_scale_prefix_source_secondtable)) * S ((dst_positive_code_prefix_source_secondtable) + (dst_positive_scale_prefix_source_secondtable)) + ((dst_positive_scale_prefix_source_secondtable) + (dst_positive_scale_prefix_source_secondtable))) + (((dst_negative_code_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)) * S ((dst_negative_code_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)) + ((dst_negative_scale_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)))) + ((((dst_negative_code_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)) * S ((dst_negative_code_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)) + ((dst_negative_scale_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable))) + (((dst_negative_code_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)) * S ((dst_negative_code_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)) + ((dst_negative_scale_prefix_source_secondtable) + (dst_negative_scale_prefix_source_secondtable)))))) /\ (forall dst_index_prefix_source_secondtable. (exists pvs_le_gap_prefix_source_secondtabledomain. pvs_le_gap_prefix_source_secondtabledomain + (dst_index_prefix_source_secondtable) = (n)) -> exists dst_positive_prefix_source_secondtable dst_negative_prefix_source_secondtable dst_value_prefix_source_secondtable. ((((exists ff_h_pvs_prefix_source_secondtableentrypositive. ff_h_pvs_prefix_source_secondtableentrypositive + S (dst_positive_prefix_source_secondtable) = S ((S (dst_index_prefix_source_secondtable)) * dst_positive_scale_prefix_source_secondtable)) /\ exists ff_q_pvs_prefix_source_secondtableentrypositive. dst_positive_code_prefix_source_secondtable = ff_q_pvs_prefix_source_secondtableentrypositive * S ((S (dst_index_prefix_source_secondtable)) * dst_positive_scale_prefix_source_secondtable) + (dst_positive_prefix_source_secondtable))) /\ (((((exists ff_h_pvs_prefix_source_secondtableentrynegative. ff_h_pvs_prefix_source_secondtableentrynegative + S (dst_negative_prefix_source_secondtable) = S ((S (dst_index_prefix_source_secondtable)) * dst_negative_scale_prefix_source_secondtable)) /\ exists ff_q_pvs_prefix_source_secondtableentrynegative. dst_negative_code_prefix_source_secondtable = ff_q_pvs_prefix_source_secondtableentrynegative * S ((S (dst_index_prefix_source_secondtable)) * dst_negative_scale_prefix_source_secondtable) + (dst_negative_prefix_source_secondtable))) /\ (exists ge_balance_positive_prefix_source_secondtableentryvalue ge_balance_negative_prefix_source_secondtableentryvalue. (((((dst_value_prefix_source_secondtable) = 2 * (ge_balance_positive_prefix_source_secondtableentryvalue) /\ (ge_balance_negative_prefix_source_secondtableentryvalue) = 0) \/ exists ge_signed_half_prefix_source_secondtableentryvaluedecode. (((dst_value_prefix_source_secondtable) = 2 * ge_signed_half_prefix_source_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_source_secondtableentryvalue) = 0) /\ (ge_balance_negative_prefix_source_secondtableentryvalue) = S ge_signed_half_prefix_source_secondtableentryvaluedecode))) /\ ((dst_positive_prefix_source_secondtable) + ge_balance_negative_prefix_source_secondtableentryvalue = (dst_negative_prefix_source_secondtable) + ge_balance_positive_prefix_source_secondtableentryvalue))))))))) /\ (forall dc_index_prefix_source_second dc_value_prefix_source_second. (exists pvs_le_gap_prefix_source_seconddomain. pvs_le_gap_prefix_source_seconddomain + (dc_index_prefix_source_second) = (n)) -> (exists dst_positive_code_prefix_source_secondlookup dst_positive_scale_prefix_source_secondlookup dst_negative_code_prefix_source_secondlookup dst_negative_scale_prefix_source_secondlookup dst_positive_prefix_source_secondlookup dst_negative_prefix_source_secondlookup. (((P) = (((((dst_positive_code_prefix_source_secondlookup) + (dst_positive_scale_prefix_source_secondlookup)) * S ((dst_positive_code_prefix_source_secondlookup) + (dst_positive_scale_prefix_source_secondlookup)) + ((dst_positive_scale_prefix_source_secondlookup) + (dst_positive_scale_prefix_source_secondlookup))) + (((dst_negative_code_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)) * S ((dst_negative_code_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)) + ((dst_negative_scale_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)))) * S ((((dst_positive_code_prefix_source_secondlookup) + (dst_positive_scale_prefix_source_secondlookup)) * S ((dst_positive_code_prefix_source_secondlookup) + (dst_positive_scale_prefix_source_secondlookup)) + ((dst_positive_scale_prefix_source_secondlookup) + (dst_positive_scale_prefix_source_secondlookup))) + (((dst_negative_code_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)) * S ((dst_negative_code_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)) + ((dst_negative_scale_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)))) + ((((dst_negative_code_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)) * S ((dst_negative_code_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)) + ((dst_negative_scale_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup))) + (((dst_negative_code_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)) * S ((dst_negative_code_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)) + ((dst_negative_scale_prefix_source_secondlookup) + (dst_negative_scale_prefix_source_secondlookup)))))) /\ (((((exists ff_h_pvs_prefix_source_secondlookuppositive. ff_h_pvs_prefix_source_secondlookuppositive + S (dst_positive_prefix_source_secondlookup) = S ((S (dc_index_prefix_source_second)) * dst_positive_scale_prefix_source_secondlookup)) /\ exists ff_q_pvs_prefix_source_secondlookuppositive. dst_positive_code_prefix_source_secondlookup = ff_q_pvs_prefix_source_secondlookuppositive * S ((S (dc_index_prefix_source_second)) * dst_positive_scale_prefix_source_secondlookup) + (dst_positive_prefix_source_secondlookup))) /\ (((((exists ff_h_pvs_prefix_source_secondlookupnegative. ff_h_pvs_prefix_source_secondlookupnegative + S (dst_negative_prefix_source_secondlookup) = S ((S (dc_index_prefix_source_second)) * dst_negative_scale_prefix_source_secondlookup)) /\ exists ff_q_pvs_prefix_source_secondlookupnegative. dst_negative_code_prefix_source_secondlookup = ff_q_pvs_prefix_source_secondlookupnegative * S ((S (dc_index_prefix_source_second)) * dst_negative_scale_prefix_source_secondlookup) + (dst_negative_prefix_source_secondlookup))) /\ (exists ge_balance_positive_prefix_source_secondlookupvalue ge_balance_negative_prefix_source_secondlookupvalue. (((((dc_value_prefix_source_second) = 2 * (ge_balance_positive_prefix_source_secondlookupvalue) /\ (ge_balance_negative_prefix_source_secondlookupvalue) = 0) \/ exists ge_signed_half_prefix_source_secondlookupvaluedecode. (((dc_value_prefix_source_second) = 2 * ge_signed_half_prefix_source_secondlookupvaluedecode + 1 /\ (ge_balance_positive_prefix_source_secondlookupvalue) = 0) /\ (ge_balance_negative_prefix_source_secondlookupvalue) = S ge_signed_half_prefix_source_secondlookupvaluedecode))) /\ ((dst_positive_prefix_source_secondlookup) + ge_balance_negative_prefix_source_secondlookupvalue = (dst_negative_prefix_source_secondlookup) + ge_balance_positive_prefix_source_secondlookupvalue))))))))) -> ((((~((dc_index_prefix_source_second)=0)) /\ (exists dc_quotient_prefix_source_secondentry dc_left_prefix_source_secondentry dc_right_prefix_source_secondentry. (((n)=(dc_index_prefix_source_second)*dc_quotient_prefix_source_secondentry) /\ (((exists dst_positive_code_prefix_source_secondentryleft dst_positive_scale_prefix_source_secondentryleft dst_negative_code_prefix_source_secondentryleft dst_negative_scale_prefix_source_secondentryleft dst_positive_prefix_source_secondentryleft dst_negative_prefix_source_secondentryleft. (((H) = (((((dst_positive_code_prefix_source_secondentryleft) + (dst_positive_scale_prefix_source_secondentryleft)) * S ((dst_positive_code_prefix_source_secondentryleft) + (dst_positive_scale_prefix_source_secondentryleft)) + ((dst_positive_scale_prefix_source_secondentryleft) + (dst_positive_scale_prefix_source_secondentryleft))) + (((dst_negative_code_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)) * S ((dst_negative_code_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)) + ((dst_negative_scale_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)))) * S ((((dst_positive_code_prefix_source_secondentryleft) + (dst_positive_scale_prefix_source_secondentryleft)) * S ((dst_positive_code_prefix_source_secondentryleft) + (dst_positive_scale_prefix_source_secondentryleft)) + ((dst_positive_scale_prefix_source_secondentryleft) + (dst_positive_scale_prefix_source_secondentryleft))) + (((dst_negative_code_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)) * S ((dst_negative_code_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)) + ((dst_negative_scale_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)))) + ((((dst_negative_code_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)) * S ((dst_negative_code_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)) + ((dst_negative_scale_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft))) + (((dst_negative_code_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)) * S ((dst_negative_code_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)) + ((dst_negative_scale_prefix_source_secondentryleft) + (dst_negative_scale_prefix_source_secondentryleft)))))) /\ (((((exists ff_h_pvs_prefix_source_secondentryleftpositive. ff_h_pvs_prefix_source_secondentryleftpositive + S (dst_positive_prefix_source_secondentryleft) = S ((S (dc_index_prefix_source_second)) * dst_positive_scale_prefix_source_secondentryleft)) /\ exists ff_q_pvs_prefix_source_secondentryleftpositive. dst_positive_code_prefix_source_secondentryleft = ff_q_pvs_prefix_source_secondentryleftpositive * S ((S (dc_index_prefix_source_second)) * dst_positive_scale_prefix_source_secondentryleft) + (dst_positive_prefix_source_secondentryleft))) /\ (((((exists ff_h_pvs_prefix_source_secondentryleftnegative. ff_h_pvs_prefix_source_secondentryleftnegative + S (dst_negative_prefix_source_secondentryleft) = S ((S (dc_index_prefix_source_second)) * dst_negative_scale_prefix_source_secondentryleft)) /\ exists ff_q_pvs_prefix_source_secondentryleftnegative. dst_negative_code_prefix_source_secondentryleft = ff_q_pvs_prefix_source_secondentryleftnegative * S ((S (dc_index_prefix_source_second)) * dst_negative_scale_prefix_source_secondentryleft) + (dst_negative_prefix_source_secondentryleft))) /\ (exists ge_balance_positive_prefix_source_secondentryleftvalue ge_balance_negative_prefix_source_secondentryleftvalue. (((((dc_left_prefix_source_secondentry) = 2 * (ge_balance_positive_prefix_source_secondentryleftvalue) /\ (ge_balance_negative_prefix_source_secondentryleftvalue) = 0) \/ exists ge_signed_half_prefix_source_secondentryleftvaluedecode. (((dc_left_prefix_source_secondentry) = 2 * ge_signed_half_prefix_source_secondentryleftvaluedecode + 1 /\ (ge_balance_positive_prefix_source_secondentryleftvalue) = 0) /\ (ge_balance_negative_prefix_source_secondentryleftvalue) = S ge_signed_half_prefix_source_secondentryleftvaluedecode))) /\ ((dst_positive_prefix_source_secondentryleft) + ge_balance_negative_prefix_source_secondentryleftvalue = (dst_negative_prefix_source_secondentryleft) + ge_balance_positive_prefix_source_secondentryleftvalue))))))))) /\ (((exists dst_positive_code_prefix_source_secondentryright dst_positive_scale_prefix_source_secondentryright dst_negative_code_prefix_source_secondentryright dst_negative_scale_prefix_source_secondentryright dst_positive_prefix_source_secondentryright dst_negative_prefix_source_secondentryright. (((K) = (((((dst_positive_code_prefix_source_secondentryright) + (dst_positive_scale_prefix_source_secondentryright)) * S ((dst_positive_code_prefix_source_secondentryright) + (dst_positive_scale_prefix_source_secondentryright)) + ((dst_positive_scale_prefix_source_secondentryright) + (dst_positive_scale_prefix_source_secondentryright))) + (((dst_negative_code_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)) * S ((dst_negative_code_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)) + ((dst_negative_scale_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)))) * S ((((dst_positive_code_prefix_source_secondentryright) + (dst_positive_scale_prefix_source_secondentryright)) * S ((dst_positive_code_prefix_source_secondentryright) + (dst_positive_scale_prefix_source_secondentryright)) + ((dst_positive_scale_prefix_source_secondentryright) + (dst_positive_scale_prefix_source_secondentryright))) + (((dst_negative_code_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)) * S ((dst_negative_code_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)) + ((dst_negative_scale_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)))) + ((((dst_negative_code_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)) * S ((dst_negative_code_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)) + ((dst_negative_scale_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright))) + (((dst_negative_code_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)) * S ((dst_negative_code_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)) + ((dst_negative_scale_prefix_source_secondentryright) + (dst_negative_scale_prefix_source_secondentryright)))))) /\ (((((exists ff_h_pvs_prefix_source_secondentryrightpositive. ff_h_pvs_prefix_source_secondentryrightpositive + S (dst_positive_prefix_source_secondentryright) = S ((S (dc_quotient_prefix_source_secondentry)) * dst_positive_scale_prefix_source_secondentryright)) /\ exists ff_q_pvs_prefix_source_secondentryrightpositive. dst_positive_code_prefix_source_secondentryright = ff_q_pvs_prefix_source_secondentryrightpositive * S ((S (dc_quotient_prefix_source_secondentry)) * dst_positive_scale_prefix_source_secondentryright) + (dst_positive_prefix_source_secondentryright))) /\ (((((exists ff_h_pvs_prefix_source_secondentryrightnegative. ff_h_pvs_prefix_source_secondentryrightnegative + S (dst_negative_prefix_source_secondentryright) = S ((S (dc_quotient_prefix_source_secondentry)) * dst_negative_scale_prefix_source_secondentryright)) /\ exists ff_q_pvs_prefix_source_secondentryrightnegative. dst_negative_code_prefix_source_secondentryright = ff_q_pvs_prefix_source_secondentryrightnegative * S ((S (dc_quotient_prefix_source_secondentry)) * dst_negative_scale_prefix_source_secondentryright) + (dst_negative_prefix_source_secondentryright))) /\ (exists ge_balance_positive_prefix_source_secondentryrightvalue ge_balance_negative_prefix_source_secondentryrightvalue. (((((dc_right_prefix_source_secondentry) = 2 * (ge_balance_positive_prefix_source_secondentryrightvalue) /\ (ge_balance_negative_prefix_source_secondentryrightvalue) = 0) \/ exists ge_signed_half_prefix_source_secondentryrightvaluedecode. (((dc_right_prefix_source_secondentry) = 2 * ge_signed_half_prefix_source_secondentryrightvaluedecode + 1 /\ (ge_balance_positive_prefix_source_secondentryrightvalue) = 0) /\ (ge_balance_negative_prefix_source_secondentryrightvalue) = S ge_signed_half_prefix_source_secondentryrightvaluedecode))) /\ ((dst_positive_prefix_source_secondentryright) + ge_balance_negative_prefix_source_secondentryrightvalue = (dst_negative_prefix_source_secondentryright) + ge_balance_positive_prefix_source_secondentryrightvalue))))))))) /\ (exists sto_ap_prefix_source_secondentryproduct sto_an_prefix_source_secondentryproduct sto_bp_prefix_source_secondentryproduct sto_bn_prefix_source_secondentryproduct sto_cp_prefix_source_secondentryproduct sto_cn_prefix_source_secondentryproduct. (((((dc_left_prefix_source_secondentry) = 2 * (sto_ap_prefix_source_secondentryproduct) /\ (sto_an_prefix_source_secondentryproduct) = 0) \/ exists ge_signed_half_prefix_source_secondentryproductleft. (((dc_left_prefix_source_secondentry) = 2 * ge_signed_half_prefix_source_secondentryproductleft + 1 /\ (sto_ap_prefix_source_secondentryproduct) = 0) /\ (sto_an_prefix_source_secondentryproduct) = S ge_signed_half_prefix_source_secondentryproductleft))) /\ ((((((dc_right_prefix_source_secondentry) = 2 * (sto_bp_prefix_source_secondentryproduct) /\ (sto_bn_prefix_source_secondentryproduct) = 0) \/ exists ge_signed_half_prefix_source_secondentryproductright. (((dc_right_prefix_source_secondentry) = 2 * ge_signed_half_prefix_source_secondentryproductright + 1 /\ (sto_bp_prefix_source_secondentryproduct) = 0) /\ (sto_bn_prefix_source_secondentryproduct) = S ge_signed_half_prefix_source_secondentryproductright))) /\ ((((((dc_value_prefix_source_second) = 2 * (sto_cp_prefix_source_secondentryproduct) /\ (sto_cn_prefix_source_secondentryproduct) = 0) \/ exists ge_signed_half_prefix_source_secondentryproductoutput. (((dc_value_prefix_source_second) = 2 * ge_signed_half_prefix_source_secondentryproductoutput + 1 /\ (sto_cp_prefix_source_secondentryproduct) = 0) /\ (sto_cn_prefix_source_secondentryproduct) = S ge_signed_half_prefix_source_secondentryproductoutput))) /\ ((sto_ap_prefix_source_secondentryproduct * sto_bp_prefix_source_secondentryproduct + sto_an_prefix_source_secondentryproduct * sto_bn_prefix_source_secondentryproduct) + sto_cn_prefix_source_secondentryproduct = (sto_ap_prefix_source_secondentryproduct * sto_bn_prefix_source_secondentryproduct + sto_an_prefix_source_secondentryproduct * sto_bp_prefix_source_secondentryproduct) + sto_cp_prefix_source_secondentryproduct))))))))))))))) \/ ((((dc_index_prefix_source_second)=0 \/ ~(exists pvs_factor_prefix_source_secondentrynondivisor. (n) = (dc_index_prefix_source_second) * pvs_factor_prefix_source_secondentrynondivisor)) /\ ((dc_value_prefix_source_second)=0))))))) -> (forall dst_index_prefix_source_result dst_first_prefix_source_result dst_second_prefix_source_result. (exists pvs_gap_prefix_source_resultbound. pvs_gap_prefix_source_resultbound + S (dst_index_prefix_source_result) = (S n)) -> (exists dst_positive_code_prefix_source_resultfirst dst_positive_scale_prefix_source_resultfirst dst_negative_code_prefix_source_resultfirst dst_negative_scale_prefix_source_resultfirst dst_positive_prefix_source_resultfirst dst_negative_prefix_source_resultfirst. (((M) = (((((dst_positive_code_prefix_source_resultfirst) + (dst_positive_scale_prefix_source_resultfirst)) * S ((dst_positive_code_prefix_source_resultfirst) + (dst_positive_scale_prefix_source_resultfirst)) + ((dst_positive_scale_prefix_source_resultfirst) + (dst_positive_scale_prefix_source_resultfirst))) + (((dst_negative_code_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)) * S ((dst_negative_code_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)) + ((dst_negative_scale_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)))) * S ((((dst_positive_code_prefix_source_resultfirst) + (dst_positive_scale_prefix_source_resultfirst)) * S ((dst_positive_code_prefix_source_resultfirst) + (dst_positive_scale_prefix_source_resultfirst)) + ((dst_positive_scale_prefix_source_resultfirst) + (dst_positive_scale_prefix_source_resultfirst))) + (((dst_negative_code_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)) * S ((dst_negative_code_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)) + ((dst_negative_scale_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)))) + ((((dst_negative_code_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)) * S ((dst_negative_code_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)) + ((dst_negative_scale_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst))) + (((dst_negative_code_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)) * S ((dst_negative_code_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)) + ((dst_negative_scale_prefix_source_resultfirst) + (dst_negative_scale_prefix_source_resultfirst)))))) /\ (((((exists ff_h_pvs_prefix_source_resultfirstpositive. ff_h_pvs_prefix_source_resultfirstpositive + S (dst_positive_prefix_source_resultfirst) = S ((S (dst_index_prefix_source_result)) * dst_positive_scale_prefix_source_resultfirst)) /\ exists ff_q_pvs_prefix_source_resultfirstpositive. dst_positive_code_prefix_source_resultfirst = ff_q_pvs_prefix_source_resultfirstpositive * S ((S (dst_index_prefix_source_result)) * dst_positive_scale_prefix_source_resultfirst) + (dst_positive_prefix_source_resultfirst))) /\ (((((exists ff_h_pvs_prefix_source_resultfirstnegative. ff_h_pvs_prefix_source_resultfirstnegative + S (dst_negative_prefix_source_resultfirst) = S ((S (dst_index_prefix_source_result)) * dst_negative_scale_prefix_source_resultfirst)) /\ exists ff_q_pvs_prefix_source_resultfirstnegative. dst_negative_code_prefix_source_resultfirst = ff_q_pvs_prefix_source_resultfirstnegative * S ((S (dst_index_prefix_source_result)) * dst_negative_scale_prefix_source_resultfirst) + (dst_negative_prefix_source_resultfirst))) /\ (exists ge_balance_positive_prefix_source_resultfirstvalue ge_balance_negative_prefix_source_resultfirstvalue. (((((dst_first_prefix_source_result) = 2 * (ge_balance_positive_prefix_source_resultfirstvalue) /\ (ge_balance_negative_prefix_source_resultfirstvalue) = 0) \/ exists ge_signed_half_prefix_source_resultfirstvaluedecode. (((dst_first_prefix_source_result) = 2 * ge_signed_half_prefix_source_resultfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_source_resultfirstvalue) = 0) /\ (ge_balance_negative_prefix_source_resultfirstvalue) = S ge_signed_half_prefix_source_resultfirstvaluedecode))) /\ ((dst_positive_prefix_source_resultfirst) + ge_balance_negative_prefix_source_resultfirstvalue = (dst_negative_prefix_source_resultfirst) + ge_balance_positive_prefix_source_resultfirstvalue))))))))) -> (exists dst_positive_code_prefix_source_resultsecond dst_positive_scale_prefix_source_resultsecond dst_negative_code_prefix_source_resultsecond dst_negative_scale_prefix_source_resultsecond dst_positive_prefix_source_resultsecond dst_negative_prefix_source_resultsecond. (((P) = (((((dst_positive_code_prefix_source_resultsecond) + (dst_positive_scale_prefix_source_resultsecond)) * S ((dst_positive_code_prefix_source_resultsecond) + (dst_positive_scale_prefix_source_resultsecond)) + ((dst_positive_scale_prefix_source_resultsecond) + (dst_positive_scale_prefix_source_resultsecond))) + (((dst_negative_code_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)) * S ((dst_negative_code_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)) + ((dst_negative_scale_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)))) * S ((((dst_positive_code_prefix_source_resultsecond) + (dst_positive_scale_prefix_source_resultsecond)) * S ((dst_positive_code_prefix_source_resultsecond) + (dst_positive_scale_prefix_source_resultsecond)) + ((dst_positive_scale_prefix_source_resultsecond) + (dst_positive_scale_prefix_source_resultsecond))) + (((dst_negative_code_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)) * S ((dst_negative_code_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)) + ((dst_negative_scale_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)))) + ((((dst_negative_code_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)) * S ((dst_negative_code_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)) + ((dst_negative_scale_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond))) + (((dst_negative_code_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)) * S ((dst_negative_code_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)) + ((dst_negative_scale_prefix_source_resultsecond) + (dst_negative_scale_prefix_source_resultsecond)))))) /\ (((((exists ff_h_pvs_prefix_source_resultsecondpositive. ff_h_pvs_prefix_source_resultsecondpositive + S (dst_positive_prefix_source_resultsecond) = S ((S (dst_index_prefix_source_result)) * dst_positive_scale_prefix_source_resultsecond)) /\ exists ff_q_pvs_prefix_source_resultsecondpositive. dst_positive_code_prefix_source_resultsecond = ff_q_pvs_prefix_source_resultsecondpositive * S ((S (dst_index_prefix_source_result)) * dst_positive_scale_prefix_source_resultsecond) + (dst_positive_prefix_source_resultsecond))) /\ (((((exists ff_h_pvs_prefix_source_resultsecondnegative. ff_h_pvs_prefix_source_resultsecondnegative + S (dst_negative_prefix_source_resultsecond) = S ((S (dst_index_prefix_source_result)) * dst_negative_scale_prefix_source_resultsecond)) /\ exists ff_q_pvs_prefix_source_resultsecondnegative. dst_negative_code_prefix_source_resultsecond = ff_q_pvs_prefix_source_resultsecondnegative * S ((S (dst_index_prefix_source_result)) * dst_negative_scale_prefix_source_resultsecond) + (dst_negative_prefix_source_resultsecond))) /\ (exists ge_balance_positive_prefix_source_resultsecondvalue ge_balance_negative_prefix_source_resultsecondvalue. (((((dst_second_prefix_source_result) = 2 * (ge_balance_positive_prefix_source_resultsecondvalue) /\ (ge_balance_negative_prefix_source_resultsecondvalue) = 0) \/ exists ge_signed_half_prefix_source_resultsecondvaluedecode. (((dst_second_prefix_source_result) = 2 * ge_signed_half_prefix_source_resultsecondvaluedecode + 1 /\ (ge_balance_positive_prefix_source_resultsecondvalue) = 0) /\ (ge_balance_negative_prefix_source_resultsecondvalue) = S ge_signed_half_prefix_source_resultsecondvaluedecode))) /\ ((dst_positive_prefix_source_resultsecond) + ge_balance_negative_prefix_source_resultsecondvalue = (dst_negative_prefix_source_resultsecond) + ge_balance_positive_prefix_source_resultsecondvalue))))))))) -> dst_first_prefix_source_result = dst_second_prefix_source_result)