signed_rectangular_slice_extensional_unique

forall F G H o s l. (((exists dst_positive_code_unique_firstsource_table dst_positive_scale_unique_firstsource_table dst_negative_code_unique_firstsource_table dst_negative_scale_unique_firstsource_table. (((F) = (((((dst_positive_code_unique_firstsource_table) + (dst_positive_scale_unique_firstsource_table)) * S ((dst_positive_code_unique_firstsource_table) + (dst_positive_scale_unique_firstsource_table)) + ((dst_positive_scale_unique_firstsource_table) + (dst_positive_scale_unique_firstsource_table))) + (((dst_negative_code_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)) * S ((dst_negative_code_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)) + ((dst_negative_scale_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)))) * S ((((dst_positive_code_unique_firstsource_table) + (dst_positive_scale_unique_firstsource_table)) * S ((dst_positive_code_unique_firstsource_table) + (dst_positive_scale_unique_firstsource_table)) + ((dst_positive_scale_unique_firstsource_table) + (dst_positive_scale_unique_firstsource_table))) + (((dst_negative_code_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)) * S ((dst_negative_code_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)) + ((dst_negative_scale_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)))) + ((((dst_negative_code_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)) * S ((dst_negative_code_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)) + ((dst_negative_scale_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table))) + (((dst_negative_code_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)) * S ((dst_negative_code_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)) + ((dst_negative_scale_unique_firstsource_table) + (dst_negative_scale_unique_firstsource_table)))))) /\ (forall dst_index_unique_firstsource_table. (exists pvs_le_gap_unique_firstsource_tabledomain. pvs_le_gap_unique_firstsource_tabledomain + (dst_index_unique_firstsource_table) = (0)) -> exists dst_positive_unique_firstsource_table dst_negative_unique_firstsource_table dst_value_unique_firstsource_table. ((((exists ff_h_pvs_unique_firstsource_tableentrypositive. ff_h_pvs_unique_firstsource_tableentrypositive + S (dst_positive_unique_firstsource_table) = S ((S (dst_index_unique_firstsource_table)) * dst_positive_scale_unique_firstsource_table)) /\ exists ff_q_pvs_unique_firstsource_tableentrypositive. dst_positive_code_unique_firstsource_table = ff_q_pvs_unique_firstsource_tableentrypositive * S ((S (dst_index_unique_firstsource_table)) * dst_positive_scale_unique_firstsource_table) + (dst_positive_unique_firstsource_table))) /\ (((((exists ff_h_pvs_unique_firstsource_tableentrynegative. ff_h_pvs_unique_firstsource_tableentrynegative + S (dst_negative_unique_firstsource_table) = S ((S (dst_index_unique_firstsource_table)) * dst_negative_scale_unique_firstsource_table)) /\ exists ff_q_pvs_unique_firstsource_tableentrynegative. dst_negative_code_unique_firstsource_table = ff_q_pvs_unique_firstsource_tableentrynegative * S ((S (dst_index_unique_firstsource_table)) * dst_negative_scale_unique_firstsource_table) + (dst_negative_unique_firstsource_table))) /\ (exists ge_balance_positive_unique_firstsource_tableentryvalue ge_balance_negative_unique_firstsource_tableentryvalue. (((((dst_value_unique_firstsource_table) = 2 * (ge_balance_positive_unique_firstsource_tableentryvalue) /\ (ge_balance_negative_unique_firstsource_tableentryvalue) = 0) \/ exists ge_signed_half_unique_firstsource_tableentryvaluedecode. (((dst_value_unique_firstsource_table) = 2 * ge_signed_half_unique_firstsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_unique_firstsource_tableentryvalue) = 0) /\ (ge_balance_negative_unique_firstsource_tableentryvalue) = S ge_signed_half_unique_firstsource_tableentryvaluedecode))) /\ ((dst_positive_unique_firstsource_table) + ge_balance_negative_unique_firstsource_tableentryvalue = (dst_negative_unique_firstsource_table) + ge_balance_positive_unique_firstsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_unique_firstoutput_table dst_positive_scale_unique_firstoutput_table dst_negative_code_unique_firstoutput_table dst_negative_scale_unique_firstoutput_table. (((G) = (((((dst_positive_code_unique_firstoutput_table) + (dst_positive_scale_unique_firstoutput_table)) * S ((dst_positive_code_unique_firstoutput_table) + (dst_positive_scale_unique_firstoutput_table)) + ((dst_positive_scale_unique_firstoutput_table) + (dst_positive_scale_unique_firstoutput_table))) + (((dst_negative_code_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)) * S ((dst_negative_code_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)) + ((dst_negative_scale_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)))) * S ((((dst_positive_code_unique_firstoutput_table) + (dst_positive_scale_unique_firstoutput_table)) * S ((dst_positive_code_unique_firstoutput_table) + (dst_positive_scale_unique_firstoutput_table)) + ((dst_positive_scale_unique_firstoutput_table) + (dst_positive_scale_unique_firstoutput_table))) + (((dst_negative_code_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)) * S ((dst_negative_code_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)) + ((dst_negative_scale_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)))) + ((((dst_negative_code_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)) * S ((dst_negative_code_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)) + ((dst_negative_scale_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table))) + (((dst_negative_code_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)) * S ((dst_negative_code_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)) + ((dst_negative_scale_unique_firstoutput_table) + (dst_negative_scale_unique_firstoutput_table)))))) /\ (forall dst_index_unique_firstoutput_table. (exists pvs_le_gap_unique_firstoutput_tabledomain. pvs_le_gap_unique_firstoutput_tabledomain + (dst_index_unique_firstoutput_table) = (l)) -> exists dst_positive_unique_firstoutput_table dst_negative_unique_firstoutput_table dst_value_unique_firstoutput_table. ((((exists ff_h_pvs_unique_firstoutput_tableentrypositive. ff_h_pvs_unique_firstoutput_tableentrypositive + S (dst_positive_unique_firstoutput_table) = S ((S (dst_index_unique_firstoutput_table)) * dst_positive_scale_unique_firstoutput_table)) /\ exists ff_q_pvs_unique_firstoutput_tableentrypositive. dst_positive_code_unique_firstoutput_table = ff_q_pvs_unique_firstoutput_tableentrypositive * S ((S (dst_index_unique_firstoutput_table)) * dst_positive_scale_unique_firstoutput_table) + (dst_positive_unique_firstoutput_table))) /\ (((((exists ff_h_pvs_unique_firstoutput_tableentrynegative. ff_h_pvs_unique_firstoutput_tableentrynegative + S (dst_negative_unique_firstoutput_table) = S ((S (dst_index_unique_firstoutput_table)) * dst_negative_scale_unique_firstoutput_table)) /\ exists ff_q_pvs_unique_firstoutput_tableentrynegative. dst_negative_code_unique_firstoutput_table = ff_q_pvs_unique_firstoutput_tableentrynegative * S ((S (dst_index_unique_firstoutput_table)) * dst_negative_scale_unique_firstoutput_table) + (dst_negative_unique_firstoutput_table))) /\ (exists ge_balance_positive_unique_firstoutput_tableentryvalue ge_balance_negative_unique_firstoutput_tableentryvalue. (((((dst_value_unique_firstoutput_table) = 2 * (ge_balance_positive_unique_firstoutput_tableentryvalue) /\ (ge_balance_negative_unique_firstoutput_tableentryvalue) = 0) \/ exists ge_signed_half_unique_firstoutput_tableentryvaluedecode. (((dst_value_unique_firstoutput_table) = 2 * ge_signed_half_unique_firstoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_unique_firstoutput_tableentryvalue) = 0) /\ (ge_balance_negative_unique_firstoutput_tableentryvalue) = S ge_signed_half_unique_firstoutput_tableentryvaluedecode))) /\ ((dst_positive_unique_firstoutput_table) + ge_balance_negative_unique_firstoutput_tableentryvalue = (dst_negative_unique_firstoutput_table) + ge_balance_positive_unique_firstoutput_tableentryvalue))))))))) /\ (forall srs_index_unique_first. (exists pvs_gap_unique_firstbound. pvs_gap_unique_firstbound + S (srs_index_unique_first) = (l)) -> exists srs_value_unique_first. (((exists dst_positive_code_unique_firstentrysource dst_positive_scale_unique_firstentrysource dst_negative_code_unique_firstentrysource dst_negative_scale_unique_firstentrysource dst_positive_unique_firstentrysource dst_negative_unique_firstentrysource. (((F) = (((((dst_positive_code_unique_firstentrysource) + (dst_positive_scale_unique_firstentrysource)) * S ((dst_positive_code_unique_firstentrysource) + (dst_positive_scale_unique_firstentrysource)) + ((dst_positive_scale_unique_firstentrysource) + (dst_positive_scale_unique_firstentrysource))) + (((dst_negative_code_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)) * S ((dst_negative_code_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)) + ((dst_negative_scale_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)))) * S ((((dst_positive_code_unique_firstentrysource) + (dst_positive_scale_unique_firstentrysource)) * S ((dst_positive_code_unique_firstentrysource) + (dst_positive_scale_unique_firstentrysource)) + ((dst_positive_scale_unique_firstentrysource) + (dst_positive_scale_unique_firstentrysource))) + (((dst_negative_code_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)) * S ((dst_negative_code_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)) + ((dst_negative_scale_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)))) + ((((dst_negative_code_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)) * S ((dst_negative_code_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)) + ((dst_negative_scale_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource))) + (((dst_negative_code_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)) * S ((dst_negative_code_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)) + ((dst_negative_scale_unique_firstentrysource) + (dst_negative_scale_unique_firstentrysource)))))) /\ (((((exists ff_h_pvs_unique_firstentrysourcepositive. ff_h_pvs_unique_firstentrysourcepositive + S (dst_positive_unique_firstentrysource) = S ((S (((o) + ((s) * (srs_index_unique_first))))) * dst_positive_scale_unique_firstentrysource)) /\ exists ff_q_pvs_unique_firstentrysourcepositive. dst_positive_code_unique_firstentrysource = ff_q_pvs_unique_firstentrysourcepositive * S ((S (((o) + ((s) * (srs_index_unique_first))))) * dst_positive_scale_unique_firstentrysource) + (dst_positive_unique_firstentrysource))) /\ (((((exists ff_h_pvs_unique_firstentrysourcenegative. ff_h_pvs_unique_firstentrysourcenegative + S (dst_negative_unique_firstentrysource) = S ((S (((o) + ((s) * (srs_index_unique_first))))) * dst_negative_scale_unique_firstentrysource)) /\ exists ff_q_pvs_unique_firstentrysourcenegative. dst_negative_code_unique_firstentrysource = ff_q_pvs_unique_firstentrysourcenegative * S ((S (((o) + ((s) * (srs_index_unique_first))))) * dst_negative_scale_unique_firstentrysource) + (dst_negative_unique_firstentrysource))) /\ (exists ge_balance_positive_unique_firstentrysourcevalue ge_balance_negative_unique_firstentrysourcevalue. (((((srs_value_unique_first) = 2 * (ge_balance_positive_unique_firstentrysourcevalue) /\ (ge_balance_negative_unique_firstentrysourcevalue) = 0) \/ exists ge_signed_half_unique_firstentrysourcevaluedecode. (((srs_value_unique_first) = 2 * ge_signed_half_unique_firstentrysourcevaluedecode + 1 /\ (ge_balance_positive_unique_firstentrysourcevalue) = 0) /\ (ge_balance_negative_unique_firstentrysourcevalue) = S ge_signed_half_unique_firstentrysourcevaluedecode))) /\ ((dst_positive_unique_firstentrysource) + ge_balance_negative_unique_firstentrysourcevalue = (dst_negative_unique_firstentrysource) + ge_balance_positive_unique_firstentrysourcevalue))))))))) /\ (exists dst_positive_code_unique_firstentryoutput dst_positive_scale_unique_firstentryoutput dst_negative_code_unique_firstentryoutput dst_negative_scale_unique_firstentryoutput dst_positive_unique_firstentryoutput dst_negative_unique_firstentryoutput. (((G) = (((((dst_positive_code_unique_firstentryoutput) + (dst_positive_scale_unique_firstentryoutput)) * S ((dst_positive_code_unique_firstentryoutput) + (dst_positive_scale_unique_firstentryoutput)) + ((dst_positive_scale_unique_firstentryoutput) + (dst_positive_scale_unique_firstentryoutput))) + (((dst_negative_code_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)) * S ((dst_negative_code_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)) + ((dst_negative_scale_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)))) * S ((((dst_positive_code_unique_firstentryoutput) + (dst_positive_scale_unique_firstentryoutput)) * S ((dst_positive_code_unique_firstentryoutput) + (dst_positive_scale_unique_firstentryoutput)) + ((dst_positive_scale_unique_firstentryoutput) + (dst_positive_scale_unique_firstentryoutput))) + (((dst_negative_code_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)) * S ((dst_negative_code_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)) + ((dst_negative_scale_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)))) + ((((dst_negative_code_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)) * S ((dst_negative_code_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)) + ((dst_negative_scale_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput))) + (((dst_negative_code_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)) * S ((dst_negative_code_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)) + ((dst_negative_scale_unique_firstentryoutput) + (dst_negative_scale_unique_firstentryoutput)))))) /\ (((((exists ff_h_pvs_unique_firstentryoutputpositive. ff_h_pvs_unique_firstentryoutputpositive + S (dst_positive_unique_firstentryoutput) = S ((S (srs_index_unique_first)) * dst_positive_scale_unique_firstentryoutput)) /\ exists ff_q_pvs_unique_firstentryoutputpositive. dst_positive_code_unique_firstentryoutput = ff_q_pvs_unique_firstentryoutputpositive * S ((S (srs_index_unique_first)) * dst_positive_scale_unique_firstentryoutput) + (dst_positive_unique_firstentryoutput))) /\ (((((exists ff_h_pvs_unique_firstentryoutputnegative. ff_h_pvs_unique_firstentryoutputnegative + S (dst_negative_unique_firstentryoutput) = S ((S (srs_index_unique_first)) * dst_negative_scale_unique_firstentryoutput)) /\ exists ff_q_pvs_unique_firstentryoutputnegative. dst_negative_code_unique_firstentryoutput = ff_q_pvs_unique_firstentryoutputnegative * S ((S (srs_index_unique_first)) * dst_negative_scale_unique_firstentryoutput) + (dst_negative_unique_firstentryoutput))) /\ (exists ge_balance_positive_unique_firstentryoutputvalue ge_balance_negative_unique_firstentryoutputvalue. (((((srs_value_unique_first) = 2 * (ge_balance_positive_unique_firstentryoutputvalue) /\ (ge_balance_negative_unique_firstentryoutputvalue) = 0) \/ exists ge_signed_half_unique_firstentryoutputvaluedecode. (((srs_value_unique_first) = 2 * ge_signed_half_unique_firstentryoutputvaluedecode + 1 /\ (ge_balance_positive_unique_firstentryoutputvalue) = 0) /\ (ge_balance_negative_unique_firstentryoutputvalue) = S ge_signed_half_unique_firstentryoutputvaluedecode))) /\ ((dst_positive_unique_firstentryoutput) + ge_balance_negative_unique_firstentryoutputvalue = (dst_negative_unique_firstentryoutput) + ge_balance_positive_unique_firstentryoutputvalue)))))))))))))))) -> (((exists dst_positive_code_unique_secondsource_table dst_positive_scale_unique_secondsource_table dst_negative_code_unique_secondsource_table dst_negative_scale_unique_secondsource_table. (((F) = (((((dst_positive_code_unique_secondsource_table) + (dst_positive_scale_unique_secondsource_table)) * S ((dst_positive_code_unique_secondsource_table) + (dst_positive_scale_unique_secondsource_table)) + ((dst_positive_scale_unique_secondsource_table) + (dst_positive_scale_unique_secondsource_table))) + (((dst_negative_code_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)) * S ((dst_negative_code_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)) + ((dst_negative_scale_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)))) * S ((((dst_positive_code_unique_secondsource_table) + (dst_positive_scale_unique_secondsource_table)) * S ((dst_positive_code_unique_secondsource_table) + (dst_positive_scale_unique_secondsource_table)) + ((dst_positive_scale_unique_secondsource_table) + (dst_positive_scale_unique_secondsource_table))) + (((dst_negative_code_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)) * S ((dst_negative_code_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)) + ((dst_negative_scale_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)))) + ((((dst_negative_code_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)) * S ((dst_negative_code_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)) + ((dst_negative_scale_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table))) + (((dst_negative_code_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)) * S ((dst_negative_code_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)) + ((dst_negative_scale_unique_secondsource_table) + (dst_negative_scale_unique_secondsource_table)))))) /\ (forall dst_index_unique_secondsource_table. (exists pvs_le_gap_unique_secondsource_tabledomain. pvs_le_gap_unique_secondsource_tabledomain + (dst_index_unique_secondsource_table) = (0)) -> exists dst_positive_unique_secondsource_table dst_negative_unique_secondsource_table dst_value_unique_secondsource_table. ((((exists ff_h_pvs_unique_secondsource_tableentrypositive. ff_h_pvs_unique_secondsource_tableentrypositive + S (dst_positive_unique_secondsource_table) = S ((S (dst_index_unique_secondsource_table)) * dst_positive_scale_unique_secondsource_table)) /\ exists ff_q_pvs_unique_secondsource_tableentrypositive. dst_positive_code_unique_secondsource_table = ff_q_pvs_unique_secondsource_tableentrypositive * S ((S (dst_index_unique_secondsource_table)) * dst_positive_scale_unique_secondsource_table) + (dst_positive_unique_secondsource_table))) /\ (((((exists ff_h_pvs_unique_secondsource_tableentrynegative. ff_h_pvs_unique_secondsource_tableentrynegative + S (dst_negative_unique_secondsource_table) = S ((S (dst_index_unique_secondsource_table)) * dst_negative_scale_unique_secondsource_table)) /\ exists ff_q_pvs_unique_secondsource_tableentrynegative. dst_negative_code_unique_secondsource_table = ff_q_pvs_unique_secondsource_tableentrynegative * S ((S (dst_index_unique_secondsource_table)) * dst_negative_scale_unique_secondsource_table) + (dst_negative_unique_secondsource_table))) /\ (exists ge_balance_positive_unique_secondsource_tableentryvalue ge_balance_negative_unique_secondsource_tableentryvalue. (((((dst_value_unique_secondsource_table) = 2 * (ge_balance_positive_unique_secondsource_tableentryvalue) /\ (ge_balance_negative_unique_secondsource_tableentryvalue) = 0) \/ exists ge_signed_half_unique_secondsource_tableentryvaluedecode. (((dst_value_unique_secondsource_table) = 2 * ge_signed_half_unique_secondsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_unique_secondsource_tableentryvalue) = 0) /\ (ge_balance_negative_unique_secondsource_tableentryvalue) = S ge_signed_half_unique_secondsource_tableentryvaluedecode))) /\ ((dst_positive_unique_secondsource_table) + ge_balance_negative_unique_secondsource_tableentryvalue = (dst_negative_unique_secondsource_table) + ge_balance_positive_unique_secondsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_unique_secondoutput_table dst_positive_scale_unique_secondoutput_table dst_negative_code_unique_secondoutput_table dst_negative_scale_unique_secondoutput_table. (((H) = (((((dst_positive_code_unique_secondoutput_table) + (dst_positive_scale_unique_secondoutput_table)) * S ((dst_positive_code_unique_secondoutput_table) + (dst_positive_scale_unique_secondoutput_table)) + ((dst_positive_scale_unique_secondoutput_table) + (dst_positive_scale_unique_secondoutput_table))) + (((dst_negative_code_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)) * S ((dst_negative_code_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)) + ((dst_negative_scale_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)))) * S ((((dst_positive_code_unique_secondoutput_table) + (dst_positive_scale_unique_secondoutput_table)) * S ((dst_positive_code_unique_secondoutput_table) + (dst_positive_scale_unique_secondoutput_table)) + ((dst_positive_scale_unique_secondoutput_table) + (dst_positive_scale_unique_secondoutput_table))) + (((dst_negative_code_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)) * S ((dst_negative_code_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)) + ((dst_negative_scale_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)))) + ((((dst_negative_code_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)) * S ((dst_negative_code_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)) + ((dst_negative_scale_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table))) + (((dst_negative_code_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)) * S ((dst_negative_code_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)) + ((dst_negative_scale_unique_secondoutput_table) + (dst_negative_scale_unique_secondoutput_table)))))) /\ (forall dst_index_unique_secondoutput_table. (exists pvs_le_gap_unique_secondoutput_tabledomain. pvs_le_gap_unique_secondoutput_tabledomain + (dst_index_unique_secondoutput_table) = (l)) -> exists dst_positive_unique_secondoutput_table dst_negative_unique_secondoutput_table dst_value_unique_secondoutput_table. ((((exists ff_h_pvs_unique_secondoutput_tableentrypositive. ff_h_pvs_unique_secondoutput_tableentrypositive + S (dst_positive_unique_secondoutput_table) = S ((S (dst_index_unique_secondoutput_table)) * dst_positive_scale_unique_secondoutput_table)) /\ exists ff_q_pvs_unique_secondoutput_tableentrypositive. dst_positive_code_unique_secondoutput_table = ff_q_pvs_unique_secondoutput_tableentrypositive * S ((S (dst_index_unique_secondoutput_table)) * dst_positive_scale_unique_secondoutput_table) + (dst_positive_unique_secondoutput_table))) /\ (((((exists ff_h_pvs_unique_secondoutput_tableentrynegative. ff_h_pvs_unique_secondoutput_tableentrynegative + S (dst_negative_unique_secondoutput_table) = S ((S (dst_index_unique_secondoutput_table)) * dst_negative_scale_unique_secondoutput_table)) /\ exists ff_q_pvs_unique_secondoutput_tableentrynegative. dst_negative_code_unique_secondoutput_table = ff_q_pvs_unique_secondoutput_tableentrynegative * S ((S (dst_index_unique_secondoutput_table)) * dst_negative_scale_unique_secondoutput_table) + (dst_negative_unique_secondoutput_table))) /\ (exists ge_balance_positive_unique_secondoutput_tableentryvalue ge_balance_negative_unique_secondoutput_tableentryvalue. (((((dst_value_unique_secondoutput_table) = 2 * (ge_balance_positive_unique_secondoutput_tableentryvalue) /\ (ge_balance_negative_unique_secondoutput_tableentryvalue) = 0) \/ exists ge_signed_half_unique_secondoutput_tableentryvaluedecode. (((dst_value_unique_secondoutput_table) = 2 * ge_signed_half_unique_secondoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_unique_secondoutput_tableentryvalue) = 0) /\ (ge_balance_negative_unique_secondoutput_tableentryvalue) = S ge_signed_half_unique_secondoutput_tableentryvaluedecode))) /\ ((dst_positive_unique_secondoutput_table) + ge_balance_negative_unique_secondoutput_tableentryvalue = (dst_negative_unique_secondoutput_table) + ge_balance_positive_unique_secondoutput_tableentryvalue))))))))) /\ (forall srs_index_unique_second. (exists pvs_gap_unique_secondbound. pvs_gap_unique_secondbound + S (srs_index_unique_second) = (l)) -> exists srs_value_unique_second. (((exists dst_positive_code_unique_secondentrysource dst_positive_scale_unique_secondentrysource dst_negative_code_unique_secondentrysource dst_negative_scale_unique_secondentrysource dst_positive_unique_secondentrysource dst_negative_unique_secondentrysource. (((F) = (((((dst_positive_code_unique_secondentrysource) + (dst_positive_scale_unique_secondentrysource)) * S ((dst_positive_code_unique_secondentrysource) + (dst_positive_scale_unique_secondentrysource)) + ((dst_positive_scale_unique_secondentrysource) + (dst_positive_scale_unique_secondentrysource))) + (((dst_negative_code_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)) * S ((dst_negative_code_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)) + ((dst_negative_scale_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)))) * S ((((dst_positive_code_unique_secondentrysource) + (dst_positive_scale_unique_secondentrysource)) * S ((dst_positive_code_unique_secondentrysource) + (dst_positive_scale_unique_secondentrysource)) + ((dst_positive_scale_unique_secondentrysource) + (dst_positive_scale_unique_secondentrysource))) + (((dst_negative_code_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)) * S ((dst_negative_code_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)) + ((dst_negative_scale_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)))) + ((((dst_negative_code_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)) * S ((dst_negative_code_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)) + ((dst_negative_scale_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource))) + (((dst_negative_code_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)) * S ((dst_negative_code_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)) + ((dst_negative_scale_unique_secondentrysource) + (dst_negative_scale_unique_secondentrysource)))))) /\ (((((exists ff_h_pvs_unique_secondentrysourcepositive. ff_h_pvs_unique_secondentrysourcepositive + S (dst_positive_unique_secondentrysource) = S ((S (((o) + ((s) * (srs_index_unique_second))))) * dst_positive_scale_unique_secondentrysource)) /\ exists ff_q_pvs_unique_secondentrysourcepositive. dst_positive_code_unique_secondentrysource = ff_q_pvs_unique_secondentrysourcepositive * S ((S (((o) + ((s) * (srs_index_unique_second))))) * dst_positive_scale_unique_secondentrysource) + (dst_positive_unique_secondentrysource))) /\ (((((exists ff_h_pvs_unique_secondentrysourcenegative. ff_h_pvs_unique_secondentrysourcenegative + S (dst_negative_unique_secondentrysource) = S ((S (((o) + ((s) * (srs_index_unique_second))))) * dst_negative_scale_unique_secondentrysource)) /\ exists ff_q_pvs_unique_secondentrysourcenegative. dst_negative_code_unique_secondentrysource = ff_q_pvs_unique_secondentrysourcenegative * S ((S (((o) + ((s) * (srs_index_unique_second))))) * dst_negative_scale_unique_secondentrysource) + (dst_negative_unique_secondentrysource))) /\ (exists ge_balance_positive_unique_secondentrysourcevalue ge_balance_negative_unique_secondentrysourcevalue. (((((srs_value_unique_second) = 2 * (ge_balance_positive_unique_secondentrysourcevalue) /\ (ge_balance_negative_unique_secondentrysourcevalue) = 0) \/ exists ge_signed_half_unique_secondentrysourcevaluedecode. (((srs_value_unique_second) = 2 * ge_signed_half_unique_secondentrysourcevaluedecode + 1 /\ (ge_balance_positive_unique_secondentrysourcevalue) = 0) /\ (ge_balance_negative_unique_secondentrysourcevalue) = S ge_signed_half_unique_secondentrysourcevaluedecode))) /\ ((dst_positive_unique_secondentrysource) + ge_balance_negative_unique_secondentrysourcevalue = (dst_negative_unique_secondentrysource) + ge_balance_positive_unique_secondentrysourcevalue))))))))) /\ (exists dst_positive_code_unique_secondentryoutput dst_positive_scale_unique_secondentryoutput dst_negative_code_unique_secondentryoutput dst_negative_scale_unique_secondentryoutput dst_positive_unique_secondentryoutput dst_negative_unique_secondentryoutput. (((H) = (((((dst_positive_code_unique_secondentryoutput) + (dst_positive_scale_unique_secondentryoutput)) * S ((dst_positive_code_unique_secondentryoutput) + (dst_positive_scale_unique_secondentryoutput)) + ((dst_positive_scale_unique_secondentryoutput) + (dst_positive_scale_unique_secondentryoutput))) + (((dst_negative_code_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)) * S ((dst_negative_code_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)) + ((dst_negative_scale_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)))) * S ((((dst_positive_code_unique_secondentryoutput) + (dst_positive_scale_unique_secondentryoutput)) * S ((dst_positive_code_unique_secondentryoutput) + (dst_positive_scale_unique_secondentryoutput)) + ((dst_positive_scale_unique_secondentryoutput) + (dst_positive_scale_unique_secondentryoutput))) + (((dst_negative_code_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)) * S ((dst_negative_code_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)) + ((dst_negative_scale_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)))) + ((((dst_negative_code_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)) * S ((dst_negative_code_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)) + ((dst_negative_scale_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput))) + (((dst_negative_code_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)) * S ((dst_negative_code_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)) + ((dst_negative_scale_unique_secondentryoutput) + (dst_negative_scale_unique_secondentryoutput)))))) /\ (((((exists ff_h_pvs_unique_secondentryoutputpositive. ff_h_pvs_unique_secondentryoutputpositive + S (dst_positive_unique_secondentryoutput) = S ((S (srs_index_unique_second)) * dst_positive_scale_unique_secondentryoutput)) /\ exists ff_q_pvs_unique_secondentryoutputpositive. dst_positive_code_unique_secondentryoutput = ff_q_pvs_unique_secondentryoutputpositive * S ((S (srs_index_unique_second)) * dst_positive_scale_unique_secondentryoutput) + (dst_positive_unique_secondentryoutput))) /\ (((((exists ff_h_pvs_unique_secondentryoutputnegative. ff_h_pvs_unique_secondentryoutputnegative + S (dst_negative_unique_secondentryoutput) = S ((S (srs_index_unique_second)) * dst_negative_scale_unique_secondentryoutput)) /\ exists ff_q_pvs_unique_secondentryoutputnegative. dst_negative_code_unique_secondentryoutput = ff_q_pvs_unique_secondentryoutputnegative * S ((S (srs_index_unique_second)) * dst_negative_scale_unique_secondentryoutput) + (dst_negative_unique_secondentryoutput))) /\ (exists ge_balance_positive_unique_secondentryoutputvalue ge_balance_negative_unique_secondentryoutputvalue. (((((srs_value_unique_second) = 2 * (ge_balance_positive_unique_secondentryoutputvalue) /\ (ge_balance_negative_unique_secondentryoutputvalue) = 0) \/ exists ge_signed_half_unique_secondentryoutputvaluedecode. (((srs_value_unique_second) = 2 * ge_signed_half_unique_secondentryoutputvaluedecode + 1 /\ (ge_balance_positive_unique_secondentryoutputvalue) = 0) /\ (ge_balance_negative_unique_secondentryoutputvalue) = S ge_signed_half_unique_secondentryoutputvaluedecode))) /\ ((dst_positive_unique_secondentryoutput) + ge_balance_negative_unique_secondentryoutputvalue = (dst_negative_unique_secondentryoutput) + ge_balance_positive_unique_secondentryoutputvalue)))))))))))))))) -> (forall dst_index_unique_result dst_first_unique_result dst_second_unique_result. (exists pvs_gap_unique_resultbound. pvs_gap_unique_resultbound + S (dst_index_unique_result) = (l)) -> (exists dst_positive_code_unique_resultfirst dst_positive_scale_unique_resultfirst dst_negative_code_unique_resultfirst dst_negative_scale_unique_resultfirst dst_positive_unique_resultfirst dst_negative_unique_resultfirst. (((G) = (((((dst_positive_code_unique_resultfirst) + (dst_positive_scale_unique_resultfirst)) * S ((dst_positive_code_unique_resultfirst) + (dst_positive_scale_unique_resultfirst)) + ((dst_positive_scale_unique_resultfirst) + (dst_positive_scale_unique_resultfirst))) + (((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) * S ((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) + ((dst_negative_scale_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)))) * S ((((dst_positive_code_unique_resultfirst) + (dst_positive_scale_unique_resultfirst)) * S ((dst_positive_code_unique_resultfirst) + (dst_positive_scale_unique_resultfirst)) + ((dst_positive_scale_unique_resultfirst) + (dst_positive_scale_unique_resultfirst))) + (((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) * S ((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) + ((dst_negative_scale_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)))) + ((((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) * S ((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) + ((dst_negative_scale_unique_resultfirst) + (dst_negative_scale_unique_resultfirst))) + (((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) * S ((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) + ((dst_negative_scale_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)))))) /\ (((((exists ff_h_pvs_unique_resultfirstpositive. ff_h_pvs_unique_resultfirstpositive + S (dst_positive_unique_resultfirst) = S ((S (dst_index_unique_result)) * dst_positive_scale_unique_resultfirst)) /\ exists ff_q_pvs_unique_resultfirstpositive. dst_positive_code_unique_resultfirst = ff_q_pvs_unique_resultfirstpositive * S ((S (dst_index_unique_result)) * dst_positive_scale_unique_resultfirst) + (dst_positive_unique_resultfirst))) /\ (((((exists ff_h_pvs_unique_resultfirstnegative. ff_h_pvs_unique_resultfirstnegative + S (dst_negative_unique_resultfirst) = S ((S (dst_index_unique_result)) * dst_negative_scale_unique_resultfirst)) /\ exists ff_q_pvs_unique_resultfirstnegative. dst_negative_code_unique_resultfirst = ff_q_pvs_unique_resultfirstnegative * S ((S (dst_index_unique_result)) * dst_negative_scale_unique_resultfirst) + (dst_negative_unique_resultfirst))) /\ (exists ge_balance_positive_unique_resultfirstvalue ge_balance_negative_unique_resultfirstvalue. (((((dst_first_unique_result) = 2 * (ge_balance_positive_unique_resultfirstvalue) /\ (ge_balance_negative_unique_resultfirstvalue) = 0) \/ exists ge_signed_half_unique_resultfirstvaluedecode. (((dst_first_unique_result) = 2 * ge_signed_half_unique_resultfirstvaluedecode + 1 /\ (ge_balance_positive_unique_resultfirstvalue) = 0) /\ (ge_balance_negative_unique_resultfirstvalue) = S ge_signed_half_unique_resultfirstvaluedecode))) /\ ((dst_positive_unique_resultfirst) + ge_balance_negative_unique_resultfirstvalue = (dst_negative_unique_resultfirst) + ge_balance_positive_unique_resultfirstvalue))))))))) -> (exists dst_positive_code_unique_resultsecond dst_positive_scale_unique_resultsecond dst_negative_code_unique_resultsecond dst_negative_scale_unique_resultsecond dst_positive_unique_resultsecond dst_negative_unique_resultsecond. (((H) = (((((dst_positive_code_unique_resultsecond) + (dst_positive_scale_unique_resultsecond)) * S ((dst_positive_code_unique_resultsecond) + (dst_positive_scale_unique_resultsecond)) + ((dst_positive_scale_unique_resultsecond) + (dst_positive_scale_unique_resultsecond))) + (((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) * S ((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) + ((dst_negative_scale_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)))) * S ((((dst_positive_code_unique_resultsecond) + (dst_positive_scale_unique_resultsecond)) * S ((dst_positive_code_unique_resultsecond) + (dst_positive_scale_unique_resultsecond)) + ((dst_positive_scale_unique_resultsecond) + (dst_positive_scale_unique_resultsecond))) + (((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) * S ((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) + ((dst_negative_scale_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)))) + ((((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) * S ((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) + ((dst_negative_scale_unique_resultsecond) + (dst_negative_scale_unique_resultsecond))) + (((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) * S ((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) + ((dst_negative_scale_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)))))) /\ (((((exists ff_h_pvs_unique_resultsecondpositive. ff_h_pvs_unique_resultsecondpositive + S (dst_positive_unique_resultsecond) = S ((S (dst_index_unique_result)) * dst_positive_scale_unique_resultsecond)) /\ exists ff_q_pvs_unique_resultsecondpositive. dst_positive_code_unique_resultsecond = ff_q_pvs_unique_resultsecondpositive * S ((S (dst_index_unique_result)) * dst_positive_scale_unique_resultsecond) + (dst_positive_unique_resultsecond))) /\ (((((exists ff_h_pvs_unique_resultsecondnegative. ff_h_pvs_unique_resultsecondnegative + S (dst_negative_unique_resultsecond) = S ((S (dst_index_unique_result)) * dst_negative_scale_unique_resultsecond)) /\ exists ff_q_pvs_unique_resultsecondnegative. dst_negative_code_unique_resultsecond = ff_q_pvs_unique_resultsecondnegative * S ((S (dst_index_unique_result)) * dst_negative_scale_unique_resultsecond) + (dst_negative_unique_resultsecond))) /\ (exists ge_balance_positive_unique_resultsecondvalue ge_balance_negative_unique_resultsecondvalue. (((((dst_second_unique_result) = 2 * (ge_balance_positive_unique_resultsecondvalue) /\ (ge_balance_negative_unique_resultsecondvalue) = 0) \/ exists ge_signed_half_unique_resultsecondvaluedecode. (((dst_second_unique_result) = 2 * ge_signed_half_unique_resultsecondvaluedecode + 1 /\ (ge_balance_positive_unique_resultsecondvalue) = 0) /\ (ge_balance_negative_unique_resultsecondvalue) = S ge_signed_half_unique_resultsecondvaluedecode))) /\ ((dst_positive_unique_resultsecond) + ge_balance_negative_unique_resultsecondvalue = (dst_negative_unique_resultsecond) + ge_balance_positive_unique_resultsecondvalue))))))))) -> dst_first_unique_result = dst_second_unique_result)