signed_rectangular_slice_sum_successor_add

Exact expanded first-order arithmetic statement

forall F o s l a b c. (exists srs_slice_sum_add_prefix. ((((exists dst_positive_code_sum_add_prefixslicesource_table dst_positive_scale_sum_add_prefixslicesource_table dst_negative_code_sum_add_prefixslicesource_table dst_negative_scale_sum_add_prefixslicesource_table. (((F) = (((((dst_positive_code_sum_add_prefixslicesource_table) + (dst_positive_scale_sum_add_prefixslicesource_table)) * S ((dst_positive_code_sum_add_prefixslicesource_table) + (dst_positive_scale_sum_add_prefixslicesource_table)) + ((dst_positive_scale_sum_add_prefixslicesource_table) + (dst_positive_scale_sum_add_prefixslicesource_table))) + (((dst_negative_code_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)) * S ((dst_negative_code_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)) + ((dst_negative_scale_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)))) * S ((((dst_positive_code_sum_add_prefixslicesource_table) + (dst_positive_scale_sum_add_prefixslicesource_table)) * S ((dst_positive_code_sum_add_prefixslicesource_table) + (dst_positive_scale_sum_add_prefixslicesource_table)) + ((dst_positive_scale_sum_add_prefixslicesource_table) + (dst_positive_scale_sum_add_prefixslicesource_table))) + (((dst_negative_code_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)) * S ((dst_negative_code_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)) + ((dst_negative_scale_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)))) + ((((dst_negative_code_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)) * S ((dst_negative_code_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)) + ((dst_negative_scale_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table))) + (((dst_negative_code_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)) * S ((dst_negative_code_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)) + ((dst_negative_scale_sum_add_prefixslicesource_table) + (dst_negative_scale_sum_add_prefixslicesource_table)))))) /\ (forall dst_index_sum_add_prefixslicesource_table. (exists pvs_le_gap_sum_add_prefixslicesource_tabledomain. pvs_le_gap_sum_add_prefixslicesource_tabledomain + (dst_index_sum_add_prefixslicesource_table) = (0)) -> exists dst_positive_sum_add_prefixslicesource_table dst_negative_sum_add_prefixslicesource_table dst_value_sum_add_prefixslicesource_table. ((((exists ff_h_pvs_sum_add_prefixslicesource_tableentrypositive. ff_h_pvs_sum_add_prefixslicesource_tableentrypositive + S (dst_positive_sum_add_prefixslicesource_table) = S ((S (dst_index_sum_add_prefixslicesource_table)) * dst_positive_scale_sum_add_prefixslicesource_table)) /\ exists ff_q_pvs_sum_add_prefixslicesource_tableentrypositive. dst_positive_code_sum_add_prefixslicesource_table = ff_q_pvs_sum_add_prefixslicesource_tableentrypositive * S ((S (dst_index_sum_add_prefixslicesource_table)) * dst_positive_scale_sum_add_prefixslicesource_table) + (dst_positive_sum_add_prefixslicesource_table))) /\ (((((exists ff_h_pvs_sum_add_prefixslicesource_tableentrynegative. ff_h_pvs_sum_add_prefixslicesource_tableentrynegative + S (dst_negative_sum_add_prefixslicesource_table) = S ((S (dst_index_sum_add_prefixslicesource_table)) * dst_negative_scale_sum_add_prefixslicesource_table)) /\ exists ff_q_pvs_sum_add_prefixslicesource_tableentrynegative. dst_negative_code_sum_add_prefixslicesource_table = ff_q_pvs_sum_add_prefixslicesource_tableentrynegative * S ((S (dst_index_sum_add_prefixslicesource_table)) * dst_negative_scale_sum_add_prefixslicesource_table) + (dst_negative_sum_add_prefixslicesource_table))) /\ (exists ge_balance_positive_sum_add_prefixslicesource_tableentryvalue ge_balance_negative_sum_add_prefixslicesource_tableentryvalue. (((((dst_value_sum_add_prefixslicesource_table) = 2 * (ge_balance_positive_sum_add_prefixslicesource_tableentryvalue) /\ (ge_balance_negative_sum_add_prefixslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_add_prefixslicesource_tableentryvaluedecode. (((dst_value_sum_add_prefixslicesource_table) = 2 * ge_signed_half_sum_add_prefixslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_add_prefixslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_add_prefixslicesource_tableentryvalue) = S ge_signed_half_sum_add_prefixslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_add_prefixslicesource_table) + ge_balance_negative_sum_add_prefixslicesource_tableentryvalue = (dst_negative_sum_add_prefixslicesource_table) + ge_balance_positive_sum_add_prefixslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_add_prefixsliceoutput_table dst_positive_scale_sum_add_prefixsliceoutput_table dst_negative_code_sum_add_prefixsliceoutput_table dst_negative_scale_sum_add_prefixsliceoutput_table. (((srs_slice_sum_add_prefix) = (((((dst_positive_code_sum_add_prefixsliceoutput_table) + (dst_positive_scale_sum_add_prefixsliceoutput_table)) * S ((dst_positive_code_sum_add_prefixsliceoutput_table) + (dst_positive_scale_sum_add_prefixsliceoutput_table)) + ((dst_positive_scale_sum_add_prefixsliceoutput_table) + (dst_positive_scale_sum_add_prefixsliceoutput_table))) + (((dst_negative_code_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)) * S ((dst_negative_code_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)) + ((dst_negative_scale_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)))) * S ((((dst_positive_code_sum_add_prefixsliceoutput_table) + (dst_positive_scale_sum_add_prefixsliceoutput_table)) * S ((dst_positive_code_sum_add_prefixsliceoutput_table) + (dst_positive_scale_sum_add_prefixsliceoutput_table)) + ((dst_positive_scale_sum_add_prefixsliceoutput_table) + (dst_positive_scale_sum_add_prefixsliceoutput_table))) + (((dst_negative_code_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)) * S ((dst_negative_code_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)) + ((dst_negative_scale_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)))) + ((((dst_negative_code_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)) * S ((dst_negative_code_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)) + ((dst_negative_scale_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table))) + (((dst_negative_code_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)) * S ((dst_negative_code_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)) + ((dst_negative_scale_sum_add_prefixsliceoutput_table) + (dst_negative_scale_sum_add_prefixsliceoutput_table)))))) /\ (forall dst_index_sum_add_prefixsliceoutput_table. (exists pvs_le_gap_sum_add_prefixsliceoutput_tabledomain. pvs_le_gap_sum_add_prefixsliceoutput_tabledomain + (dst_index_sum_add_prefixsliceoutput_table) = (l)) -> exists dst_positive_sum_add_prefixsliceoutput_table dst_negative_sum_add_prefixsliceoutput_table dst_value_sum_add_prefixsliceoutput_table. ((((exists ff_h_pvs_sum_add_prefixsliceoutput_tableentrypositive. ff_h_pvs_sum_add_prefixsliceoutput_tableentrypositive + S (dst_positive_sum_add_prefixsliceoutput_table) = S ((S (dst_index_sum_add_prefixsliceoutput_table)) * dst_positive_scale_sum_add_prefixsliceoutput_table)) /\ exists ff_q_pvs_sum_add_prefixsliceoutput_tableentrypositive. dst_positive_code_sum_add_prefixsliceoutput_table = ff_q_pvs_sum_add_prefixsliceoutput_tableentrypositive * S ((S (dst_index_sum_add_prefixsliceoutput_table)) * dst_positive_scale_sum_add_prefixsliceoutput_table) + (dst_positive_sum_add_prefixsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_add_prefixsliceoutput_tableentrynegative. ff_h_pvs_sum_add_prefixsliceoutput_tableentrynegative + S (dst_negative_sum_add_prefixsliceoutput_table) = S ((S (dst_index_sum_add_prefixsliceoutput_table)) * dst_negative_scale_sum_add_prefixsliceoutput_table)) /\ exists ff_q_pvs_sum_add_prefixsliceoutput_tableentrynegative. dst_negative_code_sum_add_prefixsliceoutput_table = ff_q_pvs_sum_add_prefixsliceoutput_tableentrynegative * S ((S (dst_index_sum_add_prefixsliceoutput_table)) * dst_negative_scale_sum_add_prefixsliceoutput_table) + (dst_negative_sum_add_prefixsliceoutput_table))) /\ (exists ge_balance_positive_sum_add_prefixsliceoutput_tableentryvalue ge_balance_negative_sum_add_prefixsliceoutput_tableentryvalue. (((((dst_value_sum_add_prefixsliceoutput_table) = 2 * (ge_balance_positive_sum_add_prefixsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_add_prefixsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_add_prefixsliceoutput_tableentryvaluedecode. (((dst_value_sum_add_prefixsliceoutput_table) = 2 * ge_signed_half_sum_add_prefixsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_add_prefixsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_add_prefixsliceoutput_tableentryvalue) = S ge_signed_half_sum_add_prefixsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_add_prefixsliceoutput_table) + ge_balance_negative_sum_add_prefixsliceoutput_tableentryvalue = (dst_negative_sum_add_prefixsliceoutput_table) + ge_balance_positive_sum_add_prefixsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_add_prefixslice. (exists pvs_gap_sum_add_prefixslicebound. pvs_gap_sum_add_prefixslicebound + S (srs_index_sum_add_prefixslice) = (l)) -> exists srs_value_sum_add_prefixslice. (((exists dst_positive_code_sum_add_prefixsliceentrysource dst_positive_scale_sum_add_prefixsliceentrysource dst_negative_code_sum_add_prefixsliceentrysource dst_negative_scale_sum_add_prefixsliceentrysource dst_positive_sum_add_prefixsliceentrysource dst_negative_sum_add_prefixsliceentrysource. (((F) = (((((dst_positive_code_sum_add_prefixsliceentrysource) + (dst_positive_scale_sum_add_prefixsliceentrysource)) * S ((dst_positive_code_sum_add_prefixsliceentrysource) + (dst_positive_scale_sum_add_prefixsliceentrysource)) + ((dst_positive_scale_sum_add_prefixsliceentrysource) + (dst_positive_scale_sum_add_prefixsliceentrysource))) + (((dst_negative_code_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)) * S ((dst_negative_code_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)) + ((dst_negative_scale_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)))) * S ((((dst_positive_code_sum_add_prefixsliceentrysource) + (dst_positive_scale_sum_add_prefixsliceentrysource)) * S ((dst_positive_code_sum_add_prefixsliceentrysource) + (dst_positive_scale_sum_add_prefixsliceentrysource)) + ((dst_positive_scale_sum_add_prefixsliceentrysource) + (dst_positive_scale_sum_add_prefixsliceentrysource))) + (((dst_negative_code_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)) * S ((dst_negative_code_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)) + ((dst_negative_scale_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)))) + ((((dst_negative_code_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)) * S ((dst_negative_code_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)) + ((dst_negative_scale_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource))) + (((dst_negative_code_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)) * S ((dst_negative_code_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)) + ((dst_negative_scale_sum_add_prefixsliceentrysource) + (dst_negative_scale_sum_add_prefixsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_add_prefixsliceentrysourcepositive. ff_h_pvs_sum_add_prefixsliceentrysourcepositive + S (dst_positive_sum_add_prefixsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_add_prefixslice))))) * dst_positive_scale_sum_add_prefixsliceentrysource)) /\ exists ff_q_pvs_sum_add_prefixsliceentrysourcepositive. dst_positive_code_sum_add_prefixsliceentrysource = ff_q_pvs_sum_add_prefixsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_add_prefixslice))))) * dst_positive_scale_sum_add_prefixsliceentrysource) + (dst_positive_sum_add_prefixsliceentrysource))) /\ (((((exists ff_h_pvs_sum_add_prefixsliceentrysourcenegative. ff_h_pvs_sum_add_prefixsliceentrysourcenegative + S (dst_negative_sum_add_prefixsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_add_prefixslice))))) * dst_negative_scale_sum_add_prefixsliceentrysource)) /\ exists ff_q_pvs_sum_add_prefixsliceentrysourcenegative. dst_negative_code_sum_add_prefixsliceentrysource = ff_q_pvs_sum_add_prefixsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_add_prefixslice))))) * dst_negative_scale_sum_add_prefixsliceentrysource) + (dst_negative_sum_add_prefixsliceentrysource))) /\ (exists ge_balance_positive_sum_add_prefixsliceentrysourcevalue ge_balance_negative_sum_add_prefixsliceentrysourcevalue. (((((srs_value_sum_add_prefixslice) = 2 * (ge_balance_positive_sum_add_prefixsliceentrysourcevalue) /\ (ge_balance_negative_sum_add_prefixsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_add_prefixsliceentrysourcevaluedecode. (((srs_value_sum_add_prefixslice) = 2 * ge_signed_half_sum_add_prefixsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_add_prefixsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_add_prefixsliceentrysourcevalue) = S ge_signed_half_sum_add_prefixsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_add_prefixsliceentrysource) + ge_balance_negative_sum_add_prefixsliceentrysourcevalue = (dst_negative_sum_add_prefixsliceentrysource) + ge_balance_positive_sum_add_prefixsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_add_prefixsliceentryoutput dst_positive_scale_sum_add_prefixsliceentryoutput dst_negative_code_sum_add_prefixsliceentryoutput dst_negative_scale_sum_add_prefixsliceentryoutput dst_positive_sum_add_prefixsliceentryoutput dst_negative_sum_add_prefixsliceentryoutput. (((srs_slice_sum_add_prefix) = (((((dst_positive_code_sum_add_prefixsliceentryoutput) + (dst_positive_scale_sum_add_prefixsliceentryoutput)) * S ((dst_positive_code_sum_add_prefixsliceentryoutput) + (dst_positive_scale_sum_add_prefixsliceentryoutput)) + ((dst_positive_scale_sum_add_prefixsliceentryoutput) + (dst_positive_scale_sum_add_prefixsliceentryoutput))) + (((dst_negative_code_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)) * S ((dst_negative_code_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)) + ((dst_negative_scale_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)))) * S ((((dst_positive_code_sum_add_prefixsliceentryoutput) + (dst_positive_scale_sum_add_prefixsliceentryoutput)) * S ((dst_positive_code_sum_add_prefixsliceentryoutput) + (dst_positive_scale_sum_add_prefixsliceentryoutput)) + ((dst_positive_scale_sum_add_prefixsliceentryoutput) + (dst_positive_scale_sum_add_prefixsliceentryoutput))) + (((dst_negative_code_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)) * S ((dst_negative_code_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)) + ((dst_negative_scale_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)))) + ((((dst_negative_code_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)) * S ((dst_negative_code_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)) + ((dst_negative_scale_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput))) + (((dst_negative_code_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)) * S ((dst_negative_code_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)) + ((dst_negative_scale_sum_add_prefixsliceentryoutput) + (dst_negative_scale_sum_add_prefixsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_add_prefixsliceentryoutputpositive. ff_h_pvs_sum_add_prefixsliceentryoutputpositive + S (dst_positive_sum_add_prefixsliceentryoutput) = S ((S (srs_index_sum_add_prefixslice)) * dst_positive_scale_sum_add_prefixsliceentryoutput)) /\ exists ff_q_pvs_sum_add_prefixsliceentryoutputpositive. dst_positive_code_sum_add_prefixsliceentryoutput = ff_q_pvs_sum_add_prefixsliceentryoutputpositive * S ((S (srs_index_sum_add_prefixslice)) * dst_positive_scale_sum_add_prefixsliceentryoutput) + (dst_positive_sum_add_prefixsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_add_prefixsliceentryoutputnegative. ff_h_pvs_sum_add_prefixsliceentryoutputnegative + S (dst_negative_sum_add_prefixsliceentryoutput) = S ((S (srs_index_sum_add_prefixslice)) * dst_negative_scale_sum_add_prefixsliceentryoutput)) /\ exists ff_q_pvs_sum_add_prefixsliceentryoutputnegative. dst_negative_code_sum_add_prefixsliceentryoutput = ff_q_pvs_sum_add_prefixsliceentryoutputnegative * S ((S (srs_index_sum_add_prefixslice)) * dst_negative_scale_sum_add_prefixsliceentryoutput) + (dst_negative_sum_add_prefixsliceentryoutput))) /\ (exists ge_balance_positive_sum_add_prefixsliceentryoutputvalue ge_balance_negative_sum_add_prefixsliceentryoutputvalue. (((((srs_value_sum_add_prefixslice) = 2 * (ge_balance_positive_sum_add_prefixsliceentryoutputvalue) /\ (ge_balance_negative_sum_add_prefixsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_add_prefixsliceentryoutputvaluedecode. (((srs_value_sum_add_prefixslice) = 2 * ge_signed_half_sum_add_prefixsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_add_prefixsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_add_prefixsliceentryoutputvalue) = S ge_signed_half_sum_add_prefixsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_add_prefixsliceentryoutput) + ge_balance_negative_sum_add_prefixsliceentryoutputvalue = (dst_negative_sum_add_prefixsliceentryoutput) + ge_balance_positive_sum_add_prefixsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_add_prefixsum dst_positive_scale_sum_add_prefixsum dst_negative_code_sum_add_prefixsum dst_negative_scale_sum_add_prefixsum dst_positive_sum_sum_add_prefixsum dst_negative_sum_sum_add_prefixsum. (((srs_slice_sum_add_prefix) = (((((dst_positive_code_sum_add_prefixsum) + (dst_positive_scale_sum_add_prefixsum)) * S ((dst_positive_code_sum_add_prefixsum) + (dst_positive_scale_sum_add_prefixsum)) + ((dst_positive_scale_sum_add_prefixsum) + (dst_positive_scale_sum_add_prefixsum))) + (((dst_negative_code_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)) * S ((dst_negative_code_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)) + ((dst_negative_scale_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)))) * S ((((dst_positive_code_sum_add_prefixsum) + (dst_positive_scale_sum_add_prefixsum)) * S ((dst_positive_code_sum_add_prefixsum) + (dst_positive_scale_sum_add_prefixsum)) + ((dst_positive_scale_sum_add_prefixsum) + (dst_positive_scale_sum_add_prefixsum))) + (((dst_negative_code_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)) * S ((dst_negative_code_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)) + ((dst_negative_scale_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)))) + ((((dst_negative_code_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)) * S ((dst_negative_code_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)) + ((dst_negative_scale_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum))) + (((dst_negative_code_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)) * S ((dst_negative_code_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)) + ((dst_negative_scale_sum_add_prefixsum) + (dst_negative_scale_sum_add_prefixsum)))))) /\ (((exists fs_u_dst_sum_add_prefixsumpositive fs_v_dst_sum_add_prefixsumpositive. ((((exists fs_h_dst_sum_add_prefixsumpositive_body_start. fs_h_dst_sum_add_prefixsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_add_prefixsumpositive)) /\ exists fs_q_dst_sum_add_prefixsumpositive_body_start. fs_u_dst_sum_add_prefixsumpositive = fs_q_dst_sum_add_prefixsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_add_prefixsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_add_prefixsumpositive_body_terminal. fs_h_dst_sum_add_prefixsumpositive_body_terminal + S (dst_positive_sum_sum_add_prefixsum) = S ((S (l)) * fs_v_dst_sum_add_prefixsumpositive)) /\ exists fs_q_dst_sum_add_prefixsumpositive_body_terminal. fs_u_dst_sum_add_prefixsumpositive = fs_q_dst_sum_add_prefixsumpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_add_prefixsumpositive) + (dst_positive_sum_sum_add_prefixsum))) /\ forall fs_i_dst_sum_add_prefixsumpositive_body_steps. (exists fs_lt_dst_sum_add_prefixsumpositive_body_steps_bound. fs_lt_dst_sum_add_prefixsumpositive_body_steps_bound + S fs_i_dst_sum_add_prefixsumpositive_body_steps = l) -> exists fs_a_dst_sum_add_prefixsumpositive_body_steps fs_r_dst_sum_add_prefixsumpositive_body_steps fs_s_dst_sum_add_prefixsumpositive_body_steps. ((((exists fs_h_dst_sum_add_prefixsumpositive_body_steps_summand. fs_h_dst_sum_add_prefixsumpositive_body_steps_summand + S (fs_a_dst_sum_add_prefixsumpositive_body_steps) = S ((S (fs_i_dst_sum_add_prefixsumpositive_body_steps)) * dst_positive_scale_sum_add_prefixsum)) /\ exists fs_q_dst_sum_add_prefixsumpositive_body_steps_summand. dst_positive_code_sum_add_prefixsum = fs_q_dst_sum_add_prefixsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_add_prefixsumpositive_body_steps)) * dst_positive_scale_sum_add_prefixsum) + (fs_a_dst_sum_add_prefixsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_add_prefixsumpositive_body_steps_partial. fs_h_dst_sum_add_prefixsumpositive_body_steps_partial + S (fs_r_dst_sum_add_prefixsumpositive_body_steps) = S ((S (fs_i_dst_sum_add_prefixsumpositive_body_steps)) * fs_v_dst_sum_add_prefixsumpositive)) /\ exists fs_q_dst_sum_add_prefixsumpositive_body_steps_partial. fs_u_dst_sum_add_prefixsumpositive = fs_q_dst_sum_add_prefixsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_add_prefixsumpositive_body_steps)) * fs_v_dst_sum_add_prefixsumpositive) + (fs_r_dst_sum_add_prefixsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_add_prefixsumpositive_body_steps_successor. fs_h_dst_sum_add_prefixsumpositive_body_steps_successor + S (fs_s_dst_sum_add_prefixsumpositive_body_steps) = S ((S (S fs_i_dst_sum_add_prefixsumpositive_body_steps)) * fs_v_dst_sum_add_prefixsumpositive)) /\ exists fs_q_dst_sum_add_prefixsumpositive_body_steps_successor. fs_u_dst_sum_add_prefixsumpositive = fs_q_dst_sum_add_prefixsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_add_prefixsumpositive_body_steps)) * fs_v_dst_sum_add_prefixsumpositive) + (fs_s_dst_sum_add_prefixsumpositive_body_steps))) /\ fs_s_dst_sum_add_prefixsumpositive_body_steps = fs_r_dst_sum_add_prefixsumpositive_body_steps + fs_a_dst_sum_add_prefixsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_add_prefixsumnegative fs_v_dst_sum_add_prefixsumnegative. ((((exists fs_h_dst_sum_add_prefixsumnegative_body_start. fs_h_dst_sum_add_prefixsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_add_prefixsumnegative)) /\ exists fs_q_dst_sum_add_prefixsumnegative_body_start. fs_u_dst_sum_add_prefixsumnegative = fs_q_dst_sum_add_prefixsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_add_prefixsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_add_prefixsumnegative_body_terminal. fs_h_dst_sum_add_prefixsumnegative_body_terminal + S (dst_negative_sum_sum_add_prefixsum) = S ((S (l)) * fs_v_dst_sum_add_prefixsumnegative)) /\ exists fs_q_dst_sum_add_prefixsumnegative_body_terminal. fs_u_dst_sum_add_prefixsumnegative = fs_q_dst_sum_add_prefixsumnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_add_prefixsumnegative) + (dst_negative_sum_sum_add_prefixsum))) /\ forall fs_i_dst_sum_add_prefixsumnegative_body_steps. (exists fs_lt_dst_sum_add_prefixsumnegative_body_steps_bound. fs_lt_dst_sum_add_prefixsumnegative_body_steps_bound + S fs_i_dst_sum_add_prefixsumnegative_body_steps = l) -> exists fs_a_dst_sum_add_prefixsumnegative_body_steps fs_r_dst_sum_add_prefixsumnegative_body_steps fs_s_dst_sum_add_prefixsumnegative_body_steps. ((((exists fs_h_dst_sum_add_prefixsumnegative_body_steps_summand. fs_h_dst_sum_add_prefixsumnegative_body_steps_summand + S (fs_a_dst_sum_add_prefixsumnegative_body_steps) = S ((S (fs_i_dst_sum_add_prefixsumnegative_body_steps)) * dst_negative_scale_sum_add_prefixsum)) /\ exists fs_q_dst_sum_add_prefixsumnegative_body_steps_summand. dst_negative_code_sum_add_prefixsum = fs_q_dst_sum_add_prefixsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_add_prefixsumnegative_body_steps)) * dst_negative_scale_sum_add_prefixsum) + (fs_a_dst_sum_add_prefixsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_add_prefixsumnegative_body_steps_partial. fs_h_dst_sum_add_prefixsumnegative_body_steps_partial + S (fs_r_dst_sum_add_prefixsumnegative_body_steps) = S ((S (fs_i_dst_sum_add_prefixsumnegative_body_steps)) * fs_v_dst_sum_add_prefixsumnegative)) /\ exists fs_q_dst_sum_add_prefixsumnegative_body_steps_partial. fs_u_dst_sum_add_prefixsumnegative = fs_q_dst_sum_add_prefixsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_add_prefixsumnegative_body_steps)) * fs_v_dst_sum_add_prefixsumnegative) + (fs_r_dst_sum_add_prefixsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_add_prefixsumnegative_body_steps_successor. fs_h_dst_sum_add_prefixsumnegative_body_steps_successor + S (fs_s_dst_sum_add_prefixsumnegative_body_steps) = S ((S (S fs_i_dst_sum_add_prefixsumnegative_body_steps)) * fs_v_dst_sum_add_prefixsumnegative)) /\ exists fs_q_dst_sum_add_prefixsumnegative_body_steps_successor. fs_u_dst_sum_add_prefixsumnegative = fs_q_dst_sum_add_prefixsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_add_prefixsumnegative_body_steps)) * fs_v_dst_sum_add_prefixsumnegative) + (fs_s_dst_sum_add_prefixsumnegative_body_steps))) /\ fs_s_dst_sum_add_prefixsumnegative_body_steps = fs_r_dst_sum_add_prefixsumnegative_body_steps + fs_a_dst_sum_add_prefixsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_add_prefixsumresult ge_balance_negative_sum_add_prefixsumresult. (((((a) = 2 * (ge_balance_positive_sum_add_prefixsumresult) /\ (ge_balance_negative_sum_add_prefixsumresult) = 0) \/ exists ge_signed_half_sum_add_prefixsumresultdecode. (((a) = 2 * ge_signed_half_sum_add_prefixsumresultdecode + 1 /\ (ge_balance_positive_sum_add_prefixsumresult) = 0) /\ (ge_balance_negative_sum_add_prefixsumresult) = S ge_signed_half_sum_add_prefixsumresultdecode))) /\ ((dst_positive_sum_sum_add_prefixsum) + ge_balance_negative_sum_add_prefixsumresult = (dst_negative_sum_sum_add_prefixsum) + ge_balance_positive_sum_add_prefixsumresult))))))))))) -> (exists dst_positive_code_sum_add_source dst_positive_scale_sum_add_source dst_negative_code_sum_add_source dst_negative_scale_sum_add_source dst_positive_sum_add_source dst_negative_sum_add_source. (((F) = (((((dst_positive_code_sum_add_source) + (dst_positive_scale_sum_add_source)) * S ((dst_positive_code_sum_add_source) + (dst_positive_scale_sum_add_source)) + ((dst_positive_scale_sum_add_source) + (dst_positive_scale_sum_add_source))) + (((dst_negative_code_sum_add_source) + (dst_negative_scale_sum_add_source)) * S ((dst_negative_code_sum_add_source) + (dst_negative_scale_sum_add_source)) + ((dst_negative_scale_sum_add_source) + (dst_negative_scale_sum_add_source)))) * S ((((dst_positive_code_sum_add_source) + (dst_positive_scale_sum_add_source)) * S ((dst_positive_code_sum_add_source) + (dst_positive_scale_sum_add_source)) + ((dst_positive_scale_sum_add_source) + (dst_positive_scale_sum_add_source))) + (((dst_negative_code_sum_add_source) + (dst_negative_scale_sum_add_source)) * S ((dst_negative_code_sum_add_source) + (dst_negative_scale_sum_add_source)) + ((dst_negative_scale_sum_add_source) + (dst_negative_scale_sum_add_source)))) + ((((dst_negative_code_sum_add_source) + (dst_negative_scale_sum_add_source)) * S ((dst_negative_code_sum_add_source) + (dst_negative_scale_sum_add_source)) + ((dst_negative_scale_sum_add_source) + (dst_negative_scale_sum_add_source))) + (((dst_negative_code_sum_add_source) + (dst_negative_scale_sum_add_source)) * S ((dst_negative_code_sum_add_source) + (dst_negative_scale_sum_add_source)) + ((dst_negative_scale_sum_add_source) + (dst_negative_scale_sum_add_source)))))) /\ (((((exists ff_h_pvs_sum_add_sourcepositive. ff_h_pvs_sum_add_sourcepositive + S (dst_positive_sum_add_source) = S ((S (((o) + ((s) * (l))))) * dst_positive_scale_sum_add_source)) /\ exists ff_q_pvs_sum_add_sourcepositive. dst_positive_code_sum_add_source = ff_q_pvs_sum_add_sourcepositive * S ((S (((o) + ((s) * (l))))) * dst_positive_scale_sum_add_source) + (dst_positive_sum_add_source))) /\ (((((exists ff_h_pvs_sum_add_sourcenegative. ff_h_pvs_sum_add_sourcenegative + S (dst_negative_sum_add_source) = S ((S (((o) + ((s) * (l))))) * dst_negative_scale_sum_add_source)) /\ exists ff_q_pvs_sum_add_sourcenegative. dst_negative_code_sum_add_source = ff_q_pvs_sum_add_sourcenegative * S ((S (((o) + ((s) * (l))))) * dst_negative_scale_sum_add_source) + (dst_negative_sum_add_source))) /\ (exists ge_balance_positive_sum_add_sourcevalue ge_balance_negative_sum_add_sourcevalue. (((((b) = 2 * (ge_balance_positive_sum_add_sourcevalue) /\ (ge_balance_negative_sum_add_sourcevalue) = 0) \/ exists ge_signed_half_sum_add_sourcevaluedecode. (((b) = 2 * ge_signed_half_sum_add_sourcevaluedecode + 1 /\ (ge_balance_positive_sum_add_sourcevalue) = 0) /\ (ge_balance_negative_sum_add_sourcevalue) = S ge_signed_half_sum_add_sourcevaluedecode))) /\ ((dst_positive_sum_add_source) + ge_balance_negative_sum_add_sourcevalue = (dst_negative_sum_add_source) + ge_balance_positive_sum_add_sourcevalue))))))))) -> (exists srs_slice_sum_add_next. ((((exists dst_positive_code_sum_add_nextslicesource_table dst_positive_scale_sum_add_nextslicesource_table dst_negative_code_sum_add_nextslicesource_table dst_negative_scale_sum_add_nextslicesource_table. (((F) = (((((dst_positive_code_sum_add_nextslicesource_table) + (dst_positive_scale_sum_add_nextslicesource_table)) * S ((dst_positive_code_sum_add_nextslicesource_table) + (dst_positive_scale_sum_add_nextslicesource_table)) + ((dst_positive_scale_sum_add_nextslicesource_table) + (dst_positive_scale_sum_add_nextslicesource_table))) + (((dst_negative_code_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)) * S ((dst_negative_code_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)) + ((dst_negative_scale_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)))) * S ((((dst_positive_code_sum_add_nextslicesource_table) + (dst_positive_scale_sum_add_nextslicesource_table)) * S ((dst_positive_code_sum_add_nextslicesource_table) + (dst_positive_scale_sum_add_nextslicesource_table)) + ((dst_positive_scale_sum_add_nextslicesource_table) + (dst_positive_scale_sum_add_nextslicesource_table))) + (((dst_negative_code_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)) * S ((dst_negative_code_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)) + ((dst_negative_scale_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)))) + ((((dst_negative_code_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)) * S ((dst_negative_code_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)) + ((dst_negative_scale_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table))) + (((dst_negative_code_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)) * S ((dst_negative_code_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)) + ((dst_negative_scale_sum_add_nextslicesource_table) + (dst_negative_scale_sum_add_nextslicesource_table)))))) /\ (forall dst_index_sum_add_nextslicesource_table. (exists pvs_le_gap_sum_add_nextslicesource_tabledomain. pvs_le_gap_sum_add_nextslicesource_tabledomain + (dst_index_sum_add_nextslicesource_table) = (0)) -> exists dst_positive_sum_add_nextslicesource_table dst_negative_sum_add_nextslicesource_table dst_value_sum_add_nextslicesource_table. ((((exists ff_h_pvs_sum_add_nextslicesource_tableentrypositive. ff_h_pvs_sum_add_nextslicesource_tableentrypositive + S (dst_positive_sum_add_nextslicesource_table) = S ((S (dst_index_sum_add_nextslicesource_table)) * dst_positive_scale_sum_add_nextslicesource_table)) /\ exists ff_q_pvs_sum_add_nextslicesource_tableentrypositive. dst_positive_code_sum_add_nextslicesource_table = ff_q_pvs_sum_add_nextslicesource_tableentrypositive * S ((S (dst_index_sum_add_nextslicesource_table)) * dst_positive_scale_sum_add_nextslicesource_table) + (dst_positive_sum_add_nextslicesource_table))) /\ (((((exists ff_h_pvs_sum_add_nextslicesource_tableentrynegative. ff_h_pvs_sum_add_nextslicesource_tableentrynegative + S (dst_negative_sum_add_nextslicesource_table) = S ((S (dst_index_sum_add_nextslicesource_table)) * dst_negative_scale_sum_add_nextslicesource_table)) /\ exists ff_q_pvs_sum_add_nextslicesource_tableentrynegative. dst_negative_code_sum_add_nextslicesource_table = ff_q_pvs_sum_add_nextslicesource_tableentrynegative * S ((S (dst_index_sum_add_nextslicesource_table)) * dst_negative_scale_sum_add_nextslicesource_table) + (dst_negative_sum_add_nextslicesource_table))) /\ (exists ge_balance_positive_sum_add_nextslicesource_tableentryvalue ge_balance_negative_sum_add_nextslicesource_tableentryvalue. (((((dst_value_sum_add_nextslicesource_table) = 2 * (ge_balance_positive_sum_add_nextslicesource_tableentryvalue) /\ (ge_balance_negative_sum_add_nextslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_add_nextslicesource_tableentryvaluedecode. (((dst_value_sum_add_nextslicesource_table) = 2 * ge_signed_half_sum_add_nextslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_add_nextslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_add_nextslicesource_tableentryvalue) = S ge_signed_half_sum_add_nextslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_add_nextslicesource_table) + ge_balance_negative_sum_add_nextslicesource_tableentryvalue = (dst_negative_sum_add_nextslicesource_table) + ge_balance_positive_sum_add_nextslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_add_nextsliceoutput_table dst_positive_scale_sum_add_nextsliceoutput_table dst_negative_code_sum_add_nextsliceoutput_table dst_negative_scale_sum_add_nextsliceoutput_table. (((srs_slice_sum_add_next) = (((((dst_positive_code_sum_add_nextsliceoutput_table) + (dst_positive_scale_sum_add_nextsliceoutput_table)) * S ((dst_positive_code_sum_add_nextsliceoutput_table) + (dst_positive_scale_sum_add_nextsliceoutput_table)) + ((dst_positive_scale_sum_add_nextsliceoutput_table) + (dst_positive_scale_sum_add_nextsliceoutput_table))) + (((dst_negative_code_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)) * S ((dst_negative_code_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)) + ((dst_negative_scale_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)))) * S ((((dst_positive_code_sum_add_nextsliceoutput_table) + (dst_positive_scale_sum_add_nextsliceoutput_table)) * S ((dst_positive_code_sum_add_nextsliceoutput_table) + (dst_positive_scale_sum_add_nextsliceoutput_table)) + ((dst_positive_scale_sum_add_nextsliceoutput_table) + (dst_positive_scale_sum_add_nextsliceoutput_table))) + (((dst_negative_code_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)) * S ((dst_negative_code_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)) + ((dst_negative_scale_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)))) + ((((dst_negative_code_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)) * S ((dst_negative_code_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)) + ((dst_negative_scale_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table))) + (((dst_negative_code_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)) * S ((dst_negative_code_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)) + ((dst_negative_scale_sum_add_nextsliceoutput_table) + (dst_negative_scale_sum_add_nextsliceoutput_table)))))) /\ (forall dst_index_sum_add_nextsliceoutput_table. (exists pvs_le_gap_sum_add_nextsliceoutput_tabledomain. pvs_le_gap_sum_add_nextsliceoutput_tabledomain + (dst_index_sum_add_nextsliceoutput_table) = (S l)) -> exists dst_positive_sum_add_nextsliceoutput_table dst_negative_sum_add_nextsliceoutput_table dst_value_sum_add_nextsliceoutput_table. ((((exists ff_h_pvs_sum_add_nextsliceoutput_tableentrypositive. ff_h_pvs_sum_add_nextsliceoutput_tableentrypositive + S (dst_positive_sum_add_nextsliceoutput_table) = S ((S (dst_index_sum_add_nextsliceoutput_table)) * dst_positive_scale_sum_add_nextsliceoutput_table)) /\ exists ff_q_pvs_sum_add_nextsliceoutput_tableentrypositive. dst_positive_code_sum_add_nextsliceoutput_table = ff_q_pvs_sum_add_nextsliceoutput_tableentrypositive * S ((S (dst_index_sum_add_nextsliceoutput_table)) * dst_positive_scale_sum_add_nextsliceoutput_table) + (dst_positive_sum_add_nextsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_add_nextsliceoutput_tableentrynegative. ff_h_pvs_sum_add_nextsliceoutput_tableentrynegative + S (dst_negative_sum_add_nextsliceoutput_table) = S ((S (dst_index_sum_add_nextsliceoutput_table)) * dst_negative_scale_sum_add_nextsliceoutput_table)) /\ exists ff_q_pvs_sum_add_nextsliceoutput_tableentrynegative. dst_negative_code_sum_add_nextsliceoutput_table = ff_q_pvs_sum_add_nextsliceoutput_tableentrynegative * S ((S (dst_index_sum_add_nextsliceoutput_table)) * dst_negative_scale_sum_add_nextsliceoutput_table) + (dst_negative_sum_add_nextsliceoutput_table))) /\ (exists ge_balance_positive_sum_add_nextsliceoutput_tableentryvalue ge_balance_negative_sum_add_nextsliceoutput_tableentryvalue. (((((dst_value_sum_add_nextsliceoutput_table) = 2 * (ge_balance_positive_sum_add_nextsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_add_nextsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_add_nextsliceoutput_tableentryvaluedecode. (((dst_value_sum_add_nextsliceoutput_table) = 2 * ge_signed_half_sum_add_nextsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_add_nextsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_add_nextsliceoutput_tableentryvalue) = S ge_signed_half_sum_add_nextsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_add_nextsliceoutput_table) + ge_balance_negative_sum_add_nextsliceoutput_tableentryvalue = (dst_negative_sum_add_nextsliceoutput_table) + ge_balance_positive_sum_add_nextsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_add_nextslice. (exists pvs_gap_sum_add_nextslicebound. pvs_gap_sum_add_nextslicebound + S (srs_index_sum_add_nextslice) = (S l)) -> exists srs_value_sum_add_nextslice. (((exists dst_positive_code_sum_add_nextsliceentrysource dst_positive_scale_sum_add_nextsliceentrysource dst_negative_code_sum_add_nextsliceentrysource dst_negative_scale_sum_add_nextsliceentrysource dst_positive_sum_add_nextsliceentrysource dst_negative_sum_add_nextsliceentrysource. (((F) = (((((dst_positive_code_sum_add_nextsliceentrysource) + (dst_positive_scale_sum_add_nextsliceentrysource)) * S ((dst_positive_code_sum_add_nextsliceentrysource) + (dst_positive_scale_sum_add_nextsliceentrysource)) + ((dst_positive_scale_sum_add_nextsliceentrysource) + (dst_positive_scale_sum_add_nextsliceentrysource))) + (((dst_negative_code_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)) * S ((dst_negative_code_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)) + ((dst_negative_scale_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)))) * S ((((dst_positive_code_sum_add_nextsliceentrysource) + (dst_positive_scale_sum_add_nextsliceentrysource)) * S ((dst_positive_code_sum_add_nextsliceentrysource) + (dst_positive_scale_sum_add_nextsliceentrysource)) + ((dst_positive_scale_sum_add_nextsliceentrysource) + (dst_positive_scale_sum_add_nextsliceentrysource))) + (((dst_negative_code_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)) * S ((dst_negative_code_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)) + ((dst_negative_scale_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)))) + ((((dst_negative_code_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)) * S ((dst_negative_code_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)) + ((dst_negative_scale_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource))) + (((dst_negative_code_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)) * S ((dst_negative_code_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)) + ((dst_negative_scale_sum_add_nextsliceentrysource) + (dst_negative_scale_sum_add_nextsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_add_nextsliceentrysourcepositive. ff_h_pvs_sum_add_nextsliceentrysourcepositive + S (dst_positive_sum_add_nextsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_add_nextslice))))) * dst_positive_scale_sum_add_nextsliceentrysource)) /\ exists ff_q_pvs_sum_add_nextsliceentrysourcepositive. dst_positive_code_sum_add_nextsliceentrysource = ff_q_pvs_sum_add_nextsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_add_nextslice))))) * dst_positive_scale_sum_add_nextsliceentrysource) + (dst_positive_sum_add_nextsliceentrysource))) /\ (((((exists ff_h_pvs_sum_add_nextsliceentrysourcenegative. ff_h_pvs_sum_add_nextsliceentrysourcenegative + S (dst_negative_sum_add_nextsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_add_nextslice))))) * dst_negative_scale_sum_add_nextsliceentrysource)) /\ exists ff_q_pvs_sum_add_nextsliceentrysourcenegative. dst_negative_code_sum_add_nextsliceentrysource = ff_q_pvs_sum_add_nextsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_add_nextslice))))) * dst_negative_scale_sum_add_nextsliceentrysource) + (dst_negative_sum_add_nextsliceentrysource))) /\ (exists ge_balance_positive_sum_add_nextsliceentrysourcevalue ge_balance_negative_sum_add_nextsliceentrysourcevalue. (((((srs_value_sum_add_nextslice) = 2 * (ge_balance_positive_sum_add_nextsliceentrysourcevalue) /\ (ge_balance_negative_sum_add_nextsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_add_nextsliceentrysourcevaluedecode. (((srs_value_sum_add_nextslice) = 2 * ge_signed_half_sum_add_nextsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_add_nextsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_add_nextsliceentrysourcevalue) = S ge_signed_half_sum_add_nextsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_add_nextsliceentrysource) + ge_balance_negative_sum_add_nextsliceentrysourcevalue = (dst_negative_sum_add_nextsliceentrysource) + ge_balance_positive_sum_add_nextsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_add_nextsliceentryoutput dst_positive_scale_sum_add_nextsliceentryoutput dst_negative_code_sum_add_nextsliceentryoutput dst_negative_scale_sum_add_nextsliceentryoutput dst_positive_sum_add_nextsliceentryoutput dst_negative_sum_add_nextsliceentryoutput. (((srs_slice_sum_add_next) = (((((dst_positive_code_sum_add_nextsliceentryoutput) + (dst_positive_scale_sum_add_nextsliceentryoutput)) * S ((dst_positive_code_sum_add_nextsliceentryoutput) + (dst_positive_scale_sum_add_nextsliceentryoutput)) + ((dst_positive_scale_sum_add_nextsliceentryoutput) + (dst_positive_scale_sum_add_nextsliceentryoutput))) + (((dst_negative_code_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)) * S ((dst_negative_code_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)) + ((dst_negative_scale_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)))) * S ((((dst_positive_code_sum_add_nextsliceentryoutput) + (dst_positive_scale_sum_add_nextsliceentryoutput)) * S ((dst_positive_code_sum_add_nextsliceentryoutput) + (dst_positive_scale_sum_add_nextsliceentryoutput)) + ((dst_positive_scale_sum_add_nextsliceentryoutput) + (dst_positive_scale_sum_add_nextsliceentryoutput))) + (((dst_negative_code_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)) * S ((dst_negative_code_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)) + ((dst_negative_scale_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)))) + ((((dst_negative_code_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)) * S ((dst_negative_code_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)) + ((dst_negative_scale_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput))) + (((dst_negative_code_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)) * S ((dst_negative_code_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)) + ((dst_negative_scale_sum_add_nextsliceentryoutput) + (dst_negative_scale_sum_add_nextsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_add_nextsliceentryoutputpositive. ff_h_pvs_sum_add_nextsliceentryoutputpositive + S (dst_positive_sum_add_nextsliceentryoutput) = S ((S (srs_index_sum_add_nextslice)) * dst_positive_scale_sum_add_nextsliceentryoutput)) /\ exists ff_q_pvs_sum_add_nextsliceentryoutputpositive. dst_positive_code_sum_add_nextsliceentryoutput = ff_q_pvs_sum_add_nextsliceentryoutputpositive * S ((S (srs_index_sum_add_nextslice)) * dst_positive_scale_sum_add_nextsliceentryoutput) + (dst_positive_sum_add_nextsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_add_nextsliceentryoutputnegative. ff_h_pvs_sum_add_nextsliceentryoutputnegative + S (dst_negative_sum_add_nextsliceentryoutput) = S ((S (srs_index_sum_add_nextslice)) * dst_negative_scale_sum_add_nextsliceentryoutput)) /\ exists ff_q_pvs_sum_add_nextsliceentryoutputnegative. dst_negative_code_sum_add_nextsliceentryoutput = ff_q_pvs_sum_add_nextsliceentryoutputnegative * S ((S (srs_index_sum_add_nextslice)) * dst_negative_scale_sum_add_nextsliceentryoutput) + (dst_negative_sum_add_nextsliceentryoutput))) /\ (exists ge_balance_positive_sum_add_nextsliceentryoutputvalue ge_balance_negative_sum_add_nextsliceentryoutputvalue. (((((srs_value_sum_add_nextslice) = 2 * (ge_balance_positive_sum_add_nextsliceentryoutputvalue) /\ (ge_balance_negative_sum_add_nextsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_add_nextsliceentryoutputvaluedecode. (((srs_value_sum_add_nextslice) = 2 * ge_signed_half_sum_add_nextsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_add_nextsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_add_nextsliceentryoutputvalue) = S ge_signed_half_sum_add_nextsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_add_nextsliceentryoutput) + ge_balance_negative_sum_add_nextsliceentryoutputvalue = (dst_negative_sum_add_nextsliceentryoutput) + ge_balance_positive_sum_add_nextsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_add_nextsum dst_positive_scale_sum_add_nextsum dst_negative_code_sum_add_nextsum dst_negative_scale_sum_add_nextsum dst_positive_sum_sum_add_nextsum dst_negative_sum_sum_add_nextsum. (((srs_slice_sum_add_next) = (((((dst_positive_code_sum_add_nextsum) + (dst_positive_scale_sum_add_nextsum)) * S ((dst_positive_code_sum_add_nextsum) + (dst_positive_scale_sum_add_nextsum)) + ((dst_positive_scale_sum_add_nextsum) + (dst_positive_scale_sum_add_nextsum))) + (((dst_negative_code_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)) * S ((dst_negative_code_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)) + ((dst_negative_scale_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)))) * S ((((dst_positive_code_sum_add_nextsum) + (dst_positive_scale_sum_add_nextsum)) * S ((dst_positive_code_sum_add_nextsum) + (dst_positive_scale_sum_add_nextsum)) + ((dst_positive_scale_sum_add_nextsum) + (dst_positive_scale_sum_add_nextsum))) + (((dst_negative_code_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)) * S ((dst_negative_code_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)) + ((dst_negative_scale_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)))) + ((((dst_negative_code_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)) * S ((dst_negative_code_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)) + ((dst_negative_scale_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum))) + (((dst_negative_code_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)) * S ((dst_negative_code_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)) + ((dst_negative_scale_sum_add_nextsum) + (dst_negative_scale_sum_add_nextsum)))))) /\ (((exists fs_u_dst_sum_add_nextsumpositive fs_v_dst_sum_add_nextsumpositive. ((((exists fs_h_dst_sum_add_nextsumpositive_body_start. fs_h_dst_sum_add_nextsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_add_nextsumpositive)) /\ exists fs_q_dst_sum_add_nextsumpositive_body_start. fs_u_dst_sum_add_nextsumpositive = fs_q_dst_sum_add_nextsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_add_nextsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_add_nextsumpositive_body_terminal. fs_h_dst_sum_add_nextsumpositive_body_terminal + S (dst_positive_sum_sum_add_nextsum) = S ((S (S l)) * fs_v_dst_sum_add_nextsumpositive)) /\ exists fs_q_dst_sum_add_nextsumpositive_body_terminal. fs_u_dst_sum_add_nextsumpositive = fs_q_dst_sum_add_nextsumpositive_body_terminal * S ((S (S l)) * fs_v_dst_sum_add_nextsumpositive) + (dst_positive_sum_sum_add_nextsum))) /\ forall fs_i_dst_sum_add_nextsumpositive_body_steps. (exists fs_lt_dst_sum_add_nextsumpositive_body_steps_bound. fs_lt_dst_sum_add_nextsumpositive_body_steps_bound + S fs_i_dst_sum_add_nextsumpositive_body_steps = S l) -> exists fs_a_dst_sum_add_nextsumpositive_body_steps fs_r_dst_sum_add_nextsumpositive_body_steps fs_s_dst_sum_add_nextsumpositive_body_steps. ((((exists fs_h_dst_sum_add_nextsumpositive_body_steps_summand. fs_h_dst_sum_add_nextsumpositive_body_steps_summand + S (fs_a_dst_sum_add_nextsumpositive_body_steps) = S ((S (fs_i_dst_sum_add_nextsumpositive_body_steps)) * dst_positive_scale_sum_add_nextsum)) /\ exists fs_q_dst_sum_add_nextsumpositive_body_steps_summand. dst_positive_code_sum_add_nextsum = fs_q_dst_sum_add_nextsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_add_nextsumpositive_body_steps)) * dst_positive_scale_sum_add_nextsum) + (fs_a_dst_sum_add_nextsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_add_nextsumpositive_body_steps_partial. fs_h_dst_sum_add_nextsumpositive_body_steps_partial + S (fs_r_dst_sum_add_nextsumpositive_body_steps) = S ((S (fs_i_dst_sum_add_nextsumpositive_body_steps)) * fs_v_dst_sum_add_nextsumpositive)) /\ exists fs_q_dst_sum_add_nextsumpositive_body_steps_partial. fs_u_dst_sum_add_nextsumpositive = fs_q_dst_sum_add_nextsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_add_nextsumpositive_body_steps)) * fs_v_dst_sum_add_nextsumpositive) + (fs_r_dst_sum_add_nextsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_add_nextsumpositive_body_steps_successor. fs_h_dst_sum_add_nextsumpositive_body_steps_successor + S (fs_s_dst_sum_add_nextsumpositive_body_steps) = S ((S (S fs_i_dst_sum_add_nextsumpositive_body_steps)) * fs_v_dst_sum_add_nextsumpositive)) /\ exists fs_q_dst_sum_add_nextsumpositive_body_steps_successor. fs_u_dst_sum_add_nextsumpositive = fs_q_dst_sum_add_nextsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_add_nextsumpositive_body_steps)) * fs_v_dst_sum_add_nextsumpositive) + (fs_s_dst_sum_add_nextsumpositive_body_steps))) /\ fs_s_dst_sum_add_nextsumpositive_body_steps = fs_r_dst_sum_add_nextsumpositive_body_steps + fs_a_dst_sum_add_nextsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_add_nextsumnegative fs_v_dst_sum_add_nextsumnegative. ((((exists fs_h_dst_sum_add_nextsumnegative_body_start. fs_h_dst_sum_add_nextsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_add_nextsumnegative)) /\ exists fs_q_dst_sum_add_nextsumnegative_body_start. fs_u_dst_sum_add_nextsumnegative = fs_q_dst_sum_add_nextsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_add_nextsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_add_nextsumnegative_body_terminal. fs_h_dst_sum_add_nextsumnegative_body_terminal + S (dst_negative_sum_sum_add_nextsum) = S ((S (S l)) * fs_v_dst_sum_add_nextsumnegative)) /\ exists fs_q_dst_sum_add_nextsumnegative_body_terminal. fs_u_dst_sum_add_nextsumnegative = fs_q_dst_sum_add_nextsumnegative_body_terminal * S ((S (S l)) * fs_v_dst_sum_add_nextsumnegative) + (dst_negative_sum_sum_add_nextsum))) /\ forall fs_i_dst_sum_add_nextsumnegative_body_steps. (exists fs_lt_dst_sum_add_nextsumnegative_body_steps_bound. fs_lt_dst_sum_add_nextsumnegative_body_steps_bound + S fs_i_dst_sum_add_nextsumnegative_body_steps = S l) -> exists fs_a_dst_sum_add_nextsumnegative_body_steps fs_r_dst_sum_add_nextsumnegative_body_steps fs_s_dst_sum_add_nextsumnegative_body_steps. ((((exists fs_h_dst_sum_add_nextsumnegative_body_steps_summand. fs_h_dst_sum_add_nextsumnegative_body_steps_summand + S (fs_a_dst_sum_add_nextsumnegative_body_steps) = S ((S (fs_i_dst_sum_add_nextsumnegative_body_steps)) * dst_negative_scale_sum_add_nextsum)) /\ exists fs_q_dst_sum_add_nextsumnegative_body_steps_summand. dst_negative_code_sum_add_nextsum = fs_q_dst_sum_add_nextsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_add_nextsumnegative_body_steps)) * dst_negative_scale_sum_add_nextsum) + (fs_a_dst_sum_add_nextsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_add_nextsumnegative_body_steps_partial. fs_h_dst_sum_add_nextsumnegative_body_steps_partial + S (fs_r_dst_sum_add_nextsumnegative_body_steps) = S ((S (fs_i_dst_sum_add_nextsumnegative_body_steps)) * fs_v_dst_sum_add_nextsumnegative)) /\ exists fs_q_dst_sum_add_nextsumnegative_body_steps_partial. fs_u_dst_sum_add_nextsumnegative = fs_q_dst_sum_add_nextsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_add_nextsumnegative_body_steps)) * fs_v_dst_sum_add_nextsumnegative) + (fs_r_dst_sum_add_nextsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_add_nextsumnegative_body_steps_successor. fs_h_dst_sum_add_nextsumnegative_body_steps_successor + S (fs_s_dst_sum_add_nextsumnegative_body_steps) = S ((S (S fs_i_dst_sum_add_nextsumnegative_body_steps)) * fs_v_dst_sum_add_nextsumnegative)) /\ exists fs_q_dst_sum_add_nextsumnegative_body_steps_successor. fs_u_dst_sum_add_nextsumnegative = fs_q_dst_sum_add_nextsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_add_nextsumnegative_body_steps)) * fs_v_dst_sum_add_nextsumnegative) + (fs_s_dst_sum_add_nextsumnegative_body_steps))) /\ fs_s_dst_sum_add_nextsumnegative_body_steps = fs_r_dst_sum_add_nextsumnegative_body_steps + fs_a_dst_sum_add_nextsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_add_nextsumresult ge_balance_negative_sum_add_nextsumresult. (((((c) = 2 * (ge_balance_positive_sum_add_nextsumresult) /\ (ge_balance_negative_sum_add_nextsumresult) = 0) \/ exists ge_signed_half_sum_add_nextsumresultdecode. (((c) = 2 * ge_signed_half_sum_add_nextsumresultdecode + 1 /\ (ge_balance_positive_sum_add_nextsumresult) = 0) /\ (ge_balance_negative_sum_add_nextsumresult) = S ge_signed_half_sum_add_nextsumresultdecode))) /\ ((dst_positive_sum_sum_add_nextsum) + ge_balance_negative_sum_add_nextsumresult = (dst_negative_sum_sum_add_nextsum) + ge_balance_positive_sum_add_nextsumresult))))))))))) -> (exists dsa_ap_sum_add_result dsa_an_sum_add_result dsa_bp_sum_add_result dsa_bn_sum_add_result dsa_cp_sum_add_result dsa_cn_sum_add_result. (((((a) = 2 * (dsa_ap_sum_add_result) /\ (dsa_an_sum_add_result) = 0) \/ exists ge_signed_half_sum_add_resultleft. (((a) = 2 * ge_signed_half_sum_add_resultleft + 1 /\ (dsa_ap_sum_add_result) = 0) /\ (dsa_an_sum_add_result) = S ge_signed_half_sum_add_resultleft))) /\ ((((((b) = 2 * (dsa_bp_sum_add_result) /\ (dsa_bn_sum_add_result) = 0) \/ exists ge_signed_half_sum_add_resultright. (((b) = 2 * ge_signed_half_sum_add_resultright + 1 /\ (dsa_bp_sum_add_result) = 0) /\ (dsa_bn_sum_add_result) = S ge_signed_half_sum_add_resultright))) /\ ((((((c) = 2 * (dsa_cp_sum_add_result) /\ (dsa_cn_sum_add_result) = 0) \/ exists ge_signed_half_sum_add_resultoutput. (((c) = 2 * ge_signed_half_sum_add_resultoutput + 1 /\ (dsa_cp_sum_add_result) = 0) /\ (dsa_cn_sum_add_result) = S ge_signed_half_sum_add_resultoutput))) /\ ((dsa_ap_sum_add_result + dsa_bp_sum_add_result) + dsa_cn_sum_add_result = (dsa_an_sum_add_result + dsa_bn_sum_add_result) + dsa_cp_sum_add_result)))))))