signed_rectangular_slice_sum_exists_unique

Exact expanded first-order arithmetic statement

forall F o s l. (exists dst_positive_code_sum_unique_input dst_positive_scale_sum_unique_input dst_negative_code_sum_unique_input dst_negative_scale_sum_unique_input. (((F) = (((((dst_positive_code_sum_unique_input) + (dst_positive_scale_sum_unique_input)) * S ((dst_positive_code_sum_unique_input) + (dst_positive_scale_sum_unique_input)) + ((dst_positive_scale_sum_unique_input) + (dst_positive_scale_sum_unique_input))) + (((dst_negative_code_sum_unique_input) + (dst_negative_scale_sum_unique_input)) * S ((dst_negative_code_sum_unique_input) + (dst_negative_scale_sum_unique_input)) + ((dst_negative_scale_sum_unique_input) + (dst_negative_scale_sum_unique_input)))) * S ((((dst_positive_code_sum_unique_input) + (dst_positive_scale_sum_unique_input)) * S ((dst_positive_code_sum_unique_input) + (dst_positive_scale_sum_unique_input)) + ((dst_positive_scale_sum_unique_input) + (dst_positive_scale_sum_unique_input))) + (((dst_negative_code_sum_unique_input) + (dst_negative_scale_sum_unique_input)) * S ((dst_negative_code_sum_unique_input) + (dst_negative_scale_sum_unique_input)) + ((dst_negative_scale_sum_unique_input) + (dst_negative_scale_sum_unique_input)))) + ((((dst_negative_code_sum_unique_input) + (dst_negative_scale_sum_unique_input)) * S ((dst_negative_code_sum_unique_input) + (dst_negative_scale_sum_unique_input)) + ((dst_negative_scale_sum_unique_input) + (dst_negative_scale_sum_unique_input))) + (((dst_negative_code_sum_unique_input) + (dst_negative_scale_sum_unique_input)) * S ((dst_negative_code_sum_unique_input) + (dst_negative_scale_sum_unique_input)) + ((dst_negative_scale_sum_unique_input) + (dst_negative_scale_sum_unique_input)))))) /\ (forall dst_index_sum_unique_input. (exists pvs_le_gap_sum_unique_inputdomain. pvs_le_gap_sum_unique_inputdomain + (dst_index_sum_unique_input) = (0)) -> exists dst_positive_sum_unique_input dst_negative_sum_unique_input dst_value_sum_unique_input. ((((exists ff_h_pvs_sum_unique_inputentrypositive. ff_h_pvs_sum_unique_inputentrypositive + S (dst_positive_sum_unique_input) = S ((S (dst_index_sum_unique_input)) * dst_positive_scale_sum_unique_input)) /\ exists ff_q_pvs_sum_unique_inputentrypositive. dst_positive_code_sum_unique_input = ff_q_pvs_sum_unique_inputentrypositive * S ((S (dst_index_sum_unique_input)) * dst_positive_scale_sum_unique_input) + (dst_positive_sum_unique_input))) /\ (((((exists ff_h_pvs_sum_unique_inputentrynegative. ff_h_pvs_sum_unique_inputentrynegative + S (dst_negative_sum_unique_input) = S ((S (dst_index_sum_unique_input)) * dst_negative_scale_sum_unique_input)) /\ exists ff_q_pvs_sum_unique_inputentrynegative. dst_negative_code_sum_unique_input = ff_q_pvs_sum_unique_inputentrynegative * S ((S (dst_index_sum_unique_input)) * dst_negative_scale_sum_unique_input) + (dst_negative_sum_unique_input))) /\ (exists ge_balance_positive_sum_unique_inputentryvalue ge_balance_negative_sum_unique_inputentryvalue. (((((dst_value_sum_unique_input) = 2 * (ge_balance_positive_sum_unique_inputentryvalue) /\ (ge_balance_negative_sum_unique_inputentryvalue) = 0) \/ exists ge_signed_half_sum_unique_inputentryvaluedecode. (((dst_value_sum_unique_input) = 2 * ge_signed_half_sum_unique_inputentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_inputentryvalue) = 0) /\ (ge_balance_negative_sum_unique_inputentryvalue) = S ge_signed_half_sum_unique_inputentryvaluedecode))) /\ ((dst_positive_sum_unique_input) + ge_balance_negative_sum_unique_inputentryvalue = (dst_negative_sum_unique_input) + ge_balance_positive_sum_unique_inputentryvalue))))))))) -> exists z. ((exists srs_slice_sum_unique_result. ((((exists dst_positive_code_sum_unique_resultslicesource_table dst_positive_scale_sum_unique_resultslicesource_table dst_negative_code_sum_unique_resultslicesource_table dst_negative_scale_sum_unique_resultslicesource_table. (((F) = (((((dst_positive_code_sum_unique_resultslicesource_table) + (dst_positive_scale_sum_unique_resultslicesource_table)) * S ((dst_positive_code_sum_unique_resultslicesource_table) + (dst_positive_scale_sum_unique_resultslicesource_table)) + ((dst_positive_scale_sum_unique_resultslicesource_table) + (dst_positive_scale_sum_unique_resultslicesource_table))) + (((dst_negative_code_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)) * S ((dst_negative_code_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)) + ((dst_negative_scale_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)))) * S ((((dst_positive_code_sum_unique_resultslicesource_table) + (dst_positive_scale_sum_unique_resultslicesource_table)) * S ((dst_positive_code_sum_unique_resultslicesource_table) + (dst_positive_scale_sum_unique_resultslicesource_table)) + ((dst_positive_scale_sum_unique_resultslicesource_table) + (dst_positive_scale_sum_unique_resultslicesource_table))) + (((dst_negative_code_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)) * S ((dst_negative_code_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)) + ((dst_negative_scale_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)))) + ((((dst_negative_code_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)) * S ((dst_negative_code_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)) + ((dst_negative_scale_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table))) + (((dst_negative_code_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)) * S ((dst_negative_code_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)) + ((dst_negative_scale_sum_unique_resultslicesource_table) + (dst_negative_scale_sum_unique_resultslicesource_table)))))) /\ (forall dst_index_sum_unique_resultslicesource_table. (exists pvs_le_gap_sum_unique_resultslicesource_tabledomain. pvs_le_gap_sum_unique_resultslicesource_tabledomain + (dst_index_sum_unique_resultslicesource_table) = (0)) -> exists dst_positive_sum_unique_resultslicesource_table dst_negative_sum_unique_resultslicesource_table dst_value_sum_unique_resultslicesource_table. ((((exists ff_h_pvs_sum_unique_resultslicesource_tableentrypositive. ff_h_pvs_sum_unique_resultslicesource_tableentrypositive + S (dst_positive_sum_unique_resultslicesource_table) = S ((S (dst_index_sum_unique_resultslicesource_table)) * dst_positive_scale_sum_unique_resultslicesource_table)) /\ exists ff_q_pvs_sum_unique_resultslicesource_tableentrypositive. dst_positive_code_sum_unique_resultslicesource_table = ff_q_pvs_sum_unique_resultslicesource_tableentrypositive * S ((S (dst_index_sum_unique_resultslicesource_table)) * dst_positive_scale_sum_unique_resultslicesource_table) + (dst_positive_sum_unique_resultslicesource_table))) /\ (((((exists ff_h_pvs_sum_unique_resultslicesource_tableentrynegative. ff_h_pvs_sum_unique_resultslicesource_tableentrynegative + S (dst_negative_sum_unique_resultslicesource_table) = S ((S (dst_index_sum_unique_resultslicesource_table)) * dst_negative_scale_sum_unique_resultslicesource_table)) /\ exists ff_q_pvs_sum_unique_resultslicesource_tableentrynegative. dst_negative_code_sum_unique_resultslicesource_table = ff_q_pvs_sum_unique_resultslicesource_tableentrynegative * S ((S (dst_index_sum_unique_resultslicesource_table)) * dst_negative_scale_sum_unique_resultslicesource_table) + (dst_negative_sum_unique_resultslicesource_table))) /\ (exists ge_balance_positive_sum_unique_resultslicesource_tableentryvalue ge_balance_negative_sum_unique_resultslicesource_tableentryvalue. (((((dst_value_sum_unique_resultslicesource_table) = 2 * (ge_balance_positive_sum_unique_resultslicesource_tableentryvalue) /\ (ge_balance_negative_sum_unique_resultslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_unique_resultslicesource_tableentryvaluedecode. (((dst_value_sum_unique_resultslicesource_table) = 2 * ge_signed_half_sum_unique_resultslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_resultslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_unique_resultslicesource_tableentryvalue) = S ge_signed_half_sum_unique_resultslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_unique_resultslicesource_table) + ge_balance_negative_sum_unique_resultslicesource_tableentryvalue = (dst_negative_sum_unique_resultslicesource_table) + ge_balance_positive_sum_unique_resultslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_unique_resultsliceoutput_table dst_positive_scale_sum_unique_resultsliceoutput_table dst_negative_code_sum_unique_resultsliceoutput_table dst_negative_scale_sum_unique_resultsliceoutput_table. (((srs_slice_sum_unique_result) = (((((dst_positive_code_sum_unique_resultsliceoutput_table) + (dst_positive_scale_sum_unique_resultsliceoutput_table)) * S ((dst_positive_code_sum_unique_resultsliceoutput_table) + (dst_positive_scale_sum_unique_resultsliceoutput_table)) + ((dst_positive_scale_sum_unique_resultsliceoutput_table) + (dst_positive_scale_sum_unique_resultsliceoutput_table))) + (((dst_negative_code_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)) * S ((dst_negative_code_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)) + ((dst_negative_scale_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)))) * S ((((dst_positive_code_sum_unique_resultsliceoutput_table) + (dst_positive_scale_sum_unique_resultsliceoutput_table)) * S ((dst_positive_code_sum_unique_resultsliceoutput_table) + (dst_positive_scale_sum_unique_resultsliceoutput_table)) + ((dst_positive_scale_sum_unique_resultsliceoutput_table) + (dst_positive_scale_sum_unique_resultsliceoutput_table))) + (((dst_negative_code_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)) * S ((dst_negative_code_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)) + ((dst_negative_scale_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)))) + ((((dst_negative_code_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)) * S ((dst_negative_code_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)) + ((dst_negative_scale_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table))) + (((dst_negative_code_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)) * S ((dst_negative_code_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)) + ((dst_negative_scale_sum_unique_resultsliceoutput_table) + (dst_negative_scale_sum_unique_resultsliceoutput_table)))))) /\ (forall dst_index_sum_unique_resultsliceoutput_table. (exists pvs_le_gap_sum_unique_resultsliceoutput_tabledomain. pvs_le_gap_sum_unique_resultsliceoutput_tabledomain + (dst_index_sum_unique_resultsliceoutput_table) = (l)) -> exists dst_positive_sum_unique_resultsliceoutput_table dst_negative_sum_unique_resultsliceoutput_table dst_value_sum_unique_resultsliceoutput_table. ((((exists ff_h_pvs_sum_unique_resultsliceoutput_tableentrypositive. ff_h_pvs_sum_unique_resultsliceoutput_tableentrypositive + S (dst_positive_sum_unique_resultsliceoutput_table) = S ((S (dst_index_sum_unique_resultsliceoutput_table)) * dst_positive_scale_sum_unique_resultsliceoutput_table)) /\ exists ff_q_pvs_sum_unique_resultsliceoutput_tableentrypositive. dst_positive_code_sum_unique_resultsliceoutput_table = ff_q_pvs_sum_unique_resultsliceoutput_tableentrypositive * S ((S (dst_index_sum_unique_resultsliceoutput_table)) * dst_positive_scale_sum_unique_resultsliceoutput_table) + (dst_positive_sum_unique_resultsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_unique_resultsliceoutput_tableentrynegative. ff_h_pvs_sum_unique_resultsliceoutput_tableentrynegative + S (dst_negative_sum_unique_resultsliceoutput_table) = S ((S (dst_index_sum_unique_resultsliceoutput_table)) * dst_negative_scale_sum_unique_resultsliceoutput_table)) /\ exists ff_q_pvs_sum_unique_resultsliceoutput_tableentrynegative. dst_negative_code_sum_unique_resultsliceoutput_table = ff_q_pvs_sum_unique_resultsliceoutput_tableentrynegative * S ((S (dst_index_sum_unique_resultsliceoutput_table)) * dst_negative_scale_sum_unique_resultsliceoutput_table) + (dst_negative_sum_unique_resultsliceoutput_table))) /\ (exists ge_balance_positive_sum_unique_resultsliceoutput_tableentryvalue ge_balance_negative_sum_unique_resultsliceoutput_tableentryvalue. (((((dst_value_sum_unique_resultsliceoutput_table) = 2 * (ge_balance_positive_sum_unique_resultsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_unique_resultsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_unique_resultsliceoutput_tableentryvaluedecode. (((dst_value_sum_unique_resultsliceoutput_table) = 2 * ge_signed_half_sum_unique_resultsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_resultsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_unique_resultsliceoutput_tableentryvalue) = S ge_signed_half_sum_unique_resultsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_unique_resultsliceoutput_table) + ge_balance_negative_sum_unique_resultsliceoutput_tableentryvalue = (dst_negative_sum_unique_resultsliceoutput_table) + ge_balance_positive_sum_unique_resultsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_unique_resultslice. (exists pvs_gap_sum_unique_resultslicebound. pvs_gap_sum_unique_resultslicebound + S (srs_index_sum_unique_resultslice) = (l)) -> exists srs_value_sum_unique_resultslice. (((exists dst_positive_code_sum_unique_resultsliceentrysource dst_positive_scale_sum_unique_resultsliceentrysource dst_negative_code_sum_unique_resultsliceentrysource dst_negative_scale_sum_unique_resultsliceentrysource dst_positive_sum_unique_resultsliceentrysource dst_negative_sum_unique_resultsliceentrysource. (((F) = (((((dst_positive_code_sum_unique_resultsliceentrysource) + (dst_positive_scale_sum_unique_resultsliceentrysource)) * S ((dst_positive_code_sum_unique_resultsliceentrysource) + (dst_positive_scale_sum_unique_resultsliceentrysource)) + ((dst_positive_scale_sum_unique_resultsliceentrysource) + (dst_positive_scale_sum_unique_resultsliceentrysource))) + (((dst_negative_code_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)) * S ((dst_negative_code_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)) + ((dst_negative_scale_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)))) * S ((((dst_positive_code_sum_unique_resultsliceentrysource) + (dst_positive_scale_sum_unique_resultsliceentrysource)) * S ((dst_positive_code_sum_unique_resultsliceentrysource) + (dst_positive_scale_sum_unique_resultsliceentrysource)) + ((dst_positive_scale_sum_unique_resultsliceentrysource) + (dst_positive_scale_sum_unique_resultsliceentrysource))) + (((dst_negative_code_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)) * S ((dst_negative_code_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)) + ((dst_negative_scale_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)))) + ((((dst_negative_code_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)) * S ((dst_negative_code_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)) + ((dst_negative_scale_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource))) + (((dst_negative_code_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)) * S ((dst_negative_code_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)) + ((dst_negative_scale_sum_unique_resultsliceentrysource) + (dst_negative_scale_sum_unique_resultsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_unique_resultsliceentrysourcepositive. ff_h_pvs_sum_unique_resultsliceentrysourcepositive + S (dst_positive_sum_unique_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_unique_resultslice))))) * dst_positive_scale_sum_unique_resultsliceentrysource)) /\ exists ff_q_pvs_sum_unique_resultsliceentrysourcepositive. dst_positive_code_sum_unique_resultsliceentrysource = ff_q_pvs_sum_unique_resultsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_unique_resultslice))))) * dst_positive_scale_sum_unique_resultsliceentrysource) + (dst_positive_sum_unique_resultsliceentrysource))) /\ (((((exists ff_h_pvs_sum_unique_resultsliceentrysourcenegative. ff_h_pvs_sum_unique_resultsliceentrysourcenegative + S (dst_negative_sum_unique_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_unique_resultslice))))) * dst_negative_scale_sum_unique_resultsliceentrysource)) /\ exists ff_q_pvs_sum_unique_resultsliceentrysourcenegative. dst_negative_code_sum_unique_resultsliceentrysource = ff_q_pvs_sum_unique_resultsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_unique_resultslice))))) * dst_negative_scale_sum_unique_resultsliceentrysource) + (dst_negative_sum_unique_resultsliceentrysource))) /\ (exists ge_balance_positive_sum_unique_resultsliceentrysourcevalue ge_balance_negative_sum_unique_resultsliceentrysourcevalue. (((((srs_value_sum_unique_resultslice) = 2 * (ge_balance_positive_sum_unique_resultsliceentrysourcevalue) /\ (ge_balance_negative_sum_unique_resultsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_unique_resultsliceentrysourcevaluedecode. (((srs_value_sum_unique_resultslice) = 2 * ge_signed_half_sum_unique_resultsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_unique_resultsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_unique_resultsliceentrysourcevalue) = S ge_signed_half_sum_unique_resultsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_unique_resultsliceentrysource) + ge_balance_negative_sum_unique_resultsliceentrysourcevalue = (dst_negative_sum_unique_resultsliceentrysource) + ge_balance_positive_sum_unique_resultsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_unique_resultsliceentryoutput dst_positive_scale_sum_unique_resultsliceentryoutput dst_negative_code_sum_unique_resultsliceentryoutput dst_negative_scale_sum_unique_resultsliceentryoutput dst_positive_sum_unique_resultsliceentryoutput dst_negative_sum_unique_resultsliceentryoutput. (((srs_slice_sum_unique_result) = (((((dst_positive_code_sum_unique_resultsliceentryoutput) + (dst_positive_scale_sum_unique_resultsliceentryoutput)) * S ((dst_positive_code_sum_unique_resultsliceentryoutput) + (dst_positive_scale_sum_unique_resultsliceentryoutput)) + ((dst_positive_scale_sum_unique_resultsliceentryoutput) + (dst_positive_scale_sum_unique_resultsliceentryoutput))) + (((dst_negative_code_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)) * S ((dst_negative_code_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)) + ((dst_negative_scale_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)))) * S ((((dst_positive_code_sum_unique_resultsliceentryoutput) + (dst_positive_scale_sum_unique_resultsliceentryoutput)) * S ((dst_positive_code_sum_unique_resultsliceentryoutput) + (dst_positive_scale_sum_unique_resultsliceentryoutput)) + ((dst_positive_scale_sum_unique_resultsliceentryoutput) + (dst_positive_scale_sum_unique_resultsliceentryoutput))) + (((dst_negative_code_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)) * S ((dst_negative_code_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)) + ((dst_negative_scale_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)))) + ((((dst_negative_code_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)) * S ((dst_negative_code_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)) + ((dst_negative_scale_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput))) + (((dst_negative_code_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)) * S ((dst_negative_code_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)) + ((dst_negative_scale_sum_unique_resultsliceentryoutput) + (dst_negative_scale_sum_unique_resultsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_unique_resultsliceentryoutputpositive. ff_h_pvs_sum_unique_resultsliceentryoutputpositive + S (dst_positive_sum_unique_resultsliceentryoutput) = S ((S (srs_index_sum_unique_resultslice)) * dst_positive_scale_sum_unique_resultsliceentryoutput)) /\ exists ff_q_pvs_sum_unique_resultsliceentryoutputpositive. dst_positive_code_sum_unique_resultsliceentryoutput = ff_q_pvs_sum_unique_resultsliceentryoutputpositive * S ((S (srs_index_sum_unique_resultslice)) * dst_positive_scale_sum_unique_resultsliceentryoutput) + (dst_positive_sum_unique_resultsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_unique_resultsliceentryoutputnegative. ff_h_pvs_sum_unique_resultsliceentryoutputnegative + S (dst_negative_sum_unique_resultsliceentryoutput) = S ((S (srs_index_sum_unique_resultslice)) * dst_negative_scale_sum_unique_resultsliceentryoutput)) /\ exists ff_q_pvs_sum_unique_resultsliceentryoutputnegative. dst_negative_code_sum_unique_resultsliceentryoutput = ff_q_pvs_sum_unique_resultsliceentryoutputnegative * S ((S (srs_index_sum_unique_resultslice)) * dst_negative_scale_sum_unique_resultsliceentryoutput) + (dst_negative_sum_unique_resultsliceentryoutput))) /\ (exists ge_balance_positive_sum_unique_resultsliceentryoutputvalue ge_balance_negative_sum_unique_resultsliceentryoutputvalue. (((((srs_value_sum_unique_resultslice) = 2 * (ge_balance_positive_sum_unique_resultsliceentryoutputvalue) /\ (ge_balance_negative_sum_unique_resultsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_unique_resultsliceentryoutputvaluedecode. (((srs_value_sum_unique_resultslice) = 2 * ge_signed_half_sum_unique_resultsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_unique_resultsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_unique_resultsliceentryoutputvalue) = S ge_signed_half_sum_unique_resultsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_unique_resultsliceentryoutput) + ge_balance_negative_sum_unique_resultsliceentryoutputvalue = (dst_negative_sum_unique_resultsliceentryoutput) + ge_balance_positive_sum_unique_resultsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_unique_resultsum dst_positive_scale_sum_unique_resultsum dst_negative_code_sum_unique_resultsum dst_negative_scale_sum_unique_resultsum dst_positive_sum_sum_unique_resultsum dst_negative_sum_sum_unique_resultsum. (((srs_slice_sum_unique_result) = (((((dst_positive_code_sum_unique_resultsum) + (dst_positive_scale_sum_unique_resultsum)) * S ((dst_positive_code_sum_unique_resultsum) + (dst_positive_scale_sum_unique_resultsum)) + ((dst_positive_scale_sum_unique_resultsum) + (dst_positive_scale_sum_unique_resultsum))) + (((dst_negative_code_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)) * S ((dst_negative_code_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)) + ((dst_negative_scale_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)))) * S ((((dst_positive_code_sum_unique_resultsum) + (dst_positive_scale_sum_unique_resultsum)) * S ((dst_positive_code_sum_unique_resultsum) + (dst_positive_scale_sum_unique_resultsum)) + ((dst_positive_scale_sum_unique_resultsum) + (dst_positive_scale_sum_unique_resultsum))) + (((dst_negative_code_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)) * S ((dst_negative_code_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)) + ((dst_negative_scale_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)))) + ((((dst_negative_code_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)) * S ((dst_negative_code_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)) + ((dst_negative_scale_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum))) + (((dst_negative_code_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)) * S ((dst_negative_code_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)) + ((dst_negative_scale_sum_unique_resultsum) + (dst_negative_scale_sum_unique_resultsum)))))) /\ (((exists fs_u_dst_sum_unique_resultsumpositive fs_v_dst_sum_unique_resultsumpositive. ((((exists fs_h_dst_sum_unique_resultsumpositive_body_start. fs_h_dst_sum_unique_resultsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_resultsumpositive)) /\ exists fs_q_dst_sum_unique_resultsumpositive_body_start. fs_u_dst_sum_unique_resultsumpositive = fs_q_dst_sum_unique_resultsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_unique_resultsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_unique_resultsumpositive_body_terminal. fs_h_dst_sum_unique_resultsumpositive_body_terminal + S (dst_positive_sum_sum_unique_resultsum) = S ((S (l)) * fs_v_dst_sum_unique_resultsumpositive)) /\ exists fs_q_dst_sum_unique_resultsumpositive_body_terminal. fs_u_dst_sum_unique_resultsumpositive = fs_q_dst_sum_unique_resultsumpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_unique_resultsumpositive) + (dst_positive_sum_sum_unique_resultsum))) /\ forall fs_i_dst_sum_unique_resultsumpositive_body_steps. (exists fs_lt_dst_sum_unique_resultsumpositive_body_steps_bound. fs_lt_dst_sum_unique_resultsumpositive_body_steps_bound + S fs_i_dst_sum_unique_resultsumpositive_body_steps = l) -> exists fs_a_dst_sum_unique_resultsumpositive_body_steps fs_r_dst_sum_unique_resultsumpositive_body_steps fs_s_dst_sum_unique_resultsumpositive_body_steps. ((((exists fs_h_dst_sum_unique_resultsumpositive_body_steps_summand. fs_h_dst_sum_unique_resultsumpositive_body_steps_summand + S (fs_a_dst_sum_unique_resultsumpositive_body_steps) = S ((S (fs_i_dst_sum_unique_resultsumpositive_body_steps)) * dst_positive_scale_sum_unique_resultsum)) /\ exists fs_q_dst_sum_unique_resultsumpositive_body_steps_summand. dst_positive_code_sum_unique_resultsum = fs_q_dst_sum_unique_resultsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_unique_resultsumpositive_body_steps)) * dst_positive_scale_sum_unique_resultsum) + (fs_a_dst_sum_unique_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_resultsumpositive_body_steps_partial. fs_h_dst_sum_unique_resultsumpositive_body_steps_partial + S (fs_r_dst_sum_unique_resultsumpositive_body_steps) = S ((S (fs_i_dst_sum_unique_resultsumpositive_body_steps)) * fs_v_dst_sum_unique_resultsumpositive)) /\ exists fs_q_dst_sum_unique_resultsumpositive_body_steps_partial. fs_u_dst_sum_unique_resultsumpositive = fs_q_dst_sum_unique_resultsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_unique_resultsumpositive_body_steps)) * fs_v_dst_sum_unique_resultsumpositive) + (fs_r_dst_sum_unique_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_resultsumpositive_body_steps_successor. fs_h_dst_sum_unique_resultsumpositive_body_steps_successor + S (fs_s_dst_sum_unique_resultsumpositive_body_steps) = S ((S (S fs_i_dst_sum_unique_resultsumpositive_body_steps)) * fs_v_dst_sum_unique_resultsumpositive)) /\ exists fs_q_dst_sum_unique_resultsumpositive_body_steps_successor. fs_u_dst_sum_unique_resultsumpositive = fs_q_dst_sum_unique_resultsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unique_resultsumpositive_body_steps)) * fs_v_dst_sum_unique_resultsumpositive) + (fs_s_dst_sum_unique_resultsumpositive_body_steps))) /\ fs_s_dst_sum_unique_resultsumpositive_body_steps = fs_r_dst_sum_unique_resultsumpositive_body_steps + fs_a_dst_sum_unique_resultsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unique_resultsumnegative fs_v_dst_sum_unique_resultsumnegative. ((((exists fs_h_dst_sum_unique_resultsumnegative_body_start. fs_h_dst_sum_unique_resultsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_resultsumnegative)) /\ exists fs_q_dst_sum_unique_resultsumnegative_body_start. fs_u_dst_sum_unique_resultsumnegative = fs_q_dst_sum_unique_resultsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_unique_resultsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_unique_resultsumnegative_body_terminal. fs_h_dst_sum_unique_resultsumnegative_body_terminal + S (dst_negative_sum_sum_unique_resultsum) = S ((S (l)) * fs_v_dst_sum_unique_resultsumnegative)) /\ exists fs_q_dst_sum_unique_resultsumnegative_body_terminal. fs_u_dst_sum_unique_resultsumnegative = fs_q_dst_sum_unique_resultsumnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_unique_resultsumnegative) + (dst_negative_sum_sum_unique_resultsum))) /\ forall fs_i_dst_sum_unique_resultsumnegative_body_steps. (exists fs_lt_dst_sum_unique_resultsumnegative_body_steps_bound. fs_lt_dst_sum_unique_resultsumnegative_body_steps_bound + S fs_i_dst_sum_unique_resultsumnegative_body_steps = l) -> exists fs_a_dst_sum_unique_resultsumnegative_body_steps fs_r_dst_sum_unique_resultsumnegative_body_steps fs_s_dst_sum_unique_resultsumnegative_body_steps. ((((exists fs_h_dst_sum_unique_resultsumnegative_body_steps_summand. fs_h_dst_sum_unique_resultsumnegative_body_steps_summand + S (fs_a_dst_sum_unique_resultsumnegative_body_steps) = S ((S (fs_i_dst_sum_unique_resultsumnegative_body_steps)) * dst_negative_scale_sum_unique_resultsum)) /\ exists fs_q_dst_sum_unique_resultsumnegative_body_steps_summand. dst_negative_code_sum_unique_resultsum = fs_q_dst_sum_unique_resultsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_unique_resultsumnegative_body_steps)) * dst_negative_scale_sum_unique_resultsum) + (fs_a_dst_sum_unique_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_resultsumnegative_body_steps_partial. fs_h_dst_sum_unique_resultsumnegative_body_steps_partial + S (fs_r_dst_sum_unique_resultsumnegative_body_steps) = S ((S (fs_i_dst_sum_unique_resultsumnegative_body_steps)) * fs_v_dst_sum_unique_resultsumnegative)) /\ exists fs_q_dst_sum_unique_resultsumnegative_body_steps_partial. fs_u_dst_sum_unique_resultsumnegative = fs_q_dst_sum_unique_resultsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_unique_resultsumnegative_body_steps)) * fs_v_dst_sum_unique_resultsumnegative) + (fs_r_dst_sum_unique_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_resultsumnegative_body_steps_successor. fs_h_dst_sum_unique_resultsumnegative_body_steps_successor + S (fs_s_dst_sum_unique_resultsumnegative_body_steps) = S ((S (S fs_i_dst_sum_unique_resultsumnegative_body_steps)) * fs_v_dst_sum_unique_resultsumnegative)) /\ exists fs_q_dst_sum_unique_resultsumnegative_body_steps_successor. fs_u_dst_sum_unique_resultsumnegative = fs_q_dst_sum_unique_resultsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unique_resultsumnegative_body_steps)) * fs_v_dst_sum_unique_resultsumnegative) + (fs_s_dst_sum_unique_resultsumnegative_body_steps))) /\ fs_s_dst_sum_unique_resultsumnegative_body_steps = fs_r_dst_sum_unique_resultsumnegative_body_steps + fs_a_dst_sum_unique_resultsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unique_resultsumresult ge_balance_negative_sum_unique_resultsumresult. (((((z) = 2 * (ge_balance_positive_sum_unique_resultsumresult) /\ (ge_balance_negative_sum_unique_resultsumresult) = 0) \/ exists ge_signed_half_sum_unique_resultsumresultdecode. (((z) = 2 * ge_signed_half_sum_unique_resultsumresultdecode + 1 /\ (ge_balance_positive_sum_unique_resultsumresult) = 0) /\ (ge_balance_negative_sum_unique_resultsumresult) = S ge_signed_half_sum_unique_resultsumresultdecode))) /\ ((dst_positive_sum_sum_unique_resultsum) + ge_balance_negative_sum_unique_resultsumresult = (dst_negative_sum_sum_unique_resultsum) + ge_balance_positive_sum_unique_resultsumresult))))))))))) /\ (forall w. (exists srs_slice_sum_unique_other. ((((exists dst_positive_code_sum_unique_otherslicesource_table dst_positive_scale_sum_unique_otherslicesource_table dst_negative_code_sum_unique_otherslicesource_table dst_negative_scale_sum_unique_otherslicesource_table. (((F) = (((((dst_positive_code_sum_unique_otherslicesource_table) + (dst_positive_scale_sum_unique_otherslicesource_table)) * S ((dst_positive_code_sum_unique_otherslicesource_table) + (dst_positive_scale_sum_unique_otherslicesource_table)) + ((dst_positive_scale_sum_unique_otherslicesource_table) + (dst_positive_scale_sum_unique_otherslicesource_table))) + (((dst_negative_code_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)) * S ((dst_negative_code_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)) + ((dst_negative_scale_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)))) * S ((((dst_positive_code_sum_unique_otherslicesource_table) + (dst_positive_scale_sum_unique_otherslicesource_table)) * S ((dst_positive_code_sum_unique_otherslicesource_table) + (dst_positive_scale_sum_unique_otherslicesource_table)) + ((dst_positive_scale_sum_unique_otherslicesource_table) + (dst_positive_scale_sum_unique_otherslicesource_table))) + (((dst_negative_code_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)) * S ((dst_negative_code_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)) + ((dst_negative_scale_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)))) + ((((dst_negative_code_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)) * S ((dst_negative_code_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)) + ((dst_negative_scale_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table))) + (((dst_negative_code_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)) * S ((dst_negative_code_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)) + ((dst_negative_scale_sum_unique_otherslicesource_table) + (dst_negative_scale_sum_unique_otherslicesource_table)))))) /\ (forall dst_index_sum_unique_otherslicesource_table. (exists pvs_le_gap_sum_unique_otherslicesource_tabledomain. pvs_le_gap_sum_unique_otherslicesource_tabledomain + (dst_index_sum_unique_otherslicesource_table) = (0)) -> exists dst_positive_sum_unique_otherslicesource_table dst_negative_sum_unique_otherslicesource_table dst_value_sum_unique_otherslicesource_table. ((((exists ff_h_pvs_sum_unique_otherslicesource_tableentrypositive. ff_h_pvs_sum_unique_otherslicesource_tableentrypositive + S (dst_positive_sum_unique_otherslicesource_table) = S ((S (dst_index_sum_unique_otherslicesource_table)) * dst_positive_scale_sum_unique_otherslicesource_table)) /\ exists ff_q_pvs_sum_unique_otherslicesource_tableentrypositive. dst_positive_code_sum_unique_otherslicesource_table = ff_q_pvs_sum_unique_otherslicesource_tableentrypositive * S ((S (dst_index_sum_unique_otherslicesource_table)) * dst_positive_scale_sum_unique_otherslicesource_table) + (dst_positive_sum_unique_otherslicesource_table))) /\ (((((exists ff_h_pvs_sum_unique_otherslicesource_tableentrynegative. ff_h_pvs_sum_unique_otherslicesource_tableentrynegative + S (dst_negative_sum_unique_otherslicesource_table) = S ((S (dst_index_sum_unique_otherslicesource_table)) * dst_negative_scale_sum_unique_otherslicesource_table)) /\ exists ff_q_pvs_sum_unique_otherslicesource_tableentrynegative. dst_negative_code_sum_unique_otherslicesource_table = ff_q_pvs_sum_unique_otherslicesource_tableentrynegative * S ((S (dst_index_sum_unique_otherslicesource_table)) * dst_negative_scale_sum_unique_otherslicesource_table) + (dst_negative_sum_unique_otherslicesource_table))) /\ (exists ge_balance_positive_sum_unique_otherslicesource_tableentryvalue ge_balance_negative_sum_unique_otherslicesource_tableentryvalue. (((((dst_value_sum_unique_otherslicesource_table) = 2 * (ge_balance_positive_sum_unique_otherslicesource_tableentryvalue) /\ (ge_balance_negative_sum_unique_otherslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_unique_otherslicesource_tableentryvaluedecode. (((dst_value_sum_unique_otherslicesource_table) = 2 * ge_signed_half_sum_unique_otherslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_otherslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_unique_otherslicesource_tableentryvalue) = S ge_signed_half_sum_unique_otherslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_unique_otherslicesource_table) + ge_balance_negative_sum_unique_otherslicesource_tableentryvalue = (dst_negative_sum_unique_otherslicesource_table) + ge_balance_positive_sum_unique_otherslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_unique_othersliceoutput_table dst_positive_scale_sum_unique_othersliceoutput_table dst_negative_code_sum_unique_othersliceoutput_table dst_negative_scale_sum_unique_othersliceoutput_table. (((srs_slice_sum_unique_other) = (((((dst_positive_code_sum_unique_othersliceoutput_table) + (dst_positive_scale_sum_unique_othersliceoutput_table)) * S ((dst_positive_code_sum_unique_othersliceoutput_table) + (dst_positive_scale_sum_unique_othersliceoutput_table)) + ((dst_positive_scale_sum_unique_othersliceoutput_table) + (dst_positive_scale_sum_unique_othersliceoutput_table))) + (((dst_negative_code_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)) * S ((dst_negative_code_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)) + ((dst_negative_scale_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)))) * S ((((dst_positive_code_sum_unique_othersliceoutput_table) + (dst_positive_scale_sum_unique_othersliceoutput_table)) * S ((dst_positive_code_sum_unique_othersliceoutput_table) + (dst_positive_scale_sum_unique_othersliceoutput_table)) + ((dst_positive_scale_sum_unique_othersliceoutput_table) + (dst_positive_scale_sum_unique_othersliceoutput_table))) + (((dst_negative_code_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)) * S ((dst_negative_code_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)) + ((dst_negative_scale_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)))) + ((((dst_negative_code_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)) * S ((dst_negative_code_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)) + ((dst_negative_scale_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table))) + (((dst_negative_code_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)) * S ((dst_negative_code_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)) + ((dst_negative_scale_sum_unique_othersliceoutput_table) + (dst_negative_scale_sum_unique_othersliceoutput_table)))))) /\ (forall dst_index_sum_unique_othersliceoutput_table. (exists pvs_le_gap_sum_unique_othersliceoutput_tabledomain. pvs_le_gap_sum_unique_othersliceoutput_tabledomain + (dst_index_sum_unique_othersliceoutput_table) = (l)) -> exists dst_positive_sum_unique_othersliceoutput_table dst_negative_sum_unique_othersliceoutput_table dst_value_sum_unique_othersliceoutput_table. ((((exists ff_h_pvs_sum_unique_othersliceoutput_tableentrypositive. ff_h_pvs_sum_unique_othersliceoutput_tableentrypositive + S (dst_positive_sum_unique_othersliceoutput_table) = S ((S (dst_index_sum_unique_othersliceoutput_table)) * dst_positive_scale_sum_unique_othersliceoutput_table)) /\ exists ff_q_pvs_sum_unique_othersliceoutput_tableentrypositive. dst_positive_code_sum_unique_othersliceoutput_table = ff_q_pvs_sum_unique_othersliceoutput_tableentrypositive * S ((S (dst_index_sum_unique_othersliceoutput_table)) * dst_positive_scale_sum_unique_othersliceoutput_table) + (dst_positive_sum_unique_othersliceoutput_table))) /\ (((((exists ff_h_pvs_sum_unique_othersliceoutput_tableentrynegative. ff_h_pvs_sum_unique_othersliceoutput_tableentrynegative + S (dst_negative_sum_unique_othersliceoutput_table) = S ((S (dst_index_sum_unique_othersliceoutput_table)) * dst_negative_scale_sum_unique_othersliceoutput_table)) /\ exists ff_q_pvs_sum_unique_othersliceoutput_tableentrynegative. dst_negative_code_sum_unique_othersliceoutput_table = ff_q_pvs_sum_unique_othersliceoutput_tableentrynegative * S ((S (dst_index_sum_unique_othersliceoutput_table)) * dst_negative_scale_sum_unique_othersliceoutput_table) + (dst_negative_sum_unique_othersliceoutput_table))) /\ (exists ge_balance_positive_sum_unique_othersliceoutput_tableentryvalue ge_balance_negative_sum_unique_othersliceoutput_tableentryvalue. (((((dst_value_sum_unique_othersliceoutput_table) = 2 * (ge_balance_positive_sum_unique_othersliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_unique_othersliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_unique_othersliceoutput_tableentryvaluedecode. (((dst_value_sum_unique_othersliceoutput_table) = 2 * ge_signed_half_sum_unique_othersliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_othersliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_unique_othersliceoutput_tableentryvalue) = S ge_signed_half_sum_unique_othersliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_unique_othersliceoutput_table) + ge_balance_negative_sum_unique_othersliceoutput_tableentryvalue = (dst_negative_sum_unique_othersliceoutput_table) + ge_balance_positive_sum_unique_othersliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_unique_otherslice. (exists pvs_gap_sum_unique_otherslicebound. pvs_gap_sum_unique_otherslicebound + S (srs_index_sum_unique_otherslice) = (l)) -> exists srs_value_sum_unique_otherslice. (((exists dst_positive_code_sum_unique_othersliceentrysource dst_positive_scale_sum_unique_othersliceentrysource dst_negative_code_sum_unique_othersliceentrysource dst_negative_scale_sum_unique_othersliceentrysource dst_positive_sum_unique_othersliceentrysource dst_negative_sum_unique_othersliceentrysource. (((F) = (((((dst_positive_code_sum_unique_othersliceentrysource) + (dst_positive_scale_sum_unique_othersliceentrysource)) * S ((dst_positive_code_sum_unique_othersliceentrysource) + (dst_positive_scale_sum_unique_othersliceentrysource)) + ((dst_positive_scale_sum_unique_othersliceentrysource) + (dst_positive_scale_sum_unique_othersliceentrysource))) + (((dst_negative_code_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)) * S ((dst_negative_code_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)) + ((dst_negative_scale_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)))) * S ((((dst_positive_code_sum_unique_othersliceentrysource) + (dst_positive_scale_sum_unique_othersliceentrysource)) * S ((dst_positive_code_sum_unique_othersliceentrysource) + (dst_positive_scale_sum_unique_othersliceentrysource)) + ((dst_positive_scale_sum_unique_othersliceentrysource) + (dst_positive_scale_sum_unique_othersliceentrysource))) + (((dst_negative_code_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)) * S ((dst_negative_code_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)) + ((dst_negative_scale_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)))) + ((((dst_negative_code_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)) * S ((dst_negative_code_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)) + ((dst_negative_scale_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource))) + (((dst_negative_code_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)) * S ((dst_negative_code_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)) + ((dst_negative_scale_sum_unique_othersliceentrysource) + (dst_negative_scale_sum_unique_othersliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_unique_othersliceentrysourcepositive. ff_h_pvs_sum_unique_othersliceentrysourcepositive + S (dst_positive_sum_unique_othersliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_unique_otherslice))))) * dst_positive_scale_sum_unique_othersliceentrysource)) /\ exists ff_q_pvs_sum_unique_othersliceentrysourcepositive. dst_positive_code_sum_unique_othersliceentrysource = ff_q_pvs_sum_unique_othersliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_unique_otherslice))))) * dst_positive_scale_sum_unique_othersliceentrysource) + (dst_positive_sum_unique_othersliceentrysource))) /\ (((((exists ff_h_pvs_sum_unique_othersliceentrysourcenegative. ff_h_pvs_sum_unique_othersliceentrysourcenegative + S (dst_negative_sum_unique_othersliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_unique_otherslice))))) * dst_negative_scale_sum_unique_othersliceentrysource)) /\ exists ff_q_pvs_sum_unique_othersliceentrysourcenegative. dst_negative_code_sum_unique_othersliceentrysource = ff_q_pvs_sum_unique_othersliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_unique_otherslice))))) * dst_negative_scale_sum_unique_othersliceentrysource) + (dst_negative_sum_unique_othersliceentrysource))) /\ (exists ge_balance_positive_sum_unique_othersliceentrysourcevalue ge_balance_negative_sum_unique_othersliceentrysourcevalue. (((((srs_value_sum_unique_otherslice) = 2 * (ge_balance_positive_sum_unique_othersliceentrysourcevalue) /\ (ge_balance_negative_sum_unique_othersliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_unique_othersliceentrysourcevaluedecode. (((srs_value_sum_unique_otherslice) = 2 * ge_signed_half_sum_unique_othersliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_unique_othersliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_unique_othersliceentrysourcevalue) = S ge_signed_half_sum_unique_othersliceentrysourcevaluedecode))) /\ ((dst_positive_sum_unique_othersliceentrysource) + ge_balance_negative_sum_unique_othersliceentrysourcevalue = (dst_negative_sum_unique_othersliceentrysource) + ge_balance_positive_sum_unique_othersliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_unique_othersliceentryoutput dst_positive_scale_sum_unique_othersliceentryoutput dst_negative_code_sum_unique_othersliceentryoutput dst_negative_scale_sum_unique_othersliceentryoutput dst_positive_sum_unique_othersliceentryoutput dst_negative_sum_unique_othersliceentryoutput. (((srs_slice_sum_unique_other) = (((((dst_positive_code_sum_unique_othersliceentryoutput) + (dst_positive_scale_sum_unique_othersliceentryoutput)) * S ((dst_positive_code_sum_unique_othersliceentryoutput) + (dst_positive_scale_sum_unique_othersliceentryoutput)) + ((dst_positive_scale_sum_unique_othersliceentryoutput) + (dst_positive_scale_sum_unique_othersliceentryoutput))) + (((dst_negative_code_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)) * S ((dst_negative_code_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)) + ((dst_negative_scale_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)))) * S ((((dst_positive_code_sum_unique_othersliceentryoutput) + (dst_positive_scale_sum_unique_othersliceentryoutput)) * S ((dst_positive_code_sum_unique_othersliceentryoutput) + (dst_positive_scale_sum_unique_othersliceentryoutput)) + ((dst_positive_scale_sum_unique_othersliceentryoutput) + (dst_positive_scale_sum_unique_othersliceentryoutput))) + (((dst_negative_code_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)) * S ((dst_negative_code_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)) + ((dst_negative_scale_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)))) + ((((dst_negative_code_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)) * S ((dst_negative_code_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)) + ((dst_negative_scale_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput))) + (((dst_negative_code_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)) * S ((dst_negative_code_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)) + ((dst_negative_scale_sum_unique_othersliceentryoutput) + (dst_negative_scale_sum_unique_othersliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_unique_othersliceentryoutputpositive. ff_h_pvs_sum_unique_othersliceentryoutputpositive + S (dst_positive_sum_unique_othersliceentryoutput) = S ((S (srs_index_sum_unique_otherslice)) * dst_positive_scale_sum_unique_othersliceentryoutput)) /\ exists ff_q_pvs_sum_unique_othersliceentryoutputpositive. dst_positive_code_sum_unique_othersliceentryoutput = ff_q_pvs_sum_unique_othersliceentryoutputpositive * S ((S (srs_index_sum_unique_otherslice)) * dst_positive_scale_sum_unique_othersliceentryoutput) + (dst_positive_sum_unique_othersliceentryoutput))) /\ (((((exists ff_h_pvs_sum_unique_othersliceentryoutputnegative. ff_h_pvs_sum_unique_othersliceentryoutputnegative + S (dst_negative_sum_unique_othersliceentryoutput) = S ((S (srs_index_sum_unique_otherslice)) * dst_negative_scale_sum_unique_othersliceentryoutput)) /\ exists ff_q_pvs_sum_unique_othersliceentryoutputnegative. dst_negative_code_sum_unique_othersliceentryoutput = ff_q_pvs_sum_unique_othersliceentryoutputnegative * S ((S (srs_index_sum_unique_otherslice)) * dst_negative_scale_sum_unique_othersliceentryoutput) + (dst_negative_sum_unique_othersliceentryoutput))) /\ (exists ge_balance_positive_sum_unique_othersliceentryoutputvalue ge_balance_negative_sum_unique_othersliceentryoutputvalue. (((((srs_value_sum_unique_otherslice) = 2 * (ge_balance_positive_sum_unique_othersliceentryoutputvalue) /\ (ge_balance_negative_sum_unique_othersliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_unique_othersliceentryoutputvaluedecode. (((srs_value_sum_unique_otherslice) = 2 * ge_signed_half_sum_unique_othersliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_unique_othersliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_unique_othersliceentryoutputvalue) = S ge_signed_half_sum_unique_othersliceentryoutputvaluedecode))) /\ ((dst_positive_sum_unique_othersliceentryoutput) + ge_balance_negative_sum_unique_othersliceentryoutputvalue = (dst_negative_sum_unique_othersliceentryoutput) + ge_balance_positive_sum_unique_othersliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_unique_othersum dst_positive_scale_sum_unique_othersum dst_negative_code_sum_unique_othersum dst_negative_scale_sum_unique_othersum dst_positive_sum_sum_unique_othersum dst_negative_sum_sum_unique_othersum. (((srs_slice_sum_unique_other) = (((((dst_positive_code_sum_unique_othersum) + (dst_positive_scale_sum_unique_othersum)) * S ((dst_positive_code_sum_unique_othersum) + (dst_positive_scale_sum_unique_othersum)) + ((dst_positive_scale_sum_unique_othersum) + (dst_positive_scale_sum_unique_othersum))) + (((dst_negative_code_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)) * S ((dst_negative_code_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)) + ((dst_negative_scale_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)))) * S ((((dst_positive_code_sum_unique_othersum) + (dst_positive_scale_sum_unique_othersum)) * S ((dst_positive_code_sum_unique_othersum) + (dst_positive_scale_sum_unique_othersum)) + ((dst_positive_scale_sum_unique_othersum) + (dst_positive_scale_sum_unique_othersum))) + (((dst_negative_code_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)) * S ((dst_negative_code_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)) + ((dst_negative_scale_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)))) + ((((dst_negative_code_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)) * S ((dst_negative_code_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)) + ((dst_negative_scale_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum))) + (((dst_negative_code_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)) * S ((dst_negative_code_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)) + ((dst_negative_scale_sum_unique_othersum) + (dst_negative_scale_sum_unique_othersum)))))) /\ (((exists fs_u_dst_sum_unique_othersumpositive fs_v_dst_sum_unique_othersumpositive. ((((exists fs_h_dst_sum_unique_othersumpositive_body_start. fs_h_dst_sum_unique_othersumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_othersumpositive)) /\ exists fs_q_dst_sum_unique_othersumpositive_body_start. fs_u_dst_sum_unique_othersumpositive = fs_q_dst_sum_unique_othersumpositive_body_start * S ((S (0)) * fs_v_dst_sum_unique_othersumpositive) + (0))) /\ ((((exists fs_h_dst_sum_unique_othersumpositive_body_terminal. fs_h_dst_sum_unique_othersumpositive_body_terminal + S (dst_positive_sum_sum_unique_othersum) = S ((S (l)) * fs_v_dst_sum_unique_othersumpositive)) /\ exists fs_q_dst_sum_unique_othersumpositive_body_terminal. fs_u_dst_sum_unique_othersumpositive = fs_q_dst_sum_unique_othersumpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_unique_othersumpositive) + (dst_positive_sum_sum_unique_othersum))) /\ forall fs_i_dst_sum_unique_othersumpositive_body_steps. (exists fs_lt_dst_sum_unique_othersumpositive_body_steps_bound. fs_lt_dst_sum_unique_othersumpositive_body_steps_bound + S fs_i_dst_sum_unique_othersumpositive_body_steps = l) -> exists fs_a_dst_sum_unique_othersumpositive_body_steps fs_r_dst_sum_unique_othersumpositive_body_steps fs_s_dst_sum_unique_othersumpositive_body_steps. ((((exists fs_h_dst_sum_unique_othersumpositive_body_steps_summand. fs_h_dst_sum_unique_othersumpositive_body_steps_summand + S (fs_a_dst_sum_unique_othersumpositive_body_steps) = S ((S (fs_i_dst_sum_unique_othersumpositive_body_steps)) * dst_positive_scale_sum_unique_othersum)) /\ exists fs_q_dst_sum_unique_othersumpositive_body_steps_summand. dst_positive_code_sum_unique_othersum = fs_q_dst_sum_unique_othersumpositive_body_steps_summand * S ((S (fs_i_dst_sum_unique_othersumpositive_body_steps)) * dst_positive_scale_sum_unique_othersum) + (fs_a_dst_sum_unique_othersumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_othersumpositive_body_steps_partial. fs_h_dst_sum_unique_othersumpositive_body_steps_partial + S (fs_r_dst_sum_unique_othersumpositive_body_steps) = S ((S (fs_i_dst_sum_unique_othersumpositive_body_steps)) * fs_v_dst_sum_unique_othersumpositive)) /\ exists fs_q_dst_sum_unique_othersumpositive_body_steps_partial. fs_u_dst_sum_unique_othersumpositive = fs_q_dst_sum_unique_othersumpositive_body_steps_partial * S ((S (fs_i_dst_sum_unique_othersumpositive_body_steps)) * fs_v_dst_sum_unique_othersumpositive) + (fs_r_dst_sum_unique_othersumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_othersumpositive_body_steps_successor. fs_h_dst_sum_unique_othersumpositive_body_steps_successor + S (fs_s_dst_sum_unique_othersumpositive_body_steps) = S ((S (S fs_i_dst_sum_unique_othersumpositive_body_steps)) * fs_v_dst_sum_unique_othersumpositive)) /\ exists fs_q_dst_sum_unique_othersumpositive_body_steps_successor. fs_u_dst_sum_unique_othersumpositive = fs_q_dst_sum_unique_othersumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unique_othersumpositive_body_steps)) * fs_v_dst_sum_unique_othersumpositive) + (fs_s_dst_sum_unique_othersumpositive_body_steps))) /\ fs_s_dst_sum_unique_othersumpositive_body_steps = fs_r_dst_sum_unique_othersumpositive_body_steps + fs_a_dst_sum_unique_othersumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unique_othersumnegative fs_v_dst_sum_unique_othersumnegative. ((((exists fs_h_dst_sum_unique_othersumnegative_body_start. fs_h_dst_sum_unique_othersumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_othersumnegative)) /\ exists fs_q_dst_sum_unique_othersumnegative_body_start. fs_u_dst_sum_unique_othersumnegative = fs_q_dst_sum_unique_othersumnegative_body_start * S ((S (0)) * fs_v_dst_sum_unique_othersumnegative) + (0))) /\ ((((exists fs_h_dst_sum_unique_othersumnegative_body_terminal. fs_h_dst_sum_unique_othersumnegative_body_terminal + S (dst_negative_sum_sum_unique_othersum) = S ((S (l)) * fs_v_dst_sum_unique_othersumnegative)) /\ exists fs_q_dst_sum_unique_othersumnegative_body_terminal. fs_u_dst_sum_unique_othersumnegative = fs_q_dst_sum_unique_othersumnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_unique_othersumnegative) + (dst_negative_sum_sum_unique_othersum))) /\ forall fs_i_dst_sum_unique_othersumnegative_body_steps. (exists fs_lt_dst_sum_unique_othersumnegative_body_steps_bound. fs_lt_dst_sum_unique_othersumnegative_body_steps_bound + S fs_i_dst_sum_unique_othersumnegative_body_steps = l) -> exists fs_a_dst_sum_unique_othersumnegative_body_steps fs_r_dst_sum_unique_othersumnegative_body_steps fs_s_dst_sum_unique_othersumnegative_body_steps. ((((exists fs_h_dst_sum_unique_othersumnegative_body_steps_summand. fs_h_dst_sum_unique_othersumnegative_body_steps_summand + S (fs_a_dst_sum_unique_othersumnegative_body_steps) = S ((S (fs_i_dst_sum_unique_othersumnegative_body_steps)) * dst_negative_scale_sum_unique_othersum)) /\ exists fs_q_dst_sum_unique_othersumnegative_body_steps_summand. dst_negative_code_sum_unique_othersum = fs_q_dst_sum_unique_othersumnegative_body_steps_summand * S ((S (fs_i_dst_sum_unique_othersumnegative_body_steps)) * dst_negative_scale_sum_unique_othersum) + (fs_a_dst_sum_unique_othersumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_othersumnegative_body_steps_partial. fs_h_dst_sum_unique_othersumnegative_body_steps_partial + S (fs_r_dst_sum_unique_othersumnegative_body_steps) = S ((S (fs_i_dst_sum_unique_othersumnegative_body_steps)) * fs_v_dst_sum_unique_othersumnegative)) /\ exists fs_q_dst_sum_unique_othersumnegative_body_steps_partial. fs_u_dst_sum_unique_othersumnegative = fs_q_dst_sum_unique_othersumnegative_body_steps_partial * S ((S (fs_i_dst_sum_unique_othersumnegative_body_steps)) * fs_v_dst_sum_unique_othersumnegative) + (fs_r_dst_sum_unique_othersumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_othersumnegative_body_steps_successor. fs_h_dst_sum_unique_othersumnegative_body_steps_successor + S (fs_s_dst_sum_unique_othersumnegative_body_steps) = S ((S (S fs_i_dst_sum_unique_othersumnegative_body_steps)) * fs_v_dst_sum_unique_othersumnegative)) /\ exists fs_q_dst_sum_unique_othersumnegative_body_steps_successor. fs_u_dst_sum_unique_othersumnegative = fs_q_dst_sum_unique_othersumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unique_othersumnegative_body_steps)) * fs_v_dst_sum_unique_othersumnegative) + (fs_s_dst_sum_unique_othersumnegative_body_steps))) /\ fs_s_dst_sum_unique_othersumnegative_body_steps = fs_r_dst_sum_unique_othersumnegative_body_steps + fs_a_dst_sum_unique_othersumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unique_othersumresult ge_balance_negative_sum_unique_othersumresult. (((((w) = 2 * (ge_balance_positive_sum_unique_othersumresult) /\ (ge_balance_negative_sum_unique_othersumresult) = 0) \/ exists ge_signed_half_sum_unique_othersumresultdecode. (((w) = 2 * ge_signed_half_sum_unique_othersumresultdecode + 1 /\ (ge_balance_positive_sum_unique_othersumresult) = 0) /\ (ge_balance_negative_sum_unique_othersumresult) = S ge_signed_half_sum_unique_othersumresultdecode))) /\ ((dst_positive_sum_sum_unique_othersum) + ge_balance_negative_sum_unique_othersumresult = (dst_negative_sum_sum_unique_othersum) + ge_balance_positive_sum_unique_othersumresult))))))))))) -> w=z))