signed_rectangular_slice_exists_extensionally_unique

forall F o s l. (exists dst_positive_code_exists_unique_input dst_positive_scale_exists_unique_input dst_negative_code_exists_unique_input dst_negative_scale_exists_unique_input. (((F) = (((((dst_positive_code_exists_unique_input) + (dst_positive_scale_exists_unique_input)) * S ((dst_positive_code_exists_unique_input) + (dst_positive_scale_exists_unique_input)) + ((dst_positive_scale_exists_unique_input) + (dst_positive_scale_exists_unique_input))) + (((dst_negative_code_exists_unique_input) + (dst_negative_scale_exists_unique_input)) * S ((dst_negative_code_exists_unique_input) + (dst_negative_scale_exists_unique_input)) + ((dst_negative_scale_exists_unique_input) + (dst_negative_scale_exists_unique_input)))) * S ((((dst_positive_code_exists_unique_input) + (dst_positive_scale_exists_unique_input)) * S ((dst_positive_code_exists_unique_input) + (dst_positive_scale_exists_unique_input)) + ((dst_positive_scale_exists_unique_input) + (dst_positive_scale_exists_unique_input))) + (((dst_negative_code_exists_unique_input) + (dst_negative_scale_exists_unique_input)) * S ((dst_negative_code_exists_unique_input) + (dst_negative_scale_exists_unique_input)) + ((dst_negative_scale_exists_unique_input) + (dst_negative_scale_exists_unique_input)))) + ((((dst_negative_code_exists_unique_input) + (dst_negative_scale_exists_unique_input)) * S ((dst_negative_code_exists_unique_input) + (dst_negative_scale_exists_unique_input)) + ((dst_negative_scale_exists_unique_input) + (dst_negative_scale_exists_unique_input))) + (((dst_negative_code_exists_unique_input) + (dst_negative_scale_exists_unique_input)) * S ((dst_negative_code_exists_unique_input) + (dst_negative_scale_exists_unique_input)) + ((dst_negative_scale_exists_unique_input) + (dst_negative_scale_exists_unique_input)))))) /\ (forall dst_index_exists_unique_input. (exists pvs_le_gap_exists_unique_inputdomain. pvs_le_gap_exists_unique_inputdomain + (dst_index_exists_unique_input) = (0)) -> exists dst_positive_exists_unique_input dst_negative_exists_unique_input dst_value_exists_unique_input. ((((exists ff_h_pvs_exists_unique_inputentrypositive. ff_h_pvs_exists_unique_inputentrypositive + S (dst_positive_exists_unique_input) = S ((S (dst_index_exists_unique_input)) * dst_positive_scale_exists_unique_input)) /\ exists ff_q_pvs_exists_unique_inputentrypositive. dst_positive_code_exists_unique_input = ff_q_pvs_exists_unique_inputentrypositive * S ((S (dst_index_exists_unique_input)) * dst_positive_scale_exists_unique_input) + (dst_positive_exists_unique_input))) /\ (((((exists ff_h_pvs_exists_unique_inputentrynegative. ff_h_pvs_exists_unique_inputentrynegative + S (dst_negative_exists_unique_input) = S ((S (dst_index_exists_unique_input)) * dst_negative_scale_exists_unique_input)) /\ exists ff_q_pvs_exists_unique_inputentrynegative. dst_negative_code_exists_unique_input = ff_q_pvs_exists_unique_inputentrynegative * S ((S (dst_index_exists_unique_input)) * dst_negative_scale_exists_unique_input) + (dst_negative_exists_unique_input))) /\ (exists ge_balance_positive_exists_unique_inputentryvalue ge_balance_negative_exists_unique_inputentryvalue. (((((dst_value_exists_unique_input) = 2 * (ge_balance_positive_exists_unique_inputentryvalue) /\ (ge_balance_negative_exists_unique_inputentryvalue) = 0) \/ exists ge_signed_half_exists_unique_inputentryvaluedecode. (((dst_value_exists_unique_input) = 2 * ge_signed_half_exists_unique_inputentryvaluedecode + 1 /\ (ge_balance_positive_exists_unique_inputentryvalue) = 0) /\ (ge_balance_negative_exists_unique_inputentryvalue) = S ge_signed_half_exists_unique_inputentryvaluedecode))) /\ ((dst_positive_exists_unique_input) + ge_balance_negative_exists_unique_inputentryvalue = (dst_negative_exists_unique_input) + ge_balance_positive_exists_unique_inputentryvalue))))))))) -> exists G. ((((exists dst_positive_code_exists_unique_resultsource_table dst_positive_scale_exists_unique_resultsource_table dst_negative_code_exists_unique_resultsource_table dst_negative_scale_exists_unique_resultsource_table. (((F) = (((((dst_positive_code_exists_unique_resultsource_table) + (dst_positive_scale_exists_unique_resultsource_table)) * S ((dst_positive_code_exists_unique_resultsource_table) + (dst_positive_scale_exists_unique_resultsource_table)) + ((dst_positive_scale_exists_unique_resultsource_table) + (dst_positive_scale_exists_unique_resultsource_table))) + (((dst_negative_code_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)) * S ((dst_negative_code_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)) + ((dst_negative_scale_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)))) * S ((((dst_positive_code_exists_unique_resultsource_table) + (dst_positive_scale_exists_unique_resultsource_table)) * S ((dst_positive_code_exists_unique_resultsource_table) + (dst_positive_scale_exists_unique_resultsource_table)) + ((dst_positive_scale_exists_unique_resultsource_table) + (dst_positive_scale_exists_unique_resultsource_table))) + (((dst_negative_code_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)) * S ((dst_negative_code_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)) + ((dst_negative_scale_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)))) + ((((dst_negative_code_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)) * S ((dst_negative_code_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)) + ((dst_negative_scale_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table))) + (((dst_negative_code_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)) * S ((dst_negative_code_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)) + ((dst_negative_scale_exists_unique_resultsource_table) + (dst_negative_scale_exists_unique_resultsource_table)))))) /\ (forall dst_index_exists_unique_resultsource_table. (exists pvs_le_gap_exists_unique_resultsource_tabledomain. pvs_le_gap_exists_unique_resultsource_tabledomain + (dst_index_exists_unique_resultsource_table) = (0)) -> exists dst_positive_exists_unique_resultsource_table dst_negative_exists_unique_resultsource_table dst_value_exists_unique_resultsource_table. ((((exists ff_h_pvs_exists_unique_resultsource_tableentrypositive. ff_h_pvs_exists_unique_resultsource_tableentrypositive + S (dst_positive_exists_unique_resultsource_table) = S ((S (dst_index_exists_unique_resultsource_table)) * dst_positive_scale_exists_unique_resultsource_table)) /\ exists ff_q_pvs_exists_unique_resultsource_tableentrypositive. dst_positive_code_exists_unique_resultsource_table = ff_q_pvs_exists_unique_resultsource_tableentrypositive * S ((S (dst_index_exists_unique_resultsource_table)) * dst_positive_scale_exists_unique_resultsource_table) + (dst_positive_exists_unique_resultsource_table))) /\ (((((exists ff_h_pvs_exists_unique_resultsource_tableentrynegative. ff_h_pvs_exists_unique_resultsource_tableentrynegative + S (dst_negative_exists_unique_resultsource_table) = S ((S (dst_index_exists_unique_resultsource_table)) * dst_negative_scale_exists_unique_resultsource_table)) /\ exists ff_q_pvs_exists_unique_resultsource_tableentrynegative. dst_negative_code_exists_unique_resultsource_table = ff_q_pvs_exists_unique_resultsource_tableentrynegative * S ((S (dst_index_exists_unique_resultsource_table)) * dst_negative_scale_exists_unique_resultsource_table) + (dst_negative_exists_unique_resultsource_table))) /\ (exists ge_balance_positive_exists_unique_resultsource_tableentryvalue ge_balance_negative_exists_unique_resultsource_tableentryvalue. (((((dst_value_exists_unique_resultsource_table) = 2 * (ge_balance_positive_exists_unique_resultsource_tableentryvalue) /\ (ge_balance_negative_exists_unique_resultsource_tableentryvalue) = 0) \/ exists ge_signed_half_exists_unique_resultsource_tableentryvaluedecode. (((dst_value_exists_unique_resultsource_table) = 2 * ge_signed_half_exists_unique_resultsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_unique_resultsource_tableentryvalue) = 0) /\ (ge_balance_negative_exists_unique_resultsource_tableentryvalue) = S ge_signed_half_exists_unique_resultsource_tableentryvaluedecode))) /\ ((dst_positive_exists_unique_resultsource_table) + ge_balance_negative_exists_unique_resultsource_tableentryvalue = (dst_negative_exists_unique_resultsource_table) + ge_balance_positive_exists_unique_resultsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_exists_unique_resultoutput_table dst_positive_scale_exists_unique_resultoutput_table dst_negative_code_exists_unique_resultoutput_table dst_negative_scale_exists_unique_resultoutput_table. (((G) = (((((dst_positive_code_exists_unique_resultoutput_table) + (dst_positive_scale_exists_unique_resultoutput_table)) * S ((dst_positive_code_exists_unique_resultoutput_table) + (dst_positive_scale_exists_unique_resultoutput_table)) + ((dst_positive_scale_exists_unique_resultoutput_table) + (dst_positive_scale_exists_unique_resultoutput_table))) + (((dst_negative_code_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)) * S ((dst_negative_code_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)) + ((dst_negative_scale_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)))) * S ((((dst_positive_code_exists_unique_resultoutput_table) + (dst_positive_scale_exists_unique_resultoutput_table)) * S ((dst_positive_code_exists_unique_resultoutput_table) + (dst_positive_scale_exists_unique_resultoutput_table)) + ((dst_positive_scale_exists_unique_resultoutput_table) + (dst_positive_scale_exists_unique_resultoutput_table))) + (((dst_negative_code_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)) * S ((dst_negative_code_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)) + ((dst_negative_scale_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)))) + ((((dst_negative_code_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)) * S ((dst_negative_code_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)) + ((dst_negative_scale_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table))) + (((dst_negative_code_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)) * S ((dst_negative_code_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)) + ((dst_negative_scale_exists_unique_resultoutput_table) + (dst_negative_scale_exists_unique_resultoutput_table)))))) /\ (forall dst_index_exists_unique_resultoutput_table. (exists pvs_le_gap_exists_unique_resultoutput_tabledomain. pvs_le_gap_exists_unique_resultoutput_tabledomain + (dst_index_exists_unique_resultoutput_table) = (l)) -> exists dst_positive_exists_unique_resultoutput_table dst_negative_exists_unique_resultoutput_table dst_value_exists_unique_resultoutput_table. ((((exists ff_h_pvs_exists_unique_resultoutput_tableentrypositive. ff_h_pvs_exists_unique_resultoutput_tableentrypositive + S (dst_positive_exists_unique_resultoutput_table) = S ((S (dst_index_exists_unique_resultoutput_table)) * dst_positive_scale_exists_unique_resultoutput_table)) /\ exists ff_q_pvs_exists_unique_resultoutput_tableentrypositive. dst_positive_code_exists_unique_resultoutput_table = ff_q_pvs_exists_unique_resultoutput_tableentrypositive * S ((S (dst_index_exists_unique_resultoutput_table)) * dst_positive_scale_exists_unique_resultoutput_table) + (dst_positive_exists_unique_resultoutput_table))) /\ (((((exists ff_h_pvs_exists_unique_resultoutput_tableentrynegative. ff_h_pvs_exists_unique_resultoutput_tableentrynegative + S (dst_negative_exists_unique_resultoutput_table) = S ((S (dst_index_exists_unique_resultoutput_table)) * dst_negative_scale_exists_unique_resultoutput_table)) /\ exists ff_q_pvs_exists_unique_resultoutput_tableentrynegative. dst_negative_code_exists_unique_resultoutput_table = ff_q_pvs_exists_unique_resultoutput_tableentrynegative * S ((S (dst_index_exists_unique_resultoutput_table)) * dst_negative_scale_exists_unique_resultoutput_table) + (dst_negative_exists_unique_resultoutput_table))) /\ (exists ge_balance_positive_exists_unique_resultoutput_tableentryvalue ge_balance_negative_exists_unique_resultoutput_tableentryvalue. (((((dst_value_exists_unique_resultoutput_table) = 2 * (ge_balance_positive_exists_unique_resultoutput_tableentryvalue) /\ (ge_balance_negative_exists_unique_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_exists_unique_resultoutput_tableentryvaluedecode. (((dst_value_exists_unique_resultoutput_table) = 2 * ge_signed_half_exists_unique_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_unique_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_exists_unique_resultoutput_tableentryvalue) = S ge_signed_half_exists_unique_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_exists_unique_resultoutput_table) + ge_balance_negative_exists_unique_resultoutput_tableentryvalue = (dst_negative_exists_unique_resultoutput_table) + ge_balance_positive_exists_unique_resultoutput_tableentryvalue))))))))) /\ (forall srs_index_exists_unique_result. (exists pvs_gap_exists_unique_resultbound. pvs_gap_exists_unique_resultbound + S (srs_index_exists_unique_result) = (l)) -> exists srs_value_exists_unique_result. (((exists dst_positive_code_exists_unique_resultentrysource dst_positive_scale_exists_unique_resultentrysource dst_negative_code_exists_unique_resultentrysource dst_negative_scale_exists_unique_resultentrysource dst_positive_exists_unique_resultentrysource dst_negative_exists_unique_resultentrysource. (((F) = (((((dst_positive_code_exists_unique_resultentrysource) + (dst_positive_scale_exists_unique_resultentrysource)) * S ((dst_positive_code_exists_unique_resultentrysource) + (dst_positive_scale_exists_unique_resultentrysource)) + ((dst_positive_scale_exists_unique_resultentrysource) + (dst_positive_scale_exists_unique_resultentrysource))) + (((dst_negative_code_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)) * S ((dst_negative_code_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)) + ((dst_negative_scale_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)))) * S ((((dst_positive_code_exists_unique_resultentrysource) + (dst_positive_scale_exists_unique_resultentrysource)) * S ((dst_positive_code_exists_unique_resultentrysource) + (dst_positive_scale_exists_unique_resultentrysource)) + ((dst_positive_scale_exists_unique_resultentrysource) + (dst_positive_scale_exists_unique_resultentrysource))) + (((dst_negative_code_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)) * S ((dst_negative_code_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)) + ((dst_negative_scale_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)))) + ((((dst_negative_code_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)) * S ((dst_negative_code_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)) + ((dst_negative_scale_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource))) + (((dst_negative_code_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)) * S ((dst_negative_code_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)) + ((dst_negative_scale_exists_unique_resultentrysource) + (dst_negative_scale_exists_unique_resultentrysource)))))) /\ (((((exists ff_h_pvs_exists_unique_resultentrysourcepositive. ff_h_pvs_exists_unique_resultentrysourcepositive + S (dst_positive_exists_unique_resultentrysource) = S ((S (((o) + ((s) * (srs_index_exists_unique_result))))) * dst_positive_scale_exists_unique_resultentrysource)) /\ exists ff_q_pvs_exists_unique_resultentrysourcepositive. dst_positive_code_exists_unique_resultentrysource = ff_q_pvs_exists_unique_resultentrysourcepositive * S ((S (((o) + ((s) * (srs_index_exists_unique_result))))) * dst_positive_scale_exists_unique_resultentrysource) + (dst_positive_exists_unique_resultentrysource))) /\ (((((exists ff_h_pvs_exists_unique_resultentrysourcenegative. ff_h_pvs_exists_unique_resultentrysourcenegative + S (dst_negative_exists_unique_resultentrysource) = S ((S (((o) + ((s) * (srs_index_exists_unique_result))))) * dst_negative_scale_exists_unique_resultentrysource)) /\ exists ff_q_pvs_exists_unique_resultentrysourcenegative. dst_negative_code_exists_unique_resultentrysource = ff_q_pvs_exists_unique_resultentrysourcenegative * S ((S (((o) + ((s) * (srs_index_exists_unique_result))))) * dst_negative_scale_exists_unique_resultentrysource) + (dst_negative_exists_unique_resultentrysource))) /\ (exists ge_balance_positive_exists_unique_resultentrysourcevalue ge_balance_negative_exists_unique_resultentrysourcevalue. (((((srs_value_exists_unique_result) = 2 * (ge_balance_positive_exists_unique_resultentrysourcevalue) /\ (ge_balance_negative_exists_unique_resultentrysourcevalue) = 0) \/ exists ge_signed_half_exists_unique_resultentrysourcevaluedecode. (((srs_value_exists_unique_result) = 2 * ge_signed_half_exists_unique_resultentrysourcevaluedecode + 1 /\ (ge_balance_positive_exists_unique_resultentrysourcevalue) = 0) /\ (ge_balance_negative_exists_unique_resultentrysourcevalue) = S ge_signed_half_exists_unique_resultentrysourcevaluedecode))) /\ ((dst_positive_exists_unique_resultentrysource) + ge_balance_negative_exists_unique_resultentrysourcevalue = (dst_negative_exists_unique_resultentrysource) + ge_balance_positive_exists_unique_resultentrysourcevalue))))))))) /\ (exists dst_positive_code_exists_unique_resultentryoutput dst_positive_scale_exists_unique_resultentryoutput dst_negative_code_exists_unique_resultentryoutput dst_negative_scale_exists_unique_resultentryoutput dst_positive_exists_unique_resultentryoutput dst_negative_exists_unique_resultentryoutput. (((G) = (((((dst_positive_code_exists_unique_resultentryoutput) + (dst_positive_scale_exists_unique_resultentryoutput)) * S ((dst_positive_code_exists_unique_resultentryoutput) + (dst_positive_scale_exists_unique_resultentryoutput)) + ((dst_positive_scale_exists_unique_resultentryoutput) + (dst_positive_scale_exists_unique_resultentryoutput))) + (((dst_negative_code_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)) * S ((dst_negative_code_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)) + ((dst_negative_scale_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)))) * S ((((dst_positive_code_exists_unique_resultentryoutput) + (dst_positive_scale_exists_unique_resultentryoutput)) * S ((dst_positive_code_exists_unique_resultentryoutput) + (dst_positive_scale_exists_unique_resultentryoutput)) + ((dst_positive_scale_exists_unique_resultentryoutput) + (dst_positive_scale_exists_unique_resultentryoutput))) + (((dst_negative_code_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)) * S ((dst_negative_code_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)) + ((dst_negative_scale_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)))) + ((((dst_negative_code_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)) * S ((dst_negative_code_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)) + ((dst_negative_scale_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput))) + (((dst_negative_code_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)) * S ((dst_negative_code_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)) + ((dst_negative_scale_exists_unique_resultentryoutput) + (dst_negative_scale_exists_unique_resultentryoutput)))))) /\ (((((exists ff_h_pvs_exists_unique_resultentryoutputpositive. ff_h_pvs_exists_unique_resultentryoutputpositive + S (dst_positive_exists_unique_resultentryoutput) = S ((S (srs_index_exists_unique_result)) * dst_positive_scale_exists_unique_resultentryoutput)) /\ exists ff_q_pvs_exists_unique_resultentryoutputpositive. dst_positive_code_exists_unique_resultentryoutput = ff_q_pvs_exists_unique_resultentryoutputpositive * S ((S (srs_index_exists_unique_result)) * dst_positive_scale_exists_unique_resultentryoutput) + (dst_positive_exists_unique_resultentryoutput))) /\ (((((exists ff_h_pvs_exists_unique_resultentryoutputnegative. ff_h_pvs_exists_unique_resultentryoutputnegative + S (dst_negative_exists_unique_resultentryoutput) = S ((S (srs_index_exists_unique_result)) * dst_negative_scale_exists_unique_resultentryoutput)) /\ exists ff_q_pvs_exists_unique_resultentryoutputnegative. dst_negative_code_exists_unique_resultentryoutput = ff_q_pvs_exists_unique_resultentryoutputnegative * S ((S (srs_index_exists_unique_result)) * dst_negative_scale_exists_unique_resultentryoutput) + (dst_negative_exists_unique_resultentryoutput))) /\ (exists ge_balance_positive_exists_unique_resultentryoutputvalue ge_balance_negative_exists_unique_resultentryoutputvalue. (((((srs_value_exists_unique_result) = 2 * (ge_balance_positive_exists_unique_resultentryoutputvalue) /\ (ge_balance_negative_exists_unique_resultentryoutputvalue) = 0) \/ exists ge_signed_half_exists_unique_resultentryoutputvaluedecode. (((srs_value_exists_unique_result) = 2 * ge_signed_half_exists_unique_resultentryoutputvaluedecode + 1 /\ (ge_balance_positive_exists_unique_resultentryoutputvalue) = 0) /\ (ge_balance_negative_exists_unique_resultentryoutputvalue) = S ge_signed_half_exists_unique_resultentryoutputvaluedecode))) /\ ((dst_positive_exists_unique_resultentryoutput) + ge_balance_negative_exists_unique_resultentryoutputvalue = (dst_negative_exists_unique_resultentryoutput) + ge_balance_positive_exists_unique_resultentryoutputvalue)))))))))))))))) /\ (forall H. (((exists dst_positive_code_exists_unique_othersource_table dst_positive_scale_exists_unique_othersource_table dst_negative_code_exists_unique_othersource_table dst_negative_scale_exists_unique_othersource_table. (((F) = (((((dst_positive_code_exists_unique_othersource_table) + (dst_positive_scale_exists_unique_othersource_table)) * S ((dst_positive_code_exists_unique_othersource_table) + (dst_positive_scale_exists_unique_othersource_table)) + ((dst_positive_scale_exists_unique_othersource_table) + (dst_positive_scale_exists_unique_othersource_table))) + (((dst_negative_code_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)) * S ((dst_negative_code_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)) + ((dst_negative_scale_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)))) * S ((((dst_positive_code_exists_unique_othersource_table) + (dst_positive_scale_exists_unique_othersource_table)) * S ((dst_positive_code_exists_unique_othersource_table) + (dst_positive_scale_exists_unique_othersource_table)) + ((dst_positive_scale_exists_unique_othersource_table) + (dst_positive_scale_exists_unique_othersource_table))) + (((dst_negative_code_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)) * S ((dst_negative_code_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)) + ((dst_negative_scale_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)))) + ((((dst_negative_code_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)) * S ((dst_negative_code_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)) + ((dst_negative_scale_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table))) + (((dst_negative_code_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)) * S ((dst_negative_code_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)) + ((dst_negative_scale_exists_unique_othersource_table) + (dst_negative_scale_exists_unique_othersource_table)))))) /\ (forall dst_index_exists_unique_othersource_table. (exists pvs_le_gap_exists_unique_othersource_tabledomain. pvs_le_gap_exists_unique_othersource_tabledomain + (dst_index_exists_unique_othersource_table) = (0)) -> exists dst_positive_exists_unique_othersource_table dst_negative_exists_unique_othersource_table dst_value_exists_unique_othersource_table. ((((exists ff_h_pvs_exists_unique_othersource_tableentrypositive. ff_h_pvs_exists_unique_othersource_tableentrypositive + S (dst_positive_exists_unique_othersource_table) = S ((S (dst_index_exists_unique_othersource_table)) * dst_positive_scale_exists_unique_othersource_table)) /\ exists ff_q_pvs_exists_unique_othersource_tableentrypositive. dst_positive_code_exists_unique_othersource_table = ff_q_pvs_exists_unique_othersource_tableentrypositive * S ((S (dst_index_exists_unique_othersource_table)) * dst_positive_scale_exists_unique_othersource_table) + (dst_positive_exists_unique_othersource_table))) /\ (((((exists ff_h_pvs_exists_unique_othersource_tableentrynegative. ff_h_pvs_exists_unique_othersource_tableentrynegative + S (dst_negative_exists_unique_othersource_table) = S ((S (dst_index_exists_unique_othersource_table)) * dst_negative_scale_exists_unique_othersource_table)) /\ exists ff_q_pvs_exists_unique_othersource_tableentrynegative. dst_negative_code_exists_unique_othersource_table = ff_q_pvs_exists_unique_othersource_tableentrynegative * S ((S (dst_index_exists_unique_othersource_table)) * dst_negative_scale_exists_unique_othersource_table) + (dst_negative_exists_unique_othersource_table))) /\ (exists ge_balance_positive_exists_unique_othersource_tableentryvalue ge_balance_negative_exists_unique_othersource_tableentryvalue. (((((dst_value_exists_unique_othersource_table) = 2 * (ge_balance_positive_exists_unique_othersource_tableentryvalue) /\ (ge_balance_negative_exists_unique_othersource_tableentryvalue) = 0) \/ exists ge_signed_half_exists_unique_othersource_tableentryvaluedecode. (((dst_value_exists_unique_othersource_table) = 2 * ge_signed_half_exists_unique_othersource_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_unique_othersource_tableentryvalue) = 0) /\ (ge_balance_negative_exists_unique_othersource_tableentryvalue) = S ge_signed_half_exists_unique_othersource_tableentryvaluedecode))) /\ ((dst_positive_exists_unique_othersource_table) + ge_balance_negative_exists_unique_othersource_tableentryvalue = (dst_negative_exists_unique_othersource_table) + ge_balance_positive_exists_unique_othersource_tableentryvalue))))))))) /\ (((exists dst_positive_code_exists_unique_otheroutput_table dst_positive_scale_exists_unique_otheroutput_table dst_negative_code_exists_unique_otheroutput_table dst_negative_scale_exists_unique_otheroutput_table. (((H) = (((((dst_positive_code_exists_unique_otheroutput_table) + (dst_positive_scale_exists_unique_otheroutput_table)) * S ((dst_positive_code_exists_unique_otheroutput_table) + (dst_positive_scale_exists_unique_otheroutput_table)) + ((dst_positive_scale_exists_unique_otheroutput_table) + (dst_positive_scale_exists_unique_otheroutput_table))) + (((dst_negative_code_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)) * S ((dst_negative_code_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)) + ((dst_negative_scale_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)))) * S ((((dst_positive_code_exists_unique_otheroutput_table) + (dst_positive_scale_exists_unique_otheroutput_table)) * S ((dst_positive_code_exists_unique_otheroutput_table) + (dst_positive_scale_exists_unique_otheroutput_table)) + ((dst_positive_scale_exists_unique_otheroutput_table) + (dst_positive_scale_exists_unique_otheroutput_table))) + (((dst_negative_code_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)) * S ((dst_negative_code_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)) + ((dst_negative_scale_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)))) + ((((dst_negative_code_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)) * S ((dst_negative_code_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)) + ((dst_negative_scale_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table))) + (((dst_negative_code_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)) * S ((dst_negative_code_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)) + ((dst_negative_scale_exists_unique_otheroutput_table) + (dst_negative_scale_exists_unique_otheroutput_table)))))) /\ (forall dst_index_exists_unique_otheroutput_table. (exists pvs_le_gap_exists_unique_otheroutput_tabledomain. pvs_le_gap_exists_unique_otheroutput_tabledomain + (dst_index_exists_unique_otheroutput_table) = (l)) -> exists dst_positive_exists_unique_otheroutput_table dst_negative_exists_unique_otheroutput_table dst_value_exists_unique_otheroutput_table. ((((exists ff_h_pvs_exists_unique_otheroutput_tableentrypositive. ff_h_pvs_exists_unique_otheroutput_tableentrypositive + S (dst_positive_exists_unique_otheroutput_table) = S ((S (dst_index_exists_unique_otheroutput_table)) * dst_positive_scale_exists_unique_otheroutput_table)) /\ exists ff_q_pvs_exists_unique_otheroutput_tableentrypositive. dst_positive_code_exists_unique_otheroutput_table = ff_q_pvs_exists_unique_otheroutput_tableentrypositive * S ((S (dst_index_exists_unique_otheroutput_table)) * dst_positive_scale_exists_unique_otheroutput_table) + (dst_positive_exists_unique_otheroutput_table))) /\ (((((exists ff_h_pvs_exists_unique_otheroutput_tableentrynegative. ff_h_pvs_exists_unique_otheroutput_tableentrynegative + S (dst_negative_exists_unique_otheroutput_table) = S ((S (dst_index_exists_unique_otheroutput_table)) * dst_negative_scale_exists_unique_otheroutput_table)) /\ exists ff_q_pvs_exists_unique_otheroutput_tableentrynegative. dst_negative_code_exists_unique_otheroutput_table = ff_q_pvs_exists_unique_otheroutput_tableentrynegative * S ((S (dst_index_exists_unique_otheroutput_table)) * dst_negative_scale_exists_unique_otheroutput_table) + (dst_negative_exists_unique_otheroutput_table))) /\ (exists ge_balance_positive_exists_unique_otheroutput_tableentryvalue ge_balance_negative_exists_unique_otheroutput_tableentryvalue. (((((dst_value_exists_unique_otheroutput_table) = 2 * (ge_balance_positive_exists_unique_otheroutput_tableentryvalue) /\ (ge_balance_negative_exists_unique_otheroutput_tableentryvalue) = 0) \/ exists ge_signed_half_exists_unique_otheroutput_tableentryvaluedecode. (((dst_value_exists_unique_otheroutput_table) = 2 * ge_signed_half_exists_unique_otheroutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_unique_otheroutput_tableentryvalue) = 0) /\ (ge_balance_negative_exists_unique_otheroutput_tableentryvalue) = S ge_signed_half_exists_unique_otheroutput_tableentryvaluedecode))) /\ ((dst_positive_exists_unique_otheroutput_table) + ge_balance_negative_exists_unique_otheroutput_tableentryvalue = (dst_negative_exists_unique_otheroutput_table) + ge_balance_positive_exists_unique_otheroutput_tableentryvalue))))))))) /\ (forall srs_index_exists_unique_other. (exists pvs_gap_exists_unique_otherbound. pvs_gap_exists_unique_otherbound + S (srs_index_exists_unique_other) = (l)) -> exists srs_value_exists_unique_other. (((exists dst_positive_code_exists_unique_otherentrysource dst_positive_scale_exists_unique_otherentrysource dst_negative_code_exists_unique_otherentrysource dst_negative_scale_exists_unique_otherentrysource dst_positive_exists_unique_otherentrysource dst_negative_exists_unique_otherentrysource. (((F) = (((((dst_positive_code_exists_unique_otherentrysource) + (dst_positive_scale_exists_unique_otherentrysource)) * S ((dst_positive_code_exists_unique_otherentrysource) + (dst_positive_scale_exists_unique_otherentrysource)) + ((dst_positive_scale_exists_unique_otherentrysource) + (dst_positive_scale_exists_unique_otherentrysource))) + (((dst_negative_code_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)) * S ((dst_negative_code_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)) + ((dst_negative_scale_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)))) * S ((((dst_positive_code_exists_unique_otherentrysource) + (dst_positive_scale_exists_unique_otherentrysource)) * S ((dst_positive_code_exists_unique_otherentrysource) + (dst_positive_scale_exists_unique_otherentrysource)) + ((dst_positive_scale_exists_unique_otherentrysource) + (dst_positive_scale_exists_unique_otherentrysource))) + (((dst_negative_code_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)) * S ((dst_negative_code_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)) + ((dst_negative_scale_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)))) + ((((dst_negative_code_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)) * S ((dst_negative_code_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)) + ((dst_negative_scale_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource))) + (((dst_negative_code_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)) * S ((dst_negative_code_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)) + ((dst_negative_scale_exists_unique_otherentrysource) + (dst_negative_scale_exists_unique_otherentrysource)))))) /\ (((((exists ff_h_pvs_exists_unique_otherentrysourcepositive. ff_h_pvs_exists_unique_otherentrysourcepositive + S (dst_positive_exists_unique_otherentrysource) = S ((S (((o) + ((s) * (srs_index_exists_unique_other))))) * dst_positive_scale_exists_unique_otherentrysource)) /\ exists ff_q_pvs_exists_unique_otherentrysourcepositive. dst_positive_code_exists_unique_otherentrysource = ff_q_pvs_exists_unique_otherentrysourcepositive * S ((S (((o) + ((s) * (srs_index_exists_unique_other))))) * dst_positive_scale_exists_unique_otherentrysource) + (dst_positive_exists_unique_otherentrysource))) /\ (((((exists ff_h_pvs_exists_unique_otherentrysourcenegative. ff_h_pvs_exists_unique_otherentrysourcenegative + S (dst_negative_exists_unique_otherentrysource) = S ((S (((o) + ((s) * (srs_index_exists_unique_other))))) * dst_negative_scale_exists_unique_otherentrysource)) /\ exists ff_q_pvs_exists_unique_otherentrysourcenegative. dst_negative_code_exists_unique_otherentrysource = ff_q_pvs_exists_unique_otherentrysourcenegative * S ((S (((o) + ((s) * (srs_index_exists_unique_other))))) * dst_negative_scale_exists_unique_otherentrysource) + (dst_negative_exists_unique_otherentrysource))) /\ (exists ge_balance_positive_exists_unique_otherentrysourcevalue ge_balance_negative_exists_unique_otherentrysourcevalue. (((((srs_value_exists_unique_other) = 2 * (ge_balance_positive_exists_unique_otherentrysourcevalue) /\ (ge_balance_negative_exists_unique_otherentrysourcevalue) = 0) \/ exists ge_signed_half_exists_unique_otherentrysourcevaluedecode. (((srs_value_exists_unique_other) = 2 * ge_signed_half_exists_unique_otherentrysourcevaluedecode + 1 /\ (ge_balance_positive_exists_unique_otherentrysourcevalue) = 0) /\ (ge_balance_negative_exists_unique_otherentrysourcevalue) = S ge_signed_half_exists_unique_otherentrysourcevaluedecode))) /\ ((dst_positive_exists_unique_otherentrysource) + ge_balance_negative_exists_unique_otherentrysourcevalue = (dst_negative_exists_unique_otherentrysource) + ge_balance_positive_exists_unique_otherentrysourcevalue))))))))) /\ (exists dst_positive_code_exists_unique_otherentryoutput dst_positive_scale_exists_unique_otherentryoutput dst_negative_code_exists_unique_otherentryoutput dst_negative_scale_exists_unique_otherentryoutput dst_positive_exists_unique_otherentryoutput dst_negative_exists_unique_otherentryoutput. (((H) = (((((dst_positive_code_exists_unique_otherentryoutput) + (dst_positive_scale_exists_unique_otherentryoutput)) * S ((dst_positive_code_exists_unique_otherentryoutput) + (dst_positive_scale_exists_unique_otherentryoutput)) + ((dst_positive_scale_exists_unique_otherentryoutput) + (dst_positive_scale_exists_unique_otherentryoutput))) + (((dst_negative_code_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)) * S ((dst_negative_code_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)) + ((dst_negative_scale_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)))) * S ((((dst_positive_code_exists_unique_otherentryoutput) + (dst_positive_scale_exists_unique_otherentryoutput)) * S ((dst_positive_code_exists_unique_otherentryoutput) + (dst_positive_scale_exists_unique_otherentryoutput)) + ((dst_positive_scale_exists_unique_otherentryoutput) + (dst_positive_scale_exists_unique_otherentryoutput))) + (((dst_negative_code_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)) * S ((dst_negative_code_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)) + ((dst_negative_scale_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)))) + ((((dst_negative_code_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)) * S ((dst_negative_code_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)) + ((dst_negative_scale_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput))) + (((dst_negative_code_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)) * S ((dst_negative_code_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)) + ((dst_negative_scale_exists_unique_otherentryoutput) + (dst_negative_scale_exists_unique_otherentryoutput)))))) /\ (((((exists ff_h_pvs_exists_unique_otherentryoutputpositive. ff_h_pvs_exists_unique_otherentryoutputpositive + S (dst_positive_exists_unique_otherentryoutput) = S ((S (srs_index_exists_unique_other)) * dst_positive_scale_exists_unique_otherentryoutput)) /\ exists ff_q_pvs_exists_unique_otherentryoutputpositive. dst_positive_code_exists_unique_otherentryoutput = ff_q_pvs_exists_unique_otherentryoutputpositive * S ((S (srs_index_exists_unique_other)) * dst_positive_scale_exists_unique_otherentryoutput) + (dst_positive_exists_unique_otherentryoutput))) /\ (((((exists ff_h_pvs_exists_unique_otherentryoutputnegative. ff_h_pvs_exists_unique_otherentryoutputnegative + S (dst_negative_exists_unique_otherentryoutput) = S ((S (srs_index_exists_unique_other)) * dst_negative_scale_exists_unique_otherentryoutput)) /\ exists ff_q_pvs_exists_unique_otherentryoutputnegative. dst_negative_code_exists_unique_otherentryoutput = ff_q_pvs_exists_unique_otherentryoutputnegative * S ((S (srs_index_exists_unique_other)) * dst_negative_scale_exists_unique_otherentryoutput) + (dst_negative_exists_unique_otherentryoutput))) /\ (exists ge_balance_positive_exists_unique_otherentryoutputvalue ge_balance_negative_exists_unique_otherentryoutputvalue. (((((srs_value_exists_unique_other) = 2 * (ge_balance_positive_exists_unique_otherentryoutputvalue) /\ (ge_balance_negative_exists_unique_otherentryoutputvalue) = 0) \/ exists ge_signed_half_exists_unique_otherentryoutputvaluedecode. (((srs_value_exists_unique_other) = 2 * ge_signed_half_exists_unique_otherentryoutputvaluedecode + 1 /\ (ge_balance_positive_exists_unique_otherentryoutputvalue) = 0) /\ (ge_balance_negative_exists_unique_otherentryoutputvalue) = S ge_signed_half_exists_unique_otherentryoutputvaluedecode))) /\ ((dst_positive_exists_unique_otherentryoutput) + ge_balance_negative_exists_unique_otherentryoutputvalue = (dst_negative_exists_unique_otherentryoutput) + ge_balance_positive_exists_unique_otherentryoutputvalue)))))))))))))))) -> (forall dst_index_exists_unique_equal dst_first_exists_unique_equal dst_second_exists_unique_equal. (exists pvs_gap_exists_unique_equalbound. pvs_gap_exists_unique_equalbound + S (dst_index_exists_unique_equal) = (l)) -> (exists dst_positive_code_exists_unique_equalfirst dst_positive_scale_exists_unique_equalfirst dst_negative_code_exists_unique_equalfirst dst_negative_scale_exists_unique_equalfirst dst_positive_exists_unique_equalfirst dst_negative_exists_unique_equalfirst. (((G) = (((((dst_positive_code_exists_unique_equalfirst) + (dst_positive_scale_exists_unique_equalfirst)) * S ((dst_positive_code_exists_unique_equalfirst) + (dst_positive_scale_exists_unique_equalfirst)) + ((dst_positive_scale_exists_unique_equalfirst) + (dst_positive_scale_exists_unique_equalfirst))) + (((dst_negative_code_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)) * S ((dst_negative_code_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)) + ((dst_negative_scale_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)))) * S ((((dst_positive_code_exists_unique_equalfirst) + (dst_positive_scale_exists_unique_equalfirst)) * S ((dst_positive_code_exists_unique_equalfirst) + (dst_positive_scale_exists_unique_equalfirst)) + ((dst_positive_scale_exists_unique_equalfirst) + (dst_positive_scale_exists_unique_equalfirst))) + (((dst_negative_code_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)) * S ((dst_negative_code_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)) + ((dst_negative_scale_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)))) + ((((dst_negative_code_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)) * S ((dst_negative_code_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)) + ((dst_negative_scale_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst))) + (((dst_negative_code_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)) * S ((dst_negative_code_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)) + ((dst_negative_scale_exists_unique_equalfirst) + (dst_negative_scale_exists_unique_equalfirst)))))) /\ (((((exists ff_h_pvs_exists_unique_equalfirstpositive. ff_h_pvs_exists_unique_equalfirstpositive + S (dst_positive_exists_unique_equalfirst) = S ((S (dst_index_exists_unique_equal)) * dst_positive_scale_exists_unique_equalfirst)) /\ exists ff_q_pvs_exists_unique_equalfirstpositive. dst_positive_code_exists_unique_equalfirst = ff_q_pvs_exists_unique_equalfirstpositive * S ((S (dst_index_exists_unique_equal)) * dst_positive_scale_exists_unique_equalfirst) + (dst_positive_exists_unique_equalfirst))) /\ (((((exists ff_h_pvs_exists_unique_equalfirstnegative. ff_h_pvs_exists_unique_equalfirstnegative + S (dst_negative_exists_unique_equalfirst) = S ((S (dst_index_exists_unique_equal)) * dst_negative_scale_exists_unique_equalfirst)) /\ exists ff_q_pvs_exists_unique_equalfirstnegative. dst_negative_code_exists_unique_equalfirst = ff_q_pvs_exists_unique_equalfirstnegative * S ((S (dst_index_exists_unique_equal)) * dst_negative_scale_exists_unique_equalfirst) + (dst_negative_exists_unique_equalfirst))) /\ (exists ge_balance_positive_exists_unique_equalfirstvalue ge_balance_negative_exists_unique_equalfirstvalue. (((((dst_first_exists_unique_equal) = 2 * (ge_balance_positive_exists_unique_equalfirstvalue) /\ (ge_balance_negative_exists_unique_equalfirstvalue) = 0) \/ exists ge_signed_half_exists_unique_equalfirstvaluedecode. (((dst_first_exists_unique_equal) = 2 * ge_signed_half_exists_unique_equalfirstvaluedecode + 1 /\ (ge_balance_positive_exists_unique_equalfirstvalue) = 0) /\ (ge_balance_negative_exists_unique_equalfirstvalue) = S ge_signed_half_exists_unique_equalfirstvaluedecode))) /\ ((dst_positive_exists_unique_equalfirst) + ge_balance_negative_exists_unique_equalfirstvalue = (dst_negative_exists_unique_equalfirst) + ge_balance_positive_exists_unique_equalfirstvalue))))))))) -> (exists dst_positive_code_exists_unique_equalsecond dst_positive_scale_exists_unique_equalsecond dst_negative_code_exists_unique_equalsecond dst_negative_scale_exists_unique_equalsecond dst_positive_exists_unique_equalsecond dst_negative_exists_unique_equalsecond. (((H) = (((((dst_positive_code_exists_unique_equalsecond) + (dst_positive_scale_exists_unique_equalsecond)) * S ((dst_positive_code_exists_unique_equalsecond) + (dst_positive_scale_exists_unique_equalsecond)) + ((dst_positive_scale_exists_unique_equalsecond) + (dst_positive_scale_exists_unique_equalsecond))) + (((dst_negative_code_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)) * S ((dst_negative_code_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)) + ((dst_negative_scale_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)))) * S ((((dst_positive_code_exists_unique_equalsecond) + (dst_positive_scale_exists_unique_equalsecond)) * S ((dst_positive_code_exists_unique_equalsecond) + (dst_positive_scale_exists_unique_equalsecond)) + ((dst_positive_scale_exists_unique_equalsecond) + (dst_positive_scale_exists_unique_equalsecond))) + (((dst_negative_code_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)) * S ((dst_negative_code_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)) + ((dst_negative_scale_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)))) + ((((dst_negative_code_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)) * S ((dst_negative_code_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)) + ((dst_negative_scale_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond))) + (((dst_negative_code_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)) * S ((dst_negative_code_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)) + ((dst_negative_scale_exists_unique_equalsecond) + (dst_negative_scale_exists_unique_equalsecond)))))) /\ (((((exists ff_h_pvs_exists_unique_equalsecondpositive. ff_h_pvs_exists_unique_equalsecondpositive + S (dst_positive_exists_unique_equalsecond) = S ((S (dst_index_exists_unique_equal)) * dst_positive_scale_exists_unique_equalsecond)) /\ exists ff_q_pvs_exists_unique_equalsecondpositive. dst_positive_code_exists_unique_equalsecond = ff_q_pvs_exists_unique_equalsecondpositive * S ((S (dst_index_exists_unique_equal)) * dst_positive_scale_exists_unique_equalsecond) + (dst_positive_exists_unique_equalsecond))) /\ (((((exists ff_h_pvs_exists_unique_equalsecondnegative. ff_h_pvs_exists_unique_equalsecondnegative + S (dst_negative_exists_unique_equalsecond) = S ((S (dst_index_exists_unique_equal)) * dst_negative_scale_exists_unique_equalsecond)) /\ exists ff_q_pvs_exists_unique_equalsecondnegative. dst_negative_code_exists_unique_equalsecond = ff_q_pvs_exists_unique_equalsecondnegative * S ((S (dst_index_exists_unique_equal)) * dst_negative_scale_exists_unique_equalsecond) + (dst_negative_exists_unique_equalsecond))) /\ (exists ge_balance_positive_exists_unique_equalsecondvalue ge_balance_negative_exists_unique_equalsecondvalue. (((((dst_second_exists_unique_equal) = 2 * (ge_balance_positive_exists_unique_equalsecondvalue) /\ (ge_balance_negative_exists_unique_equalsecondvalue) = 0) \/ exists ge_signed_half_exists_unique_equalsecondvaluedecode. (((dst_second_exists_unique_equal) = 2 * ge_signed_half_exists_unique_equalsecondvaluedecode + 1 /\ (ge_balance_positive_exists_unique_equalsecondvalue) = 0) /\ (ge_balance_negative_exists_unique_equalsecondvalue) = S ge_signed_half_exists_unique_equalsecondvaluedecode))) /\ ((dst_positive_exists_unique_equalsecond) + ge_balance_negative_exists_unique_equalsecondvalue = (dst_negative_exists_unique_equalsecond) + ge_balance_positive_exists_unique_equalsecondvalue))))))))) -> dst_first_exists_unique_equal = dst_second_exists_unique_equal)))