signed_rectangular_slice_sum_successor_intro

Exact expanded first-order arithmetic statement

forall F o s l a b c. (exists srs_slice_sum_intro_prefix. ((((exists dst_positive_code_sum_intro_prefixslicesource_table dst_positive_scale_sum_intro_prefixslicesource_table dst_negative_code_sum_intro_prefixslicesource_table dst_negative_scale_sum_intro_prefixslicesource_table. (((F) = (((((dst_positive_code_sum_intro_prefixslicesource_table) + (dst_positive_scale_sum_intro_prefixslicesource_table)) * S ((dst_positive_code_sum_intro_prefixslicesource_table) + (dst_positive_scale_sum_intro_prefixslicesource_table)) + ((dst_positive_scale_sum_intro_prefixslicesource_table) + (dst_positive_scale_sum_intro_prefixslicesource_table))) + (((dst_negative_code_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)) * S ((dst_negative_code_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)) + ((dst_negative_scale_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)))) * S ((((dst_positive_code_sum_intro_prefixslicesource_table) + (dst_positive_scale_sum_intro_prefixslicesource_table)) * S ((dst_positive_code_sum_intro_prefixslicesource_table) + (dst_positive_scale_sum_intro_prefixslicesource_table)) + ((dst_positive_scale_sum_intro_prefixslicesource_table) + (dst_positive_scale_sum_intro_prefixslicesource_table))) + (((dst_negative_code_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)) * S ((dst_negative_code_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)) + ((dst_negative_scale_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)))) + ((((dst_negative_code_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)) * S ((dst_negative_code_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)) + ((dst_negative_scale_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table))) + (((dst_negative_code_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)) * S ((dst_negative_code_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)) + ((dst_negative_scale_sum_intro_prefixslicesource_table) + (dst_negative_scale_sum_intro_prefixslicesource_table)))))) /\ (forall dst_index_sum_intro_prefixslicesource_table. (exists pvs_le_gap_sum_intro_prefixslicesource_tabledomain. pvs_le_gap_sum_intro_prefixslicesource_tabledomain + (dst_index_sum_intro_prefixslicesource_table) = (0)) -> exists dst_positive_sum_intro_prefixslicesource_table dst_negative_sum_intro_prefixslicesource_table dst_value_sum_intro_prefixslicesource_table. ((((exists ff_h_pvs_sum_intro_prefixslicesource_tableentrypositive. ff_h_pvs_sum_intro_prefixslicesource_tableentrypositive + S (dst_positive_sum_intro_prefixslicesource_table) = S ((S (dst_index_sum_intro_prefixslicesource_table)) * dst_positive_scale_sum_intro_prefixslicesource_table)) /\ exists ff_q_pvs_sum_intro_prefixslicesource_tableentrypositive. dst_positive_code_sum_intro_prefixslicesource_table = ff_q_pvs_sum_intro_prefixslicesource_tableentrypositive * S ((S (dst_index_sum_intro_prefixslicesource_table)) * dst_positive_scale_sum_intro_prefixslicesource_table) + (dst_positive_sum_intro_prefixslicesource_table))) /\ (((((exists ff_h_pvs_sum_intro_prefixslicesource_tableentrynegative. ff_h_pvs_sum_intro_prefixslicesource_tableentrynegative + S (dst_negative_sum_intro_prefixslicesource_table) = S ((S (dst_index_sum_intro_prefixslicesource_table)) * dst_negative_scale_sum_intro_prefixslicesource_table)) /\ exists ff_q_pvs_sum_intro_prefixslicesource_tableentrynegative. dst_negative_code_sum_intro_prefixslicesource_table = ff_q_pvs_sum_intro_prefixslicesource_tableentrynegative * S ((S (dst_index_sum_intro_prefixslicesource_table)) * dst_negative_scale_sum_intro_prefixslicesource_table) + (dst_negative_sum_intro_prefixslicesource_table))) /\ (exists ge_balance_positive_sum_intro_prefixslicesource_tableentryvalue ge_balance_negative_sum_intro_prefixslicesource_tableentryvalue. (((((dst_value_sum_intro_prefixslicesource_table) = 2 * (ge_balance_positive_sum_intro_prefixslicesource_tableentryvalue) /\ (ge_balance_negative_sum_intro_prefixslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_intro_prefixslicesource_tableentryvaluedecode. (((dst_value_sum_intro_prefixslicesource_table) = 2 * ge_signed_half_sum_intro_prefixslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_intro_prefixslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_intro_prefixslicesource_tableentryvalue) = S ge_signed_half_sum_intro_prefixslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_intro_prefixslicesource_table) + ge_balance_negative_sum_intro_prefixslicesource_tableentryvalue = (dst_negative_sum_intro_prefixslicesource_table) + ge_balance_positive_sum_intro_prefixslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_intro_prefixsliceoutput_table dst_positive_scale_sum_intro_prefixsliceoutput_table dst_negative_code_sum_intro_prefixsliceoutput_table dst_negative_scale_sum_intro_prefixsliceoutput_table. (((srs_slice_sum_intro_prefix) = (((((dst_positive_code_sum_intro_prefixsliceoutput_table) + (dst_positive_scale_sum_intro_prefixsliceoutput_table)) * S ((dst_positive_code_sum_intro_prefixsliceoutput_table) + (dst_positive_scale_sum_intro_prefixsliceoutput_table)) + ((dst_positive_scale_sum_intro_prefixsliceoutput_table) + (dst_positive_scale_sum_intro_prefixsliceoutput_table))) + (((dst_negative_code_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)) * S ((dst_negative_code_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)) + ((dst_negative_scale_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)))) * S ((((dst_positive_code_sum_intro_prefixsliceoutput_table) + (dst_positive_scale_sum_intro_prefixsliceoutput_table)) * S ((dst_positive_code_sum_intro_prefixsliceoutput_table) + (dst_positive_scale_sum_intro_prefixsliceoutput_table)) + ((dst_positive_scale_sum_intro_prefixsliceoutput_table) + (dst_positive_scale_sum_intro_prefixsliceoutput_table))) + (((dst_negative_code_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)) * S ((dst_negative_code_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)) + ((dst_negative_scale_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)))) + ((((dst_negative_code_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)) * S ((dst_negative_code_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)) + ((dst_negative_scale_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table))) + (((dst_negative_code_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)) * S ((dst_negative_code_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)) + ((dst_negative_scale_sum_intro_prefixsliceoutput_table) + (dst_negative_scale_sum_intro_prefixsliceoutput_table)))))) /\ (forall dst_index_sum_intro_prefixsliceoutput_table. (exists pvs_le_gap_sum_intro_prefixsliceoutput_tabledomain. pvs_le_gap_sum_intro_prefixsliceoutput_tabledomain + (dst_index_sum_intro_prefixsliceoutput_table) = (l)) -> exists dst_positive_sum_intro_prefixsliceoutput_table dst_negative_sum_intro_prefixsliceoutput_table dst_value_sum_intro_prefixsliceoutput_table. ((((exists ff_h_pvs_sum_intro_prefixsliceoutput_tableentrypositive. ff_h_pvs_sum_intro_prefixsliceoutput_tableentrypositive + S (dst_positive_sum_intro_prefixsliceoutput_table) = S ((S (dst_index_sum_intro_prefixsliceoutput_table)) * dst_positive_scale_sum_intro_prefixsliceoutput_table)) /\ exists ff_q_pvs_sum_intro_prefixsliceoutput_tableentrypositive. dst_positive_code_sum_intro_prefixsliceoutput_table = ff_q_pvs_sum_intro_prefixsliceoutput_tableentrypositive * S ((S (dst_index_sum_intro_prefixsliceoutput_table)) * dst_positive_scale_sum_intro_prefixsliceoutput_table) + (dst_positive_sum_intro_prefixsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_intro_prefixsliceoutput_tableentrynegative. ff_h_pvs_sum_intro_prefixsliceoutput_tableentrynegative + S (dst_negative_sum_intro_prefixsliceoutput_table) = S ((S (dst_index_sum_intro_prefixsliceoutput_table)) * dst_negative_scale_sum_intro_prefixsliceoutput_table)) /\ exists ff_q_pvs_sum_intro_prefixsliceoutput_tableentrynegative. dst_negative_code_sum_intro_prefixsliceoutput_table = ff_q_pvs_sum_intro_prefixsliceoutput_tableentrynegative * S ((S (dst_index_sum_intro_prefixsliceoutput_table)) * dst_negative_scale_sum_intro_prefixsliceoutput_table) + (dst_negative_sum_intro_prefixsliceoutput_table))) /\ (exists ge_balance_positive_sum_intro_prefixsliceoutput_tableentryvalue ge_balance_negative_sum_intro_prefixsliceoutput_tableentryvalue. (((((dst_value_sum_intro_prefixsliceoutput_table) = 2 * (ge_balance_positive_sum_intro_prefixsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_intro_prefixsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_intro_prefixsliceoutput_tableentryvaluedecode. (((dst_value_sum_intro_prefixsliceoutput_table) = 2 * ge_signed_half_sum_intro_prefixsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_intro_prefixsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_intro_prefixsliceoutput_tableentryvalue) = S ge_signed_half_sum_intro_prefixsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_intro_prefixsliceoutput_table) + ge_balance_negative_sum_intro_prefixsliceoutput_tableentryvalue = (dst_negative_sum_intro_prefixsliceoutput_table) + ge_balance_positive_sum_intro_prefixsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_intro_prefixslice. (exists pvs_gap_sum_intro_prefixslicebound. pvs_gap_sum_intro_prefixslicebound + S (srs_index_sum_intro_prefixslice) = (l)) -> exists srs_value_sum_intro_prefixslice. (((exists dst_positive_code_sum_intro_prefixsliceentrysource dst_positive_scale_sum_intro_prefixsliceentrysource dst_negative_code_sum_intro_prefixsliceentrysource dst_negative_scale_sum_intro_prefixsliceentrysource dst_positive_sum_intro_prefixsliceentrysource dst_negative_sum_intro_prefixsliceentrysource. (((F) = (((((dst_positive_code_sum_intro_prefixsliceentrysource) + (dst_positive_scale_sum_intro_prefixsliceentrysource)) * S ((dst_positive_code_sum_intro_prefixsliceentrysource) + (dst_positive_scale_sum_intro_prefixsliceentrysource)) + ((dst_positive_scale_sum_intro_prefixsliceentrysource) + (dst_positive_scale_sum_intro_prefixsliceentrysource))) + (((dst_negative_code_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)) * S ((dst_negative_code_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)) + ((dst_negative_scale_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)))) * S ((((dst_positive_code_sum_intro_prefixsliceentrysource) + (dst_positive_scale_sum_intro_prefixsliceentrysource)) * S ((dst_positive_code_sum_intro_prefixsliceentrysource) + (dst_positive_scale_sum_intro_prefixsliceentrysource)) + ((dst_positive_scale_sum_intro_prefixsliceentrysource) + (dst_positive_scale_sum_intro_prefixsliceentrysource))) + (((dst_negative_code_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)) * S ((dst_negative_code_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)) + ((dst_negative_scale_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)))) + ((((dst_negative_code_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)) * S ((dst_negative_code_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)) + ((dst_negative_scale_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource))) + (((dst_negative_code_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)) * S ((dst_negative_code_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)) + ((dst_negative_scale_sum_intro_prefixsliceentrysource) + (dst_negative_scale_sum_intro_prefixsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_intro_prefixsliceentrysourcepositive. ff_h_pvs_sum_intro_prefixsliceentrysourcepositive + S (dst_positive_sum_intro_prefixsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_intro_prefixslice))))) * dst_positive_scale_sum_intro_prefixsliceentrysource)) /\ exists ff_q_pvs_sum_intro_prefixsliceentrysourcepositive. dst_positive_code_sum_intro_prefixsliceentrysource = ff_q_pvs_sum_intro_prefixsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_intro_prefixslice))))) * dst_positive_scale_sum_intro_prefixsliceentrysource) + (dst_positive_sum_intro_prefixsliceentrysource))) /\ (((((exists ff_h_pvs_sum_intro_prefixsliceentrysourcenegative. ff_h_pvs_sum_intro_prefixsliceentrysourcenegative + S (dst_negative_sum_intro_prefixsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_intro_prefixslice))))) * dst_negative_scale_sum_intro_prefixsliceentrysource)) /\ exists ff_q_pvs_sum_intro_prefixsliceentrysourcenegative. dst_negative_code_sum_intro_prefixsliceentrysource = ff_q_pvs_sum_intro_prefixsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_intro_prefixslice))))) * dst_negative_scale_sum_intro_prefixsliceentrysource) + (dst_negative_sum_intro_prefixsliceentrysource))) /\ (exists ge_balance_positive_sum_intro_prefixsliceentrysourcevalue ge_balance_negative_sum_intro_prefixsliceentrysourcevalue. (((((srs_value_sum_intro_prefixslice) = 2 * (ge_balance_positive_sum_intro_prefixsliceentrysourcevalue) /\ (ge_balance_negative_sum_intro_prefixsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_intro_prefixsliceentrysourcevaluedecode. (((srs_value_sum_intro_prefixslice) = 2 * ge_signed_half_sum_intro_prefixsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_intro_prefixsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_intro_prefixsliceentrysourcevalue) = S ge_signed_half_sum_intro_prefixsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_intro_prefixsliceentrysource) + ge_balance_negative_sum_intro_prefixsliceentrysourcevalue = (dst_negative_sum_intro_prefixsliceentrysource) + ge_balance_positive_sum_intro_prefixsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_intro_prefixsliceentryoutput dst_positive_scale_sum_intro_prefixsliceentryoutput dst_negative_code_sum_intro_prefixsliceentryoutput dst_negative_scale_sum_intro_prefixsliceentryoutput dst_positive_sum_intro_prefixsliceentryoutput dst_negative_sum_intro_prefixsliceentryoutput. (((srs_slice_sum_intro_prefix) = (((((dst_positive_code_sum_intro_prefixsliceentryoutput) + (dst_positive_scale_sum_intro_prefixsliceentryoutput)) * S ((dst_positive_code_sum_intro_prefixsliceentryoutput) + (dst_positive_scale_sum_intro_prefixsliceentryoutput)) + ((dst_positive_scale_sum_intro_prefixsliceentryoutput) + (dst_positive_scale_sum_intro_prefixsliceentryoutput))) + (((dst_negative_code_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)) * S ((dst_negative_code_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)) + ((dst_negative_scale_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)))) * S ((((dst_positive_code_sum_intro_prefixsliceentryoutput) + (dst_positive_scale_sum_intro_prefixsliceentryoutput)) * S ((dst_positive_code_sum_intro_prefixsliceentryoutput) + (dst_positive_scale_sum_intro_prefixsliceentryoutput)) + ((dst_positive_scale_sum_intro_prefixsliceentryoutput) + (dst_positive_scale_sum_intro_prefixsliceentryoutput))) + (((dst_negative_code_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)) * S ((dst_negative_code_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)) + ((dst_negative_scale_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)))) + ((((dst_negative_code_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)) * S ((dst_negative_code_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)) + ((dst_negative_scale_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput))) + (((dst_negative_code_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)) * S ((dst_negative_code_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)) + ((dst_negative_scale_sum_intro_prefixsliceentryoutput) + (dst_negative_scale_sum_intro_prefixsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_intro_prefixsliceentryoutputpositive. ff_h_pvs_sum_intro_prefixsliceentryoutputpositive + S (dst_positive_sum_intro_prefixsliceentryoutput) = S ((S (srs_index_sum_intro_prefixslice)) * dst_positive_scale_sum_intro_prefixsliceentryoutput)) /\ exists ff_q_pvs_sum_intro_prefixsliceentryoutputpositive. dst_positive_code_sum_intro_prefixsliceentryoutput = ff_q_pvs_sum_intro_prefixsliceentryoutputpositive * S ((S (srs_index_sum_intro_prefixslice)) * dst_positive_scale_sum_intro_prefixsliceentryoutput) + (dst_positive_sum_intro_prefixsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_intro_prefixsliceentryoutputnegative. ff_h_pvs_sum_intro_prefixsliceentryoutputnegative + S (dst_negative_sum_intro_prefixsliceentryoutput) = S ((S (srs_index_sum_intro_prefixslice)) * dst_negative_scale_sum_intro_prefixsliceentryoutput)) /\ exists ff_q_pvs_sum_intro_prefixsliceentryoutputnegative. dst_negative_code_sum_intro_prefixsliceentryoutput = ff_q_pvs_sum_intro_prefixsliceentryoutputnegative * S ((S (srs_index_sum_intro_prefixslice)) * dst_negative_scale_sum_intro_prefixsliceentryoutput) + (dst_negative_sum_intro_prefixsliceentryoutput))) /\ (exists ge_balance_positive_sum_intro_prefixsliceentryoutputvalue ge_balance_negative_sum_intro_prefixsliceentryoutputvalue. (((((srs_value_sum_intro_prefixslice) = 2 * (ge_balance_positive_sum_intro_prefixsliceentryoutputvalue) /\ (ge_balance_negative_sum_intro_prefixsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_intro_prefixsliceentryoutputvaluedecode. (((srs_value_sum_intro_prefixslice) = 2 * ge_signed_half_sum_intro_prefixsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_intro_prefixsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_intro_prefixsliceentryoutputvalue) = S ge_signed_half_sum_intro_prefixsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_intro_prefixsliceentryoutput) + ge_balance_negative_sum_intro_prefixsliceentryoutputvalue = (dst_negative_sum_intro_prefixsliceentryoutput) + ge_balance_positive_sum_intro_prefixsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_intro_prefixsum dst_positive_scale_sum_intro_prefixsum dst_negative_code_sum_intro_prefixsum dst_negative_scale_sum_intro_prefixsum dst_positive_sum_sum_intro_prefixsum dst_negative_sum_sum_intro_prefixsum. (((srs_slice_sum_intro_prefix) = (((((dst_positive_code_sum_intro_prefixsum) + (dst_positive_scale_sum_intro_prefixsum)) * S ((dst_positive_code_sum_intro_prefixsum) + (dst_positive_scale_sum_intro_prefixsum)) + ((dst_positive_scale_sum_intro_prefixsum) + (dst_positive_scale_sum_intro_prefixsum))) + (((dst_negative_code_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)) * S ((dst_negative_code_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)) + ((dst_negative_scale_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)))) * S ((((dst_positive_code_sum_intro_prefixsum) + (dst_positive_scale_sum_intro_prefixsum)) * S ((dst_positive_code_sum_intro_prefixsum) + (dst_positive_scale_sum_intro_prefixsum)) + ((dst_positive_scale_sum_intro_prefixsum) + (dst_positive_scale_sum_intro_prefixsum))) + (((dst_negative_code_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)) * S ((dst_negative_code_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)) + ((dst_negative_scale_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)))) + ((((dst_negative_code_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)) * S ((dst_negative_code_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)) + ((dst_negative_scale_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum))) + (((dst_negative_code_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)) * S ((dst_negative_code_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)) + ((dst_negative_scale_sum_intro_prefixsum) + (dst_negative_scale_sum_intro_prefixsum)))))) /\ (((exists fs_u_dst_sum_intro_prefixsumpositive fs_v_dst_sum_intro_prefixsumpositive. ((((exists fs_h_dst_sum_intro_prefixsumpositive_body_start. fs_h_dst_sum_intro_prefixsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_intro_prefixsumpositive)) /\ exists fs_q_dst_sum_intro_prefixsumpositive_body_start. fs_u_dst_sum_intro_prefixsumpositive = fs_q_dst_sum_intro_prefixsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_intro_prefixsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_intro_prefixsumpositive_body_terminal. fs_h_dst_sum_intro_prefixsumpositive_body_terminal + S (dst_positive_sum_sum_intro_prefixsum) = S ((S (l)) * fs_v_dst_sum_intro_prefixsumpositive)) /\ exists fs_q_dst_sum_intro_prefixsumpositive_body_terminal. fs_u_dst_sum_intro_prefixsumpositive = fs_q_dst_sum_intro_prefixsumpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_intro_prefixsumpositive) + (dst_positive_sum_sum_intro_prefixsum))) /\ forall fs_i_dst_sum_intro_prefixsumpositive_body_steps. (exists fs_lt_dst_sum_intro_prefixsumpositive_body_steps_bound. fs_lt_dst_sum_intro_prefixsumpositive_body_steps_bound + S fs_i_dst_sum_intro_prefixsumpositive_body_steps = l) -> exists fs_a_dst_sum_intro_prefixsumpositive_body_steps fs_r_dst_sum_intro_prefixsumpositive_body_steps fs_s_dst_sum_intro_prefixsumpositive_body_steps. ((((exists fs_h_dst_sum_intro_prefixsumpositive_body_steps_summand. fs_h_dst_sum_intro_prefixsumpositive_body_steps_summand + S (fs_a_dst_sum_intro_prefixsumpositive_body_steps) = S ((S (fs_i_dst_sum_intro_prefixsumpositive_body_steps)) * dst_positive_scale_sum_intro_prefixsum)) /\ exists fs_q_dst_sum_intro_prefixsumpositive_body_steps_summand. dst_positive_code_sum_intro_prefixsum = fs_q_dst_sum_intro_prefixsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_intro_prefixsumpositive_body_steps)) * dst_positive_scale_sum_intro_prefixsum) + (fs_a_dst_sum_intro_prefixsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_intro_prefixsumpositive_body_steps_partial. fs_h_dst_sum_intro_prefixsumpositive_body_steps_partial + S (fs_r_dst_sum_intro_prefixsumpositive_body_steps) = S ((S (fs_i_dst_sum_intro_prefixsumpositive_body_steps)) * fs_v_dst_sum_intro_prefixsumpositive)) /\ exists fs_q_dst_sum_intro_prefixsumpositive_body_steps_partial. fs_u_dst_sum_intro_prefixsumpositive = fs_q_dst_sum_intro_prefixsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_intro_prefixsumpositive_body_steps)) * fs_v_dst_sum_intro_prefixsumpositive) + (fs_r_dst_sum_intro_prefixsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_intro_prefixsumpositive_body_steps_successor. fs_h_dst_sum_intro_prefixsumpositive_body_steps_successor + S (fs_s_dst_sum_intro_prefixsumpositive_body_steps) = S ((S (S fs_i_dst_sum_intro_prefixsumpositive_body_steps)) * fs_v_dst_sum_intro_prefixsumpositive)) /\ exists fs_q_dst_sum_intro_prefixsumpositive_body_steps_successor. fs_u_dst_sum_intro_prefixsumpositive = fs_q_dst_sum_intro_prefixsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_intro_prefixsumpositive_body_steps)) * fs_v_dst_sum_intro_prefixsumpositive) + (fs_s_dst_sum_intro_prefixsumpositive_body_steps))) /\ fs_s_dst_sum_intro_prefixsumpositive_body_steps = fs_r_dst_sum_intro_prefixsumpositive_body_steps + fs_a_dst_sum_intro_prefixsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_intro_prefixsumnegative fs_v_dst_sum_intro_prefixsumnegative. ((((exists fs_h_dst_sum_intro_prefixsumnegative_body_start. fs_h_dst_sum_intro_prefixsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_intro_prefixsumnegative)) /\ exists fs_q_dst_sum_intro_prefixsumnegative_body_start. fs_u_dst_sum_intro_prefixsumnegative = fs_q_dst_sum_intro_prefixsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_intro_prefixsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_intro_prefixsumnegative_body_terminal. fs_h_dst_sum_intro_prefixsumnegative_body_terminal + S (dst_negative_sum_sum_intro_prefixsum) = S ((S (l)) * fs_v_dst_sum_intro_prefixsumnegative)) /\ exists fs_q_dst_sum_intro_prefixsumnegative_body_terminal. fs_u_dst_sum_intro_prefixsumnegative = fs_q_dst_sum_intro_prefixsumnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_intro_prefixsumnegative) + (dst_negative_sum_sum_intro_prefixsum))) /\ forall fs_i_dst_sum_intro_prefixsumnegative_body_steps. (exists fs_lt_dst_sum_intro_prefixsumnegative_body_steps_bound. fs_lt_dst_sum_intro_prefixsumnegative_body_steps_bound + S fs_i_dst_sum_intro_prefixsumnegative_body_steps = l) -> exists fs_a_dst_sum_intro_prefixsumnegative_body_steps fs_r_dst_sum_intro_prefixsumnegative_body_steps fs_s_dst_sum_intro_prefixsumnegative_body_steps. ((((exists fs_h_dst_sum_intro_prefixsumnegative_body_steps_summand. fs_h_dst_sum_intro_prefixsumnegative_body_steps_summand + S (fs_a_dst_sum_intro_prefixsumnegative_body_steps) = S ((S (fs_i_dst_sum_intro_prefixsumnegative_body_steps)) * dst_negative_scale_sum_intro_prefixsum)) /\ exists fs_q_dst_sum_intro_prefixsumnegative_body_steps_summand. dst_negative_code_sum_intro_prefixsum = fs_q_dst_sum_intro_prefixsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_intro_prefixsumnegative_body_steps)) * dst_negative_scale_sum_intro_prefixsum) + (fs_a_dst_sum_intro_prefixsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_intro_prefixsumnegative_body_steps_partial. fs_h_dst_sum_intro_prefixsumnegative_body_steps_partial + S (fs_r_dst_sum_intro_prefixsumnegative_body_steps) = S ((S (fs_i_dst_sum_intro_prefixsumnegative_body_steps)) * fs_v_dst_sum_intro_prefixsumnegative)) /\ exists fs_q_dst_sum_intro_prefixsumnegative_body_steps_partial. fs_u_dst_sum_intro_prefixsumnegative = fs_q_dst_sum_intro_prefixsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_intro_prefixsumnegative_body_steps)) * fs_v_dst_sum_intro_prefixsumnegative) + (fs_r_dst_sum_intro_prefixsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_intro_prefixsumnegative_body_steps_successor. fs_h_dst_sum_intro_prefixsumnegative_body_steps_successor + S (fs_s_dst_sum_intro_prefixsumnegative_body_steps) = S ((S (S fs_i_dst_sum_intro_prefixsumnegative_body_steps)) * fs_v_dst_sum_intro_prefixsumnegative)) /\ exists fs_q_dst_sum_intro_prefixsumnegative_body_steps_successor. fs_u_dst_sum_intro_prefixsumnegative = fs_q_dst_sum_intro_prefixsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_intro_prefixsumnegative_body_steps)) * fs_v_dst_sum_intro_prefixsumnegative) + (fs_s_dst_sum_intro_prefixsumnegative_body_steps))) /\ fs_s_dst_sum_intro_prefixsumnegative_body_steps = fs_r_dst_sum_intro_prefixsumnegative_body_steps + fs_a_dst_sum_intro_prefixsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_intro_prefixsumresult ge_balance_negative_sum_intro_prefixsumresult. (((((a) = 2 * (ge_balance_positive_sum_intro_prefixsumresult) /\ (ge_balance_negative_sum_intro_prefixsumresult) = 0) \/ exists ge_signed_half_sum_intro_prefixsumresultdecode. (((a) = 2 * ge_signed_half_sum_intro_prefixsumresultdecode + 1 /\ (ge_balance_positive_sum_intro_prefixsumresult) = 0) /\ (ge_balance_negative_sum_intro_prefixsumresult) = S ge_signed_half_sum_intro_prefixsumresultdecode))) /\ ((dst_positive_sum_sum_intro_prefixsum) + ge_balance_negative_sum_intro_prefixsumresult = (dst_negative_sum_sum_intro_prefixsum) + ge_balance_positive_sum_intro_prefixsumresult))))))))))) -> (exists dst_positive_code_sum_intro_source dst_positive_scale_sum_intro_source dst_negative_code_sum_intro_source dst_negative_scale_sum_intro_source dst_positive_sum_intro_source dst_negative_sum_intro_source. (((F) = (((((dst_positive_code_sum_intro_source) + (dst_positive_scale_sum_intro_source)) * S ((dst_positive_code_sum_intro_source) + (dst_positive_scale_sum_intro_source)) + ((dst_positive_scale_sum_intro_source) + (dst_positive_scale_sum_intro_source))) + (((dst_negative_code_sum_intro_source) + (dst_negative_scale_sum_intro_source)) * S ((dst_negative_code_sum_intro_source) + (dst_negative_scale_sum_intro_source)) + ((dst_negative_scale_sum_intro_source) + (dst_negative_scale_sum_intro_source)))) * S ((((dst_positive_code_sum_intro_source) + (dst_positive_scale_sum_intro_source)) * S ((dst_positive_code_sum_intro_source) + (dst_positive_scale_sum_intro_source)) + ((dst_positive_scale_sum_intro_source) + (dst_positive_scale_sum_intro_source))) + (((dst_negative_code_sum_intro_source) + (dst_negative_scale_sum_intro_source)) * S ((dst_negative_code_sum_intro_source) + (dst_negative_scale_sum_intro_source)) + ((dst_negative_scale_sum_intro_source) + (dst_negative_scale_sum_intro_source)))) + ((((dst_negative_code_sum_intro_source) + (dst_negative_scale_sum_intro_source)) * S ((dst_negative_code_sum_intro_source) + (dst_negative_scale_sum_intro_source)) + ((dst_negative_scale_sum_intro_source) + (dst_negative_scale_sum_intro_source))) + (((dst_negative_code_sum_intro_source) + (dst_negative_scale_sum_intro_source)) * S ((dst_negative_code_sum_intro_source) + (dst_negative_scale_sum_intro_source)) + ((dst_negative_scale_sum_intro_source) + (dst_negative_scale_sum_intro_source)))))) /\ (((((exists ff_h_pvs_sum_intro_sourcepositive. ff_h_pvs_sum_intro_sourcepositive + S (dst_positive_sum_intro_source) = S ((S (((o) + ((s) * (l))))) * dst_positive_scale_sum_intro_source)) /\ exists ff_q_pvs_sum_intro_sourcepositive. dst_positive_code_sum_intro_source = ff_q_pvs_sum_intro_sourcepositive * S ((S (((o) + ((s) * (l))))) * dst_positive_scale_sum_intro_source) + (dst_positive_sum_intro_source))) /\ (((((exists ff_h_pvs_sum_intro_sourcenegative. ff_h_pvs_sum_intro_sourcenegative + S (dst_negative_sum_intro_source) = S ((S (((o) + ((s) * (l))))) * dst_negative_scale_sum_intro_source)) /\ exists ff_q_pvs_sum_intro_sourcenegative. dst_negative_code_sum_intro_source = ff_q_pvs_sum_intro_sourcenegative * S ((S (((o) + ((s) * (l))))) * dst_negative_scale_sum_intro_source) + (dst_negative_sum_intro_source))) /\ (exists ge_balance_positive_sum_intro_sourcevalue ge_balance_negative_sum_intro_sourcevalue. (((((b) = 2 * (ge_balance_positive_sum_intro_sourcevalue) /\ (ge_balance_negative_sum_intro_sourcevalue) = 0) \/ exists ge_signed_half_sum_intro_sourcevaluedecode. (((b) = 2 * ge_signed_half_sum_intro_sourcevaluedecode + 1 /\ (ge_balance_positive_sum_intro_sourcevalue) = 0) /\ (ge_balance_negative_sum_intro_sourcevalue) = S ge_signed_half_sum_intro_sourcevaluedecode))) /\ ((dst_positive_sum_intro_source) + ge_balance_negative_sum_intro_sourcevalue = (dst_negative_sum_intro_source) + ge_balance_positive_sum_intro_sourcevalue))))))))) -> (exists dsa_ap_sum_intro_add dsa_an_sum_intro_add dsa_bp_sum_intro_add dsa_bn_sum_intro_add dsa_cp_sum_intro_add dsa_cn_sum_intro_add. (((((a) = 2 * (dsa_ap_sum_intro_add) /\ (dsa_an_sum_intro_add) = 0) \/ exists ge_signed_half_sum_intro_addleft. (((a) = 2 * ge_signed_half_sum_intro_addleft + 1 /\ (dsa_ap_sum_intro_add) = 0) /\ (dsa_an_sum_intro_add) = S ge_signed_half_sum_intro_addleft))) /\ ((((((b) = 2 * (dsa_bp_sum_intro_add) /\ (dsa_bn_sum_intro_add) = 0) \/ exists ge_signed_half_sum_intro_addright. (((b) = 2 * ge_signed_half_sum_intro_addright + 1 /\ (dsa_bp_sum_intro_add) = 0) /\ (dsa_bn_sum_intro_add) = S ge_signed_half_sum_intro_addright))) /\ ((((((c) = 2 * (dsa_cp_sum_intro_add) /\ (dsa_cn_sum_intro_add) = 0) \/ exists ge_signed_half_sum_intro_addoutput. (((c) = 2 * ge_signed_half_sum_intro_addoutput + 1 /\ (dsa_cp_sum_intro_add) = 0) /\ (dsa_cn_sum_intro_add) = S ge_signed_half_sum_intro_addoutput))) /\ ((dsa_ap_sum_intro_add + dsa_bp_sum_intro_add) + dsa_cn_sum_intro_add = (dsa_an_sum_intro_add + dsa_bn_sum_intro_add) + dsa_cp_sum_intro_add))))))) -> (exists srs_slice_sum_intro_result. ((((exists dst_positive_code_sum_intro_resultslicesource_table dst_positive_scale_sum_intro_resultslicesource_table dst_negative_code_sum_intro_resultslicesource_table dst_negative_scale_sum_intro_resultslicesource_table. (((F) = (((((dst_positive_code_sum_intro_resultslicesource_table) + (dst_positive_scale_sum_intro_resultslicesource_table)) * S ((dst_positive_code_sum_intro_resultslicesource_table) + (dst_positive_scale_sum_intro_resultslicesource_table)) + ((dst_positive_scale_sum_intro_resultslicesource_table) + (dst_positive_scale_sum_intro_resultslicesource_table))) + (((dst_negative_code_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)) * S ((dst_negative_code_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)) + ((dst_negative_scale_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)))) * S ((((dst_positive_code_sum_intro_resultslicesource_table) + (dst_positive_scale_sum_intro_resultslicesource_table)) * S ((dst_positive_code_sum_intro_resultslicesource_table) + (dst_positive_scale_sum_intro_resultslicesource_table)) + ((dst_positive_scale_sum_intro_resultslicesource_table) + (dst_positive_scale_sum_intro_resultslicesource_table))) + (((dst_negative_code_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)) * S ((dst_negative_code_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)) + ((dst_negative_scale_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)))) + ((((dst_negative_code_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)) * S ((dst_negative_code_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)) + ((dst_negative_scale_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table))) + (((dst_negative_code_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)) * S ((dst_negative_code_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)) + ((dst_negative_scale_sum_intro_resultslicesource_table) + (dst_negative_scale_sum_intro_resultslicesource_table)))))) /\ (forall dst_index_sum_intro_resultslicesource_table. (exists pvs_le_gap_sum_intro_resultslicesource_tabledomain. pvs_le_gap_sum_intro_resultslicesource_tabledomain + (dst_index_sum_intro_resultslicesource_table) = (0)) -> exists dst_positive_sum_intro_resultslicesource_table dst_negative_sum_intro_resultslicesource_table dst_value_sum_intro_resultslicesource_table. ((((exists ff_h_pvs_sum_intro_resultslicesource_tableentrypositive. ff_h_pvs_sum_intro_resultslicesource_tableentrypositive + S (dst_positive_sum_intro_resultslicesource_table) = S ((S (dst_index_sum_intro_resultslicesource_table)) * dst_positive_scale_sum_intro_resultslicesource_table)) /\ exists ff_q_pvs_sum_intro_resultslicesource_tableentrypositive. dst_positive_code_sum_intro_resultslicesource_table = ff_q_pvs_sum_intro_resultslicesource_tableentrypositive * S ((S (dst_index_sum_intro_resultslicesource_table)) * dst_positive_scale_sum_intro_resultslicesource_table) + (dst_positive_sum_intro_resultslicesource_table))) /\ (((((exists ff_h_pvs_sum_intro_resultslicesource_tableentrynegative. ff_h_pvs_sum_intro_resultslicesource_tableentrynegative + S (dst_negative_sum_intro_resultslicesource_table) = S ((S (dst_index_sum_intro_resultslicesource_table)) * dst_negative_scale_sum_intro_resultslicesource_table)) /\ exists ff_q_pvs_sum_intro_resultslicesource_tableentrynegative. dst_negative_code_sum_intro_resultslicesource_table = ff_q_pvs_sum_intro_resultslicesource_tableentrynegative * S ((S (dst_index_sum_intro_resultslicesource_table)) * dst_negative_scale_sum_intro_resultslicesource_table) + (dst_negative_sum_intro_resultslicesource_table))) /\ (exists ge_balance_positive_sum_intro_resultslicesource_tableentryvalue ge_balance_negative_sum_intro_resultslicesource_tableentryvalue. (((((dst_value_sum_intro_resultslicesource_table) = 2 * (ge_balance_positive_sum_intro_resultslicesource_tableentryvalue) /\ (ge_balance_negative_sum_intro_resultslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_intro_resultslicesource_tableentryvaluedecode. (((dst_value_sum_intro_resultslicesource_table) = 2 * ge_signed_half_sum_intro_resultslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_intro_resultslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_intro_resultslicesource_tableentryvalue) = S ge_signed_half_sum_intro_resultslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_intro_resultslicesource_table) + ge_balance_negative_sum_intro_resultslicesource_tableentryvalue = (dst_negative_sum_intro_resultslicesource_table) + ge_balance_positive_sum_intro_resultslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_intro_resultsliceoutput_table dst_positive_scale_sum_intro_resultsliceoutput_table dst_negative_code_sum_intro_resultsliceoutput_table dst_negative_scale_sum_intro_resultsliceoutput_table. (((srs_slice_sum_intro_result) = (((((dst_positive_code_sum_intro_resultsliceoutput_table) + (dst_positive_scale_sum_intro_resultsliceoutput_table)) * S ((dst_positive_code_sum_intro_resultsliceoutput_table) + (dst_positive_scale_sum_intro_resultsliceoutput_table)) + ((dst_positive_scale_sum_intro_resultsliceoutput_table) + (dst_positive_scale_sum_intro_resultsliceoutput_table))) + (((dst_negative_code_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)) * S ((dst_negative_code_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)) + ((dst_negative_scale_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)))) * S ((((dst_positive_code_sum_intro_resultsliceoutput_table) + (dst_positive_scale_sum_intro_resultsliceoutput_table)) * S ((dst_positive_code_sum_intro_resultsliceoutput_table) + (dst_positive_scale_sum_intro_resultsliceoutput_table)) + ((dst_positive_scale_sum_intro_resultsliceoutput_table) + (dst_positive_scale_sum_intro_resultsliceoutput_table))) + (((dst_negative_code_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)) * S ((dst_negative_code_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)) + ((dst_negative_scale_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)))) + ((((dst_negative_code_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)) * S ((dst_negative_code_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)) + ((dst_negative_scale_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table))) + (((dst_negative_code_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)) * S ((dst_negative_code_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)) + ((dst_negative_scale_sum_intro_resultsliceoutput_table) + (dst_negative_scale_sum_intro_resultsliceoutput_table)))))) /\ (forall dst_index_sum_intro_resultsliceoutput_table. (exists pvs_le_gap_sum_intro_resultsliceoutput_tabledomain. pvs_le_gap_sum_intro_resultsliceoutput_tabledomain + (dst_index_sum_intro_resultsliceoutput_table) = (S l)) -> exists dst_positive_sum_intro_resultsliceoutput_table dst_negative_sum_intro_resultsliceoutput_table dst_value_sum_intro_resultsliceoutput_table. ((((exists ff_h_pvs_sum_intro_resultsliceoutput_tableentrypositive. ff_h_pvs_sum_intro_resultsliceoutput_tableentrypositive + S (dst_positive_sum_intro_resultsliceoutput_table) = S ((S (dst_index_sum_intro_resultsliceoutput_table)) * dst_positive_scale_sum_intro_resultsliceoutput_table)) /\ exists ff_q_pvs_sum_intro_resultsliceoutput_tableentrypositive. dst_positive_code_sum_intro_resultsliceoutput_table = ff_q_pvs_sum_intro_resultsliceoutput_tableentrypositive * S ((S (dst_index_sum_intro_resultsliceoutput_table)) * dst_positive_scale_sum_intro_resultsliceoutput_table) + (dst_positive_sum_intro_resultsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_intro_resultsliceoutput_tableentrynegative. ff_h_pvs_sum_intro_resultsliceoutput_tableentrynegative + S (dst_negative_sum_intro_resultsliceoutput_table) = S ((S (dst_index_sum_intro_resultsliceoutput_table)) * dst_negative_scale_sum_intro_resultsliceoutput_table)) /\ exists ff_q_pvs_sum_intro_resultsliceoutput_tableentrynegative. dst_negative_code_sum_intro_resultsliceoutput_table = ff_q_pvs_sum_intro_resultsliceoutput_tableentrynegative * S ((S (dst_index_sum_intro_resultsliceoutput_table)) * dst_negative_scale_sum_intro_resultsliceoutput_table) + (dst_negative_sum_intro_resultsliceoutput_table))) /\ (exists ge_balance_positive_sum_intro_resultsliceoutput_tableentryvalue ge_balance_negative_sum_intro_resultsliceoutput_tableentryvalue. (((((dst_value_sum_intro_resultsliceoutput_table) = 2 * (ge_balance_positive_sum_intro_resultsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_intro_resultsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_intro_resultsliceoutput_tableentryvaluedecode. (((dst_value_sum_intro_resultsliceoutput_table) = 2 * ge_signed_half_sum_intro_resultsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_intro_resultsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_intro_resultsliceoutput_tableentryvalue) = S ge_signed_half_sum_intro_resultsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_intro_resultsliceoutput_table) + ge_balance_negative_sum_intro_resultsliceoutput_tableentryvalue = (dst_negative_sum_intro_resultsliceoutput_table) + ge_balance_positive_sum_intro_resultsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_intro_resultslice. (exists pvs_gap_sum_intro_resultslicebound. pvs_gap_sum_intro_resultslicebound + S (srs_index_sum_intro_resultslice) = (S l)) -> exists srs_value_sum_intro_resultslice. (((exists dst_positive_code_sum_intro_resultsliceentrysource dst_positive_scale_sum_intro_resultsliceentrysource dst_negative_code_sum_intro_resultsliceentrysource dst_negative_scale_sum_intro_resultsliceentrysource dst_positive_sum_intro_resultsliceentrysource dst_negative_sum_intro_resultsliceentrysource. (((F) = (((((dst_positive_code_sum_intro_resultsliceentrysource) + (dst_positive_scale_sum_intro_resultsliceentrysource)) * S ((dst_positive_code_sum_intro_resultsliceentrysource) + (dst_positive_scale_sum_intro_resultsliceentrysource)) + ((dst_positive_scale_sum_intro_resultsliceentrysource) + (dst_positive_scale_sum_intro_resultsliceentrysource))) + (((dst_negative_code_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)) * S ((dst_negative_code_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)) + ((dst_negative_scale_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)))) * S ((((dst_positive_code_sum_intro_resultsliceentrysource) + (dst_positive_scale_sum_intro_resultsliceentrysource)) * S ((dst_positive_code_sum_intro_resultsliceentrysource) + (dst_positive_scale_sum_intro_resultsliceentrysource)) + ((dst_positive_scale_sum_intro_resultsliceentrysource) + (dst_positive_scale_sum_intro_resultsliceentrysource))) + (((dst_negative_code_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)) * S ((dst_negative_code_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)) + ((dst_negative_scale_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)))) + ((((dst_negative_code_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)) * S ((dst_negative_code_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)) + ((dst_negative_scale_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource))) + (((dst_negative_code_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)) * S ((dst_negative_code_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)) + ((dst_negative_scale_sum_intro_resultsliceentrysource) + (dst_negative_scale_sum_intro_resultsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_intro_resultsliceentrysourcepositive. ff_h_pvs_sum_intro_resultsliceentrysourcepositive + S (dst_positive_sum_intro_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_intro_resultslice))))) * dst_positive_scale_sum_intro_resultsliceentrysource)) /\ exists ff_q_pvs_sum_intro_resultsliceentrysourcepositive. dst_positive_code_sum_intro_resultsliceentrysource = ff_q_pvs_sum_intro_resultsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_intro_resultslice))))) * dst_positive_scale_sum_intro_resultsliceentrysource) + (dst_positive_sum_intro_resultsliceentrysource))) /\ (((((exists ff_h_pvs_sum_intro_resultsliceentrysourcenegative. ff_h_pvs_sum_intro_resultsliceentrysourcenegative + S (dst_negative_sum_intro_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_intro_resultslice))))) * dst_negative_scale_sum_intro_resultsliceentrysource)) /\ exists ff_q_pvs_sum_intro_resultsliceentrysourcenegative. dst_negative_code_sum_intro_resultsliceentrysource = ff_q_pvs_sum_intro_resultsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_intro_resultslice))))) * dst_negative_scale_sum_intro_resultsliceentrysource) + (dst_negative_sum_intro_resultsliceentrysource))) /\ (exists ge_balance_positive_sum_intro_resultsliceentrysourcevalue ge_balance_negative_sum_intro_resultsliceentrysourcevalue. (((((srs_value_sum_intro_resultslice) = 2 * (ge_balance_positive_sum_intro_resultsliceentrysourcevalue) /\ (ge_balance_negative_sum_intro_resultsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_intro_resultsliceentrysourcevaluedecode. (((srs_value_sum_intro_resultslice) = 2 * ge_signed_half_sum_intro_resultsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_intro_resultsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_intro_resultsliceentrysourcevalue) = S ge_signed_half_sum_intro_resultsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_intro_resultsliceentrysource) + ge_balance_negative_sum_intro_resultsliceentrysourcevalue = (dst_negative_sum_intro_resultsliceentrysource) + ge_balance_positive_sum_intro_resultsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_intro_resultsliceentryoutput dst_positive_scale_sum_intro_resultsliceentryoutput dst_negative_code_sum_intro_resultsliceentryoutput dst_negative_scale_sum_intro_resultsliceentryoutput dst_positive_sum_intro_resultsliceentryoutput dst_negative_sum_intro_resultsliceentryoutput. (((srs_slice_sum_intro_result) = (((((dst_positive_code_sum_intro_resultsliceentryoutput) + (dst_positive_scale_sum_intro_resultsliceentryoutput)) * S ((dst_positive_code_sum_intro_resultsliceentryoutput) + (dst_positive_scale_sum_intro_resultsliceentryoutput)) + ((dst_positive_scale_sum_intro_resultsliceentryoutput) + (dst_positive_scale_sum_intro_resultsliceentryoutput))) + (((dst_negative_code_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)) * S ((dst_negative_code_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)) + ((dst_negative_scale_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)))) * S ((((dst_positive_code_sum_intro_resultsliceentryoutput) + (dst_positive_scale_sum_intro_resultsliceentryoutput)) * S ((dst_positive_code_sum_intro_resultsliceentryoutput) + (dst_positive_scale_sum_intro_resultsliceentryoutput)) + ((dst_positive_scale_sum_intro_resultsliceentryoutput) + (dst_positive_scale_sum_intro_resultsliceentryoutput))) + (((dst_negative_code_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)) * S ((dst_negative_code_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)) + ((dst_negative_scale_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)))) + ((((dst_negative_code_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)) * S ((dst_negative_code_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)) + ((dst_negative_scale_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput))) + (((dst_negative_code_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)) * S ((dst_negative_code_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)) + ((dst_negative_scale_sum_intro_resultsliceentryoutput) + (dst_negative_scale_sum_intro_resultsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_intro_resultsliceentryoutputpositive. ff_h_pvs_sum_intro_resultsliceentryoutputpositive + S (dst_positive_sum_intro_resultsliceentryoutput) = S ((S (srs_index_sum_intro_resultslice)) * dst_positive_scale_sum_intro_resultsliceentryoutput)) /\ exists ff_q_pvs_sum_intro_resultsliceentryoutputpositive. dst_positive_code_sum_intro_resultsliceentryoutput = ff_q_pvs_sum_intro_resultsliceentryoutputpositive * S ((S (srs_index_sum_intro_resultslice)) * dst_positive_scale_sum_intro_resultsliceentryoutput) + (dst_positive_sum_intro_resultsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_intro_resultsliceentryoutputnegative. ff_h_pvs_sum_intro_resultsliceentryoutputnegative + S (dst_negative_sum_intro_resultsliceentryoutput) = S ((S (srs_index_sum_intro_resultslice)) * dst_negative_scale_sum_intro_resultsliceentryoutput)) /\ exists ff_q_pvs_sum_intro_resultsliceentryoutputnegative. dst_negative_code_sum_intro_resultsliceentryoutput = ff_q_pvs_sum_intro_resultsliceentryoutputnegative * S ((S (srs_index_sum_intro_resultslice)) * dst_negative_scale_sum_intro_resultsliceentryoutput) + (dst_negative_sum_intro_resultsliceentryoutput))) /\ (exists ge_balance_positive_sum_intro_resultsliceentryoutputvalue ge_balance_negative_sum_intro_resultsliceentryoutputvalue. (((((srs_value_sum_intro_resultslice) = 2 * (ge_balance_positive_sum_intro_resultsliceentryoutputvalue) /\ (ge_balance_negative_sum_intro_resultsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_intro_resultsliceentryoutputvaluedecode. (((srs_value_sum_intro_resultslice) = 2 * ge_signed_half_sum_intro_resultsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_intro_resultsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_intro_resultsliceentryoutputvalue) = S ge_signed_half_sum_intro_resultsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_intro_resultsliceentryoutput) + ge_balance_negative_sum_intro_resultsliceentryoutputvalue = (dst_negative_sum_intro_resultsliceentryoutput) + ge_balance_positive_sum_intro_resultsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_intro_resultsum dst_positive_scale_sum_intro_resultsum dst_negative_code_sum_intro_resultsum dst_negative_scale_sum_intro_resultsum dst_positive_sum_sum_intro_resultsum dst_negative_sum_sum_intro_resultsum. (((srs_slice_sum_intro_result) = (((((dst_positive_code_sum_intro_resultsum) + (dst_positive_scale_sum_intro_resultsum)) * S ((dst_positive_code_sum_intro_resultsum) + (dst_positive_scale_sum_intro_resultsum)) + ((dst_positive_scale_sum_intro_resultsum) + (dst_positive_scale_sum_intro_resultsum))) + (((dst_negative_code_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)) * S ((dst_negative_code_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)) + ((dst_negative_scale_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)))) * S ((((dst_positive_code_sum_intro_resultsum) + (dst_positive_scale_sum_intro_resultsum)) * S ((dst_positive_code_sum_intro_resultsum) + (dst_positive_scale_sum_intro_resultsum)) + ((dst_positive_scale_sum_intro_resultsum) + (dst_positive_scale_sum_intro_resultsum))) + (((dst_negative_code_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)) * S ((dst_negative_code_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)) + ((dst_negative_scale_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)))) + ((((dst_negative_code_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)) * S ((dst_negative_code_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)) + ((dst_negative_scale_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum))) + (((dst_negative_code_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)) * S ((dst_negative_code_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)) + ((dst_negative_scale_sum_intro_resultsum) + (dst_negative_scale_sum_intro_resultsum)))))) /\ (((exists fs_u_dst_sum_intro_resultsumpositive fs_v_dst_sum_intro_resultsumpositive. ((((exists fs_h_dst_sum_intro_resultsumpositive_body_start. fs_h_dst_sum_intro_resultsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_intro_resultsumpositive)) /\ exists fs_q_dst_sum_intro_resultsumpositive_body_start. fs_u_dst_sum_intro_resultsumpositive = fs_q_dst_sum_intro_resultsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_intro_resultsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_intro_resultsumpositive_body_terminal. fs_h_dst_sum_intro_resultsumpositive_body_terminal + S (dst_positive_sum_sum_intro_resultsum) = S ((S (S l)) * fs_v_dst_sum_intro_resultsumpositive)) /\ exists fs_q_dst_sum_intro_resultsumpositive_body_terminal. fs_u_dst_sum_intro_resultsumpositive = fs_q_dst_sum_intro_resultsumpositive_body_terminal * S ((S (S l)) * fs_v_dst_sum_intro_resultsumpositive) + (dst_positive_sum_sum_intro_resultsum))) /\ forall fs_i_dst_sum_intro_resultsumpositive_body_steps. (exists fs_lt_dst_sum_intro_resultsumpositive_body_steps_bound. fs_lt_dst_sum_intro_resultsumpositive_body_steps_bound + S fs_i_dst_sum_intro_resultsumpositive_body_steps = S l) -> exists fs_a_dst_sum_intro_resultsumpositive_body_steps fs_r_dst_sum_intro_resultsumpositive_body_steps fs_s_dst_sum_intro_resultsumpositive_body_steps. ((((exists fs_h_dst_sum_intro_resultsumpositive_body_steps_summand. fs_h_dst_sum_intro_resultsumpositive_body_steps_summand + S (fs_a_dst_sum_intro_resultsumpositive_body_steps) = S ((S (fs_i_dst_sum_intro_resultsumpositive_body_steps)) * dst_positive_scale_sum_intro_resultsum)) /\ exists fs_q_dst_sum_intro_resultsumpositive_body_steps_summand. dst_positive_code_sum_intro_resultsum = fs_q_dst_sum_intro_resultsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_intro_resultsumpositive_body_steps)) * dst_positive_scale_sum_intro_resultsum) + (fs_a_dst_sum_intro_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_intro_resultsumpositive_body_steps_partial. fs_h_dst_sum_intro_resultsumpositive_body_steps_partial + S (fs_r_dst_sum_intro_resultsumpositive_body_steps) = S ((S (fs_i_dst_sum_intro_resultsumpositive_body_steps)) * fs_v_dst_sum_intro_resultsumpositive)) /\ exists fs_q_dst_sum_intro_resultsumpositive_body_steps_partial. fs_u_dst_sum_intro_resultsumpositive = fs_q_dst_sum_intro_resultsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_intro_resultsumpositive_body_steps)) * fs_v_dst_sum_intro_resultsumpositive) + (fs_r_dst_sum_intro_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_intro_resultsumpositive_body_steps_successor. fs_h_dst_sum_intro_resultsumpositive_body_steps_successor + S (fs_s_dst_sum_intro_resultsumpositive_body_steps) = S ((S (S fs_i_dst_sum_intro_resultsumpositive_body_steps)) * fs_v_dst_sum_intro_resultsumpositive)) /\ exists fs_q_dst_sum_intro_resultsumpositive_body_steps_successor. fs_u_dst_sum_intro_resultsumpositive = fs_q_dst_sum_intro_resultsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_intro_resultsumpositive_body_steps)) * fs_v_dst_sum_intro_resultsumpositive) + (fs_s_dst_sum_intro_resultsumpositive_body_steps))) /\ fs_s_dst_sum_intro_resultsumpositive_body_steps = fs_r_dst_sum_intro_resultsumpositive_body_steps + fs_a_dst_sum_intro_resultsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_intro_resultsumnegative fs_v_dst_sum_intro_resultsumnegative. ((((exists fs_h_dst_sum_intro_resultsumnegative_body_start. fs_h_dst_sum_intro_resultsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_intro_resultsumnegative)) /\ exists fs_q_dst_sum_intro_resultsumnegative_body_start. fs_u_dst_sum_intro_resultsumnegative = fs_q_dst_sum_intro_resultsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_intro_resultsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_intro_resultsumnegative_body_terminal. fs_h_dst_sum_intro_resultsumnegative_body_terminal + S (dst_negative_sum_sum_intro_resultsum) = S ((S (S l)) * fs_v_dst_sum_intro_resultsumnegative)) /\ exists fs_q_dst_sum_intro_resultsumnegative_body_terminal. fs_u_dst_sum_intro_resultsumnegative = fs_q_dst_sum_intro_resultsumnegative_body_terminal * S ((S (S l)) * fs_v_dst_sum_intro_resultsumnegative) + (dst_negative_sum_sum_intro_resultsum))) /\ forall fs_i_dst_sum_intro_resultsumnegative_body_steps. (exists fs_lt_dst_sum_intro_resultsumnegative_body_steps_bound. fs_lt_dst_sum_intro_resultsumnegative_body_steps_bound + S fs_i_dst_sum_intro_resultsumnegative_body_steps = S l) -> exists fs_a_dst_sum_intro_resultsumnegative_body_steps fs_r_dst_sum_intro_resultsumnegative_body_steps fs_s_dst_sum_intro_resultsumnegative_body_steps. ((((exists fs_h_dst_sum_intro_resultsumnegative_body_steps_summand. fs_h_dst_sum_intro_resultsumnegative_body_steps_summand + S (fs_a_dst_sum_intro_resultsumnegative_body_steps) = S ((S (fs_i_dst_sum_intro_resultsumnegative_body_steps)) * dst_negative_scale_sum_intro_resultsum)) /\ exists fs_q_dst_sum_intro_resultsumnegative_body_steps_summand. dst_negative_code_sum_intro_resultsum = fs_q_dst_sum_intro_resultsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_intro_resultsumnegative_body_steps)) * dst_negative_scale_sum_intro_resultsum) + (fs_a_dst_sum_intro_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_intro_resultsumnegative_body_steps_partial. fs_h_dst_sum_intro_resultsumnegative_body_steps_partial + S (fs_r_dst_sum_intro_resultsumnegative_body_steps) = S ((S (fs_i_dst_sum_intro_resultsumnegative_body_steps)) * fs_v_dst_sum_intro_resultsumnegative)) /\ exists fs_q_dst_sum_intro_resultsumnegative_body_steps_partial. fs_u_dst_sum_intro_resultsumnegative = fs_q_dst_sum_intro_resultsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_intro_resultsumnegative_body_steps)) * fs_v_dst_sum_intro_resultsumnegative) + (fs_r_dst_sum_intro_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_intro_resultsumnegative_body_steps_successor. fs_h_dst_sum_intro_resultsumnegative_body_steps_successor + S (fs_s_dst_sum_intro_resultsumnegative_body_steps) = S ((S (S fs_i_dst_sum_intro_resultsumnegative_body_steps)) * fs_v_dst_sum_intro_resultsumnegative)) /\ exists fs_q_dst_sum_intro_resultsumnegative_body_steps_successor. fs_u_dst_sum_intro_resultsumnegative = fs_q_dst_sum_intro_resultsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_intro_resultsumnegative_body_steps)) * fs_v_dst_sum_intro_resultsumnegative) + (fs_s_dst_sum_intro_resultsumnegative_body_steps))) /\ fs_s_dst_sum_intro_resultsumnegative_body_steps = fs_r_dst_sum_intro_resultsumnegative_body_steps + fs_a_dst_sum_intro_resultsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_intro_resultsumresult ge_balance_negative_sum_intro_resultsumresult. (((((c) = 2 * (ge_balance_positive_sum_intro_resultsumresult) /\ (ge_balance_negative_sum_intro_resultsumresult) = 0) \/ exists ge_signed_half_sum_intro_resultsumresultdecode. (((c) = 2 * ge_signed_half_sum_intro_resultsumresultdecode + 1 /\ (ge_balance_positive_sum_intro_resultsumresult) = 0) /\ (ge_balance_negative_sum_intro_resultsumresult) = S ge_signed_half_sum_intro_resultsumresultdecode))) /\ ((dst_positive_sum_sum_intro_resultsum) + ge_balance_negative_sum_intro_resultsumresult = (dst_negative_sum_sum_intro_resultsum) + ge_balance_positive_sum_intro_resultsumresult)))))))))))