signed_rectangular_slice_sum_successor_decompose

Exact expanded first-order arithmetic statement

forall F o s l z. (exists srs_slice_sum_decomp_input. ((((exists dst_positive_code_sum_decomp_inputslicesource_table dst_positive_scale_sum_decomp_inputslicesource_table dst_negative_code_sum_decomp_inputslicesource_table dst_negative_scale_sum_decomp_inputslicesource_table. (((F) = (((((dst_positive_code_sum_decomp_inputslicesource_table) + (dst_positive_scale_sum_decomp_inputslicesource_table)) * S ((dst_positive_code_sum_decomp_inputslicesource_table) + (dst_positive_scale_sum_decomp_inputslicesource_table)) + ((dst_positive_scale_sum_decomp_inputslicesource_table) + (dst_positive_scale_sum_decomp_inputslicesource_table))) + (((dst_negative_code_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)) * S ((dst_negative_code_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)) + ((dst_negative_scale_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)))) * S ((((dst_positive_code_sum_decomp_inputslicesource_table) + (dst_positive_scale_sum_decomp_inputslicesource_table)) * S ((dst_positive_code_sum_decomp_inputslicesource_table) + (dst_positive_scale_sum_decomp_inputslicesource_table)) + ((dst_positive_scale_sum_decomp_inputslicesource_table) + (dst_positive_scale_sum_decomp_inputslicesource_table))) + (((dst_negative_code_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)) * S ((dst_negative_code_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)) + ((dst_negative_scale_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)))) + ((((dst_negative_code_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)) * S ((dst_negative_code_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)) + ((dst_negative_scale_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table))) + (((dst_negative_code_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)) * S ((dst_negative_code_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)) + ((dst_negative_scale_sum_decomp_inputslicesource_table) + (dst_negative_scale_sum_decomp_inputslicesource_table)))))) /\ (forall dst_index_sum_decomp_inputslicesource_table. (exists pvs_le_gap_sum_decomp_inputslicesource_tabledomain. pvs_le_gap_sum_decomp_inputslicesource_tabledomain + (dst_index_sum_decomp_inputslicesource_table) = (0)) -> exists dst_positive_sum_decomp_inputslicesource_table dst_negative_sum_decomp_inputslicesource_table dst_value_sum_decomp_inputslicesource_table. ((((exists ff_h_pvs_sum_decomp_inputslicesource_tableentrypositive. ff_h_pvs_sum_decomp_inputslicesource_tableentrypositive + S (dst_positive_sum_decomp_inputslicesource_table) = S ((S (dst_index_sum_decomp_inputslicesource_table)) * dst_positive_scale_sum_decomp_inputslicesource_table)) /\ exists ff_q_pvs_sum_decomp_inputslicesource_tableentrypositive. dst_positive_code_sum_decomp_inputslicesource_table = ff_q_pvs_sum_decomp_inputslicesource_tableentrypositive * S ((S (dst_index_sum_decomp_inputslicesource_table)) * dst_positive_scale_sum_decomp_inputslicesource_table) + (dst_positive_sum_decomp_inputslicesource_table))) /\ (((((exists ff_h_pvs_sum_decomp_inputslicesource_tableentrynegative. ff_h_pvs_sum_decomp_inputslicesource_tableentrynegative + S (dst_negative_sum_decomp_inputslicesource_table) = S ((S (dst_index_sum_decomp_inputslicesource_table)) * dst_negative_scale_sum_decomp_inputslicesource_table)) /\ exists ff_q_pvs_sum_decomp_inputslicesource_tableentrynegative. dst_negative_code_sum_decomp_inputslicesource_table = ff_q_pvs_sum_decomp_inputslicesource_tableentrynegative * S ((S (dst_index_sum_decomp_inputslicesource_table)) * dst_negative_scale_sum_decomp_inputslicesource_table) + (dst_negative_sum_decomp_inputslicesource_table))) /\ (exists ge_balance_positive_sum_decomp_inputslicesource_tableentryvalue ge_balance_negative_sum_decomp_inputslicesource_tableentryvalue. (((((dst_value_sum_decomp_inputslicesource_table) = 2 * (ge_balance_positive_sum_decomp_inputslicesource_tableentryvalue) /\ (ge_balance_negative_sum_decomp_inputslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_decomp_inputslicesource_tableentryvaluedecode. (((dst_value_sum_decomp_inputslicesource_table) = 2 * ge_signed_half_sum_decomp_inputslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_decomp_inputslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_decomp_inputslicesource_tableentryvalue) = S ge_signed_half_sum_decomp_inputslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_decomp_inputslicesource_table) + ge_balance_negative_sum_decomp_inputslicesource_tableentryvalue = (dst_negative_sum_decomp_inputslicesource_table) + ge_balance_positive_sum_decomp_inputslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_decomp_inputsliceoutput_table dst_positive_scale_sum_decomp_inputsliceoutput_table dst_negative_code_sum_decomp_inputsliceoutput_table dst_negative_scale_sum_decomp_inputsliceoutput_table. (((srs_slice_sum_decomp_input) = (((((dst_positive_code_sum_decomp_inputsliceoutput_table) + (dst_positive_scale_sum_decomp_inputsliceoutput_table)) * S ((dst_positive_code_sum_decomp_inputsliceoutput_table) + (dst_positive_scale_sum_decomp_inputsliceoutput_table)) + ((dst_positive_scale_sum_decomp_inputsliceoutput_table) + (dst_positive_scale_sum_decomp_inputsliceoutput_table))) + (((dst_negative_code_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)) * S ((dst_negative_code_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)) + ((dst_negative_scale_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)))) * S ((((dst_positive_code_sum_decomp_inputsliceoutput_table) + (dst_positive_scale_sum_decomp_inputsliceoutput_table)) * S ((dst_positive_code_sum_decomp_inputsliceoutput_table) + (dst_positive_scale_sum_decomp_inputsliceoutput_table)) + ((dst_positive_scale_sum_decomp_inputsliceoutput_table) + (dst_positive_scale_sum_decomp_inputsliceoutput_table))) + (((dst_negative_code_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)) * S ((dst_negative_code_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)) + ((dst_negative_scale_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)))) + ((((dst_negative_code_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)) * S ((dst_negative_code_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)) + ((dst_negative_scale_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table))) + (((dst_negative_code_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)) * S ((dst_negative_code_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)) + ((dst_negative_scale_sum_decomp_inputsliceoutput_table) + (dst_negative_scale_sum_decomp_inputsliceoutput_table)))))) /\ (forall dst_index_sum_decomp_inputsliceoutput_table. (exists pvs_le_gap_sum_decomp_inputsliceoutput_tabledomain. pvs_le_gap_sum_decomp_inputsliceoutput_tabledomain + (dst_index_sum_decomp_inputsliceoutput_table) = (S l)) -> exists dst_positive_sum_decomp_inputsliceoutput_table dst_negative_sum_decomp_inputsliceoutput_table dst_value_sum_decomp_inputsliceoutput_table. ((((exists ff_h_pvs_sum_decomp_inputsliceoutput_tableentrypositive. ff_h_pvs_sum_decomp_inputsliceoutput_tableentrypositive + S (dst_positive_sum_decomp_inputsliceoutput_table) = S ((S (dst_index_sum_decomp_inputsliceoutput_table)) * dst_positive_scale_sum_decomp_inputsliceoutput_table)) /\ exists ff_q_pvs_sum_decomp_inputsliceoutput_tableentrypositive. dst_positive_code_sum_decomp_inputsliceoutput_table = ff_q_pvs_sum_decomp_inputsliceoutput_tableentrypositive * S ((S (dst_index_sum_decomp_inputsliceoutput_table)) * dst_positive_scale_sum_decomp_inputsliceoutput_table) + (dst_positive_sum_decomp_inputsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_decomp_inputsliceoutput_tableentrynegative. ff_h_pvs_sum_decomp_inputsliceoutput_tableentrynegative + S (dst_negative_sum_decomp_inputsliceoutput_table) = S ((S (dst_index_sum_decomp_inputsliceoutput_table)) * dst_negative_scale_sum_decomp_inputsliceoutput_table)) /\ exists ff_q_pvs_sum_decomp_inputsliceoutput_tableentrynegative. dst_negative_code_sum_decomp_inputsliceoutput_table = ff_q_pvs_sum_decomp_inputsliceoutput_tableentrynegative * S ((S (dst_index_sum_decomp_inputsliceoutput_table)) * dst_negative_scale_sum_decomp_inputsliceoutput_table) + (dst_negative_sum_decomp_inputsliceoutput_table))) /\ (exists ge_balance_positive_sum_decomp_inputsliceoutput_tableentryvalue ge_balance_negative_sum_decomp_inputsliceoutput_tableentryvalue. (((((dst_value_sum_decomp_inputsliceoutput_table) = 2 * (ge_balance_positive_sum_decomp_inputsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_decomp_inputsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_decomp_inputsliceoutput_tableentryvaluedecode. (((dst_value_sum_decomp_inputsliceoutput_table) = 2 * ge_signed_half_sum_decomp_inputsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_decomp_inputsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_decomp_inputsliceoutput_tableentryvalue) = S ge_signed_half_sum_decomp_inputsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_decomp_inputsliceoutput_table) + ge_balance_negative_sum_decomp_inputsliceoutput_tableentryvalue = (dst_negative_sum_decomp_inputsliceoutput_table) + ge_balance_positive_sum_decomp_inputsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_decomp_inputslice. (exists pvs_gap_sum_decomp_inputslicebound. pvs_gap_sum_decomp_inputslicebound + S (srs_index_sum_decomp_inputslice) = (S l)) -> exists srs_value_sum_decomp_inputslice. (((exists dst_positive_code_sum_decomp_inputsliceentrysource dst_positive_scale_sum_decomp_inputsliceentrysource dst_negative_code_sum_decomp_inputsliceentrysource dst_negative_scale_sum_decomp_inputsliceentrysource dst_positive_sum_decomp_inputsliceentrysource dst_negative_sum_decomp_inputsliceentrysource. (((F) = (((((dst_positive_code_sum_decomp_inputsliceentrysource) + (dst_positive_scale_sum_decomp_inputsliceentrysource)) * S ((dst_positive_code_sum_decomp_inputsliceentrysource) + (dst_positive_scale_sum_decomp_inputsliceentrysource)) + ((dst_positive_scale_sum_decomp_inputsliceentrysource) + (dst_positive_scale_sum_decomp_inputsliceentrysource))) + (((dst_negative_code_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)) * S ((dst_negative_code_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)) + ((dst_negative_scale_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)))) * S ((((dst_positive_code_sum_decomp_inputsliceentrysource) + (dst_positive_scale_sum_decomp_inputsliceentrysource)) * S ((dst_positive_code_sum_decomp_inputsliceentrysource) + (dst_positive_scale_sum_decomp_inputsliceentrysource)) + ((dst_positive_scale_sum_decomp_inputsliceentrysource) + (dst_positive_scale_sum_decomp_inputsliceentrysource))) + (((dst_negative_code_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)) * S ((dst_negative_code_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)) + ((dst_negative_scale_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)))) + ((((dst_negative_code_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)) * S ((dst_negative_code_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)) + ((dst_negative_scale_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource))) + (((dst_negative_code_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)) * S ((dst_negative_code_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)) + ((dst_negative_scale_sum_decomp_inputsliceentrysource) + (dst_negative_scale_sum_decomp_inputsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_decomp_inputsliceentrysourcepositive. ff_h_pvs_sum_decomp_inputsliceentrysourcepositive + S (dst_positive_sum_decomp_inputsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_decomp_inputslice))))) * dst_positive_scale_sum_decomp_inputsliceentrysource)) /\ exists ff_q_pvs_sum_decomp_inputsliceentrysourcepositive. dst_positive_code_sum_decomp_inputsliceentrysource = ff_q_pvs_sum_decomp_inputsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_decomp_inputslice))))) * dst_positive_scale_sum_decomp_inputsliceentrysource) + (dst_positive_sum_decomp_inputsliceentrysource))) /\ (((((exists ff_h_pvs_sum_decomp_inputsliceentrysourcenegative. ff_h_pvs_sum_decomp_inputsliceentrysourcenegative + S (dst_negative_sum_decomp_inputsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_decomp_inputslice))))) * dst_negative_scale_sum_decomp_inputsliceentrysource)) /\ exists ff_q_pvs_sum_decomp_inputsliceentrysourcenegative. dst_negative_code_sum_decomp_inputsliceentrysource = ff_q_pvs_sum_decomp_inputsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_decomp_inputslice))))) * dst_negative_scale_sum_decomp_inputsliceentrysource) + (dst_negative_sum_decomp_inputsliceentrysource))) /\ (exists ge_balance_positive_sum_decomp_inputsliceentrysourcevalue ge_balance_negative_sum_decomp_inputsliceentrysourcevalue. (((((srs_value_sum_decomp_inputslice) = 2 * (ge_balance_positive_sum_decomp_inputsliceentrysourcevalue) /\ (ge_balance_negative_sum_decomp_inputsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_decomp_inputsliceentrysourcevaluedecode. (((srs_value_sum_decomp_inputslice) = 2 * ge_signed_half_sum_decomp_inputsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_decomp_inputsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_decomp_inputsliceentrysourcevalue) = S ge_signed_half_sum_decomp_inputsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_decomp_inputsliceentrysource) + ge_balance_negative_sum_decomp_inputsliceentrysourcevalue = (dst_negative_sum_decomp_inputsliceentrysource) + ge_balance_positive_sum_decomp_inputsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_decomp_inputsliceentryoutput dst_positive_scale_sum_decomp_inputsliceentryoutput dst_negative_code_sum_decomp_inputsliceentryoutput dst_negative_scale_sum_decomp_inputsliceentryoutput dst_positive_sum_decomp_inputsliceentryoutput dst_negative_sum_decomp_inputsliceentryoutput. (((srs_slice_sum_decomp_input) = (((((dst_positive_code_sum_decomp_inputsliceentryoutput) + (dst_positive_scale_sum_decomp_inputsliceentryoutput)) * S ((dst_positive_code_sum_decomp_inputsliceentryoutput) + (dst_positive_scale_sum_decomp_inputsliceentryoutput)) + ((dst_positive_scale_sum_decomp_inputsliceentryoutput) + (dst_positive_scale_sum_decomp_inputsliceentryoutput))) + (((dst_negative_code_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)) * S ((dst_negative_code_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)) + ((dst_negative_scale_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)))) * S ((((dst_positive_code_sum_decomp_inputsliceentryoutput) + (dst_positive_scale_sum_decomp_inputsliceentryoutput)) * S ((dst_positive_code_sum_decomp_inputsliceentryoutput) + (dst_positive_scale_sum_decomp_inputsliceentryoutput)) + ((dst_positive_scale_sum_decomp_inputsliceentryoutput) + (dst_positive_scale_sum_decomp_inputsliceentryoutput))) + (((dst_negative_code_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)) * S ((dst_negative_code_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)) + ((dst_negative_scale_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)))) + ((((dst_negative_code_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)) * S ((dst_negative_code_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)) + ((dst_negative_scale_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput))) + (((dst_negative_code_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)) * S ((dst_negative_code_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)) + ((dst_negative_scale_sum_decomp_inputsliceentryoutput) + (dst_negative_scale_sum_decomp_inputsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_decomp_inputsliceentryoutputpositive. ff_h_pvs_sum_decomp_inputsliceentryoutputpositive + S (dst_positive_sum_decomp_inputsliceentryoutput) = S ((S (srs_index_sum_decomp_inputslice)) * dst_positive_scale_sum_decomp_inputsliceentryoutput)) /\ exists ff_q_pvs_sum_decomp_inputsliceentryoutputpositive. dst_positive_code_sum_decomp_inputsliceentryoutput = ff_q_pvs_sum_decomp_inputsliceentryoutputpositive * S ((S (srs_index_sum_decomp_inputslice)) * dst_positive_scale_sum_decomp_inputsliceentryoutput) + (dst_positive_sum_decomp_inputsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_decomp_inputsliceentryoutputnegative. ff_h_pvs_sum_decomp_inputsliceentryoutputnegative + S (dst_negative_sum_decomp_inputsliceentryoutput) = S ((S (srs_index_sum_decomp_inputslice)) * dst_negative_scale_sum_decomp_inputsliceentryoutput)) /\ exists ff_q_pvs_sum_decomp_inputsliceentryoutputnegative. dst_negative_code_sum_decomp_inputsliceentryoutput = ff_q_pvs_sum_decomp_inputsliceentryoutputnegative * S ((S (srs_index_sum_decomp_inputslice)) * dst_negative_scale_sum_decomp_inputsliceentryoutput) + (dst_negative_sum_decomp_inputsliceentryoutput))) /\ (exists ge_balance_positive_sum_decomp_inputsliceentryoutputvalue ge_balance_negative_sum_decomp_inputsliceentryoutputvalue. (((((srs_value_sum_decomp_inputslice) = 2 * (ge_balance_positive_sum_decomp_inputsliceentryoutputvalue) /\ (ge_balance_negative_sum_decomp_inputsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_decomp_inputsliceentryoutputvaluedecode. (((srs_value_sum_decomp_inputslice) = 2 * ge_signed_half_sum_decomp_inputsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_decomp_inputsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_decomp_inputsliceentryoutputvalue) = S ge_signed_half_sum_decomp_inputsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_decomp_inputsliceentryoutput) + ge_balance_negative_sum_decomp_inputsliceentryoutputvalue = (dst_negative_sum_decomp_inputsliceentryoutput) + ge_balance_positive_sum_decomp_inputsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_decomp_inputsum dst_positive_scale_sum_decomp_inputsum dst_negative_code_sum_decomp_inputsum dst_negative_scale_sum_decomp_inputsum dst_positive_sum_sum_decomp_inputsum dst_negative_sum_sum_decomp_inputsum. (((srs_slice_sum_decomp_input) = (((((dst_positive_code_sum_decomp_inputsum) + (dst_positive_scale_sum_decomp_inputsum)) * S ((dst_positive_code_sum_decomp_inputsum) + (dst_positive_scale_sum_decomp_inputsum)) + ((dst_positive_scale_sum_decomp_inputsum) + (dst_positive_scale_sum_decomp_inputsum))) + (((dst_negative_code_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)) * S ((dst_negative_code_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)) + ((dst_negative_scale_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)))) * S ((((dst_positive_code_sum_decomp_inputsum) + (dst_positive_scale_sum_decomp_inputsum)) * S ((dst_positive_code_sum_decomp_inputsum) + (dst_positive_scale_sum_decomp_inputsum)) + ((dst_positive_scale_sum_decomp_inputsum) + (dst_positive_scale_sum_decomp_inputsum))) + (((dst_negative_code_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)) * S ((dst_negative_code_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)) + ((dst_negative_scale_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)))) + ((((dst_negative_code_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)) * S ((dst_negative_code_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)) + ((dst_negative_scale_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum))) + (((dst_negative_code_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)) * S ((dst_negative_code_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)) + ((dst_negative_scale_sum_decomp_inputsum) + (dst_negative_scale_sum_decomp_inputsum)))))) /\ (((exists fs_u_dst_sum_decomp_inputsumpositive fs_v_dst_sum_decomp_inputsumpositive. ((((exists fs_h_dst_sum_decomp_inputsumpositive_body_start. fs_h_dst_sum_decomp_inputsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_decomp_inputsumpositive)) /\ exists fs_q_dst_sum_decomp_inputsumpositive_body_start. fs_u_dst_sum_decomp_inputsumpositive = fs_q_dst_sum_decomp_inputsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_decomp_inputsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_decomp_inputsumpositive_body_terminal. fs_h_dst_sum_decomp_inputsumpositive_body_terminal + S (dst_positive_sum_sum_decomp_inputsum) = S ((S (S l)) * fs_v_dst_sum_decomp_inputsumpositive)) /\ exists fs_q_dst_sum_decomp_inputsumpositive_body_terminal. fs_u_dst_sum_decomp_inputsumpositive = fs_q_dst_sum_decomp_inputsumpositive_body_terminal * S ((S (S l)) * fs_v_dst_sum_decomp_inputsumpositive) + (dst_positive_sum_sum_decomp_inputsum))) /\ forall fs_i_dst_sum_decomp_inputsumpositive_body_steps. (exists fs_lt_dst_sum_decomp_inputsumpositive_body_steps_bound. fs_lt_dst_sum_decomp_inputsumpositive_body_steps_bound + S fs_i_dst_sum_decomp_inputsumpositive_body_steps = S l) -> exists fs_a_dst_sum_decomp_inputsumpositive_body_steps fs_r_dst_sum_decomp_inputsumpositive_body_steps fs_s_dst_sum_decomp_inputsumpositive_body_steps. ((((exists fs_h_dst_sum_decomp_inputsumpositive_body_steps_summand. fs_h_dst_sum_decomp_inputsumpositive_body_steps_summand + S (fs_a_dst_sum_decomp_inputsumpositive_body_steps) = S ((S (fs_i_dst_sum_decomp_inputsumpositive_body_steps)) * dst_positive_scale_sum_decomp_inputsum)) /\ exists fs_q_dst_sum_decomp_inputsumpositive_body_steps_summand. dst_positive_code_sum_decomp_inputsum = fs_q_dst_sum_decomp_inputsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_decomp_inputsumpositive_body_steps)) * dst_positive_scale_sum_decomp_inputsum) + (fs_a_dst_sum_decomp_inputsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_decomp_inputsumpositive_body_steps_partial. fs_h_dst_sum_decomp_inputsumpositive_body_steps_partial + S (fs_r_dst_sum_decomp_inputsumpositive_body_steps) = S ((S (fs_i_dst_sum_decomp_inputsumpositive_body_steps)) * fs_v_dst_sum_decomp_inputsumpositive)) /\ exists fs_q_dst_sum_decomp_inputsumpositive_body_steps_partial. fs_u_dst_sum_decomp_inputsumpositive = fs_q_dst_sum_decomp_inputsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_decomp_inputsumpositive_body_steps)) * fs_v_dst_sum_decomp_inputsumpositive) + (fs_r_dst_sum_decomp_inputsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_decomp_inputsumpositive_body_steps_successor. fs_h_dst_sum_decomp_inputsumpositive_body_steps_successor + S (fs_s_dst_sum_decomp_inputsumpositive_body_steps) = S ((S (S fs_i_dst_sum_decomp_inputsumpositive_body_steps)) * fs_v_dst_sum_decomp_inputsumpositive)) /\ exists fs_q_dst_sum_decomp_inputsumpositive_body_steps_successor. fs_u_dst_sum_decomp_inputsumpositive = fs_q_dst_sum_decomp_inputsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_decomp_inputsumpositive_body_steps)) * fs_v_dst_sum_decomp_inputsumpositive) + (fs_s_dst_sum_decomp_inputsumpositive_body_steps))) /\ fs_s_dst_sum_decomp_inputsumpositive_body_steps = fs_r_dst_sum_decomp_inputsumpositive_body_steps + fs_a_dst_sum_decomp_inputsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_decomp_inputsumnegative fs_v_dst_sum_decomp_inputsumnegative. ((((exists fs_h_dst_sum_decomp_inputsumnegative_body_start. fs_h_dst_sum_decomp_inputsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_decomp_inputsumnegative)) /\ exists fs_q_dst_sum_decomp_inputsumnegative_body_start. fs_u_dst_sum_decomp_inputsumnegative = fs_q_dst_sum_decomp_inputsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_decomp_inputsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_decomp_inputsumnegative_body_terminal. fs_h_dst_sum_decomp_inputsumnegative_body_terminal + S (dst_negative_sum_sum_decomp_inputsum) = S ((S (S l)) * fs_v_dst_sum_decomp_inputsumnegative)) /\ exists fs_q_dst_sum_decomp_inputsumnegative_body_terminal. fs_u_dst_sum_decomp_inputsumnegative = fs_q_dst_sum_decomp_inputsumnegative_body_terminal * S ((S (S l)) * fs_v_dst_sum_decomp_inputsumnegative) + (dst_negative_sum_sum_decomp_inputsum))) /\ forall fs_i_dst_sum_decomp_inputsumnegative_body_steps. (exists fs_lt_dst_sum_decomp_inputsumnegative_body_steps_bound. fs_lt_dst_sum_decomp_inputsumnegative_body_steps_bound + S fs_i_dst_sum_decomp_inputsumnegative_body_steps = S l) -> exists fs_a_dst_sum_decomp_inputsumnegative_body_steps fs_r_dst_sum_decomp_inputsumnegative_body_steps fs_s_dst_sum_decomp_inputsumnegative_body_steps. ((((exists fs_h_dst_sum_decomp_inputsumnegative_body_steps_summand. fs_h_dst_sum_decomp_inputsumnegative_body_steps_summand + S (fs_a_dst_sum_decomp_inputsumnegative_body_steps) = S ((S (fs_i_dst_sum_decomp_inputsumnegative_body_steps)) * dst_negative_scale_sum_decomp_inputsum)) /\ exists fs_q_dst_sum_decomp_inputsumnegative_body_steps_summand. dst_negative_code_sum_decomp_inputsum = fs_q_dst_sum_decomp_inputsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_decomp_inputsumnegative_body_steps)) * dst_negative_scale_sum_decomp_inputsum) + (fs_a_dst_sum_decomp_inputsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_decomp_inputsumnegative_body_steps_partial. fs_h_dst_sum_decomp_inputsumnegative_body_steps_partial + S (fs_r_dst_sum_decomp_inputsumnegative_body_steps) = S ((S (fs_i_dst_sum_decomp_inputsumnegative_body_steps)) * fs_v_dst_sum_decomp_inputsumnegative)) /\ exists fs_q_dst_sum_decomp_inputsumnegative_body_steps_partial. fs_u_dst_sum_decomp_inputsumnegative = fs_q_dst_sum_decomp_inputsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_decomp_inputsumnegative_body_steps)) * fs_v_dst_sum_decomp_inputsumnegative) + (fs_r_dst_sum_decomp_inputsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_decomp_inputsumnegative_body_steps_successor. fs_h_dst_sum_decomp_inputsumnegative_body_steps_successor + S (fs_s_dst_sum_decomp_inputsumnegative_body_steps) = S ((S (S fs_i_dst_sum_decomp_inputsumnegative_body_steps)) * fs_v_dst_sum_decomp_inputsumnegative)) /\ exists fs_q_dst_sum_decomp_inputsumnegative_body_steps_successor. fs_u_dst_sum_decomp_inputsumnegative = fs_q_dst_sum_decomp_inputsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_decomp_inputsumnegative_body_steps)) * fs_v_dst_sum_decomp_inputsumnegative) + (fs_s_dst_sum_decomp_inputsumnegative_body_steps))) /\ fs_s_dst_sum_decomp_inputsumnegative_body_steps = fs_r_dst_sum_decomp_inputsumnegative_body_steps + fs_a_dst_sum_decomp_inputsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_decomp_inputsumresult ge_balance_negative_sum_decomp_inputsumresult. (((((z) = 2 * (ge_balance_positive_sum_decomp_inputsumresult) /\ (ge_balance_negative_sum_decomp_inputsumresult) = 0) \/ exists ge_signed_half_sum_decomp_inputsumresultdecode. (((z) = 2 * ge_signed_half_sum_decomp_inputsumresultdecode + 1 /\ (ge_balance_positive_sum_decomp_inputsumresult) = 0) /\ (ge_balance_negative_sum_decomp_inputsumresult) = S ge_signed_half_sum_decomp_inputsumresultdecode))) /\ ((dst_positive_sum_sum_decomp_inputsum) + ge_balance_negative_sum_decomp_inputsumresult = (dst_negative_sum_sum_decomp_inputsum) + ge_balance_positive_sum_decomp_inputsumresult))))))))))) -> exists a b. ((exists srs_slice_sum_decomp_output. ((((exists dst_positive_code_sum_decomp_outputslicesource_table dst_positive_scale_sum_decomp_outputslicesource_table dst_negative_code_sum_decomp_outputslicesource_table dst_negative_scale_sum_decomp_outputslicesource_table. (((F) = (((((dst_positive_code_sum_decomp_outputslicesource_table) + (dst_positive_scale_sum_decomp_outputslicesource_table)) * S ((dst_positive_code_sum_decomp_outputslicesource_table) + (dst_positive_scale_sum_decomp_outputslicesource_table)) + ((dst_positive_scale_sum_decomp_outputslicesource_table) + (dst_positive_scale_sum_decomp_outputslicesource_table))) + (((dst_negative_code_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)) * S ((dst_negative_code_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)) + ((dst_negative_scale_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)))) * S ((((dst_positive_code_sum_decomp_outputslicesource_table) + (dst_positive_scale_sum_decomp_outputslicesource_table)) * S ((dst_positive_code_sum_decomp_outputslicesource_table) + (dst_positive_scale_sum_decomp_outputslicesource_table)) + ((dst_positive_scale_sum_decomp_outputslicesource_table) + (dst_positive_scale_sum_decomp_outputslicesource_table))) + (((dst_negative_code_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)) * S ((dst_negative_code_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)) + ((dst_negative_scale_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)))) + ((((dst_negative_code_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)) * S ((dst_negative_code_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)) + ((dst_negative_scale_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table))) + (((dst_negative_code_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)) * S ((dst_negative_code_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)) + ((dst_negative_scale_sum_decomp_outputslicesource_table) + (dst_negative_scale_sum_decomp_outputslicesource_table)))))) /\ (forall dst_index_sum_decomp_outputslicesource_table. (exists pvs_le_gap_sum_decomp_outputslicesource_tabledomain. pvs_le_gap_sum_decomp_outputslicesource_tabledomain + (dst_index_sum_decomp_outputslicesource_table) = (0)) -> exists dst_positive_sum_decomp_outputslicesource_table dst_negative_sum_decomp_outputslicesource_table dst_value_sum_decomp_outputslicesource_table. ((((exists ff_h_pvs_sum_decomp_outputslicesource_tableentrypositive. ff_h_pvs_sum_decomp_outputslicesource_tableentrypositive + S (dst_positive_sum_decomp_outputslicesource_table) = S ((S (dst_index_sum_decomp_outputslicesource_table)) * dst_positive_scale_sum_decomp_outputslicesource_table)) /\ exists ff_q_pvs_sum_decomp_outputslicesource_tableentrypositive. dst_positive_code_sum_decomp_outputslicesource_table = ff_q_pvs_sum_decomp_outputslicesource_tableentrypositive * S ((S (dst_index_sum_decomp_outputslicesource_table)) * dst_positive_scale_sum_decomp_outputslicesource_table) + (dst_positive_sum_decomp_outputslicesource_table))) /\ (((((exists ff_h_pvs_sum_decomp_outputslicesource_tableentrynegative. ff_h_pvs_sum_decomp_outputslicesource_tableentrynegative + S (dst_negative_sum_decomp_outputslicesource_table) = S ((S (dst_index_sum_decomp_outputslicesource_table)) * dst_negative_scale_sum_decomp_outputslicesource_table)) /\ exists ff_q_pvs_sum_decomp_outputslicesource_tableentrynegative. dst_negative_code_sum_decomp_outputslicesource_table = ff_q_pvs_sum_decomp_outputslicesource_tableentrynegative * S ((S (dst_index_sum_decomp_outputslicesource_table)) * dst_negative_scale_sum_decomp_outputslicesource_table) + (dst_negative_sum_decomp_outputslicesource_table))) /\ (exists ge_balance_positive_sum_decomp_outputslicesource_tableentryvalue ge_balance_negative_sum_decomp_outputslicesource_tableentryvalue. (((((dst_value_sum_decomp_outputslicesource_table) = 2 * (ge_balance_positive_sum_decomp_outputslicesource_tableentryvalue) /\ (ge_balance_negative_sum_decomp_outputslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_decomp_outputslicesource_tableentryvaluedecode. (((dst_value_sum_decomp_outputslicesource_table) = 2 * ge_signed_half_sum_decomp_outputslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_decomp_outputslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_decomp_outputslicesource_tableentryvalue) = S ge_signed_half_sum_decomp_outputslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_decomp_outputslicesource_table) + ge_balance_negative_sum_decomp_outputslicesource_tableentryvalue = (dst_negative_sum_decomp_outputslicesource_table) + ge_balance_positive_sum_decomp_outputslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_decomp_outputsliceoutput_table dst_positive_scale_sum_decomp_outputsliceoutput_table dst_negative_code_sum_decomp_outputsliceoutput_table dst_negative_scale_sum_decomp_outputsliceoutput_table. (((srs_slice_sum_decomp_output) = (((((dst_positive_code_sum_decomp_outputsliceoutput_table) + (dst_positive_scale_sum_decomp_outputsliceoutput_table)) * S ((dst_positive_code_sum_decomp_outputsliceoutput_table) + (dst_positive_scale_sum_decomp_outputsliceoutput_table)) + ((dst_positive_scale_sum_decomp_outputsliceoutput_table) + (dst_positive_scale_sum_decomp_outputsliceoutput_table))) + (((dst_negative_code_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)) * S ((dst_negative_code_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)) + ((dst_negative_scale_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)))) * S ((((dst_positive_code_sum_decomp_outputsliceoutput_table) + (dst_positive_scale_sum_decomp_outputsliceoutput_table)) * S ((dst_positive_code_sum_decomp_outputsliceoutput_table) + (dst_positive_scale_sum_decomp_outputsliceoutput_table)) + ((dst_positive_scale_sum_decomp_outputsliceoutput_table) + (dst_positive_scale_sum_decomp_outputsliceoutput_table))) + (((dst_negative_code_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)) * S ((dst_negative_code_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)) + ((dst_negative_scale_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)))) + ((((dst_negative_code_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)) * S ((dst_negative_code_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)) + ((dst_negative_scale_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table))) + (((dst_negative_code_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)) * S ((dst_negative_code_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)) + ((dst_negative_scale_sum_decomp_outputsliceoutput_table) + (dst_negative_scale_sum_decomp_outputsliceoutput_table)))))) /\ (forall dst_index_sum_decomp_outputsliceoutput_table. (exists pvs_le_gap_sum_decomp_outputsliceoutput_tabledomain. pvs_le_gap_sum_decomp_outputsliceoutput_tabledomain + (dst_index_sum_decomp_outputsliceoutput_table) = (l)) -> exists dst_positive_sum_decomp_outputsliceoutput_table dst_negative_sum_decomp_outputsliceoutput_table dst_value_sum_decomp_outputsliceoutput_table. ((((exists ff_h_pvs_sum_decomp_outputsliceoutput_tableentrypositive. ff_h_pvs_sum_decomp_outputsliceoutput_tableentrypositive + S (dst_positive_sum_decomp_outputsliceoutput_table) = S ((S (dst_index_sum_decomp_outputsliceoutput_table)) * dst_positive_scale_sum_decomp_outputsliceoutput_table)) /\ exists ff_q_pvs_sum_decomp_outputsliceoutput_tableentrypositive. dst_positive_code_sum_decomp_outputsliceoutput_table = ff_q_pvs_sum_decomp_outputsliceoutput_tableentrypositive * S ((S (dst_index_sum_decomp_outputsliceoutput_table)) * dst_positive_scale_sum_decomp_outputsliceoutput_table) + (dst_positive_sum_decomp_outputsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_decomp_outputsliceoutput_tableentrynegative. ff_h_pvs_sum_decomp_outputsliceoutput_tableentrynegative + S (dst_negative_sum_decomp_outputsliceoutput_table) = S ((S (dst_index_sum_decomp_outputsliceoutput_table)) * dst_negative_scale_sum_decomp_outputsliceoutput_table)) /\ exists ff_q_pvs_sum_decomp_outputsliceoutput_tableentrynegative. dst_negative_code_sum_decomp_outputsliceoutput_table = ff_q_pvs_sum_decomp_outputsliceoutput_tableentrynegative * S ((S (dst_index_sum_decomp_outputsliceoutput_table)) * dst_negative_scale_sum_decomp_outputsliceoutput_table) + (dst_negative_sum_decomp_outputsliceoutput_table))) /\ (exists ge_balance_positive_sum_decomp_outputsliceoutput_tableentryvalue ge_balance_negative_sum_decomp_outputsliceoutput_tableentryvalue. (((((dst_value_sum_decomp_outputsliceoutput_table) = 2 * (ge_balance_positive_sum_decomp_outputsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_decomp_outputsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_decomp_outputsliceoutput_tableentryvaluedecode. (((dst_value_sum_decomp_outputsliceoutput_table) = 2 * ge_signed_half_sum_decomp_outputsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_decomp_outputsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_decomp_outputsliceoutput_tableentryvalue) = S ge_signed_half_sum_decomp_outputsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_decomp_outputsliceoutput_table) + ge_balance_negative_sum_decomp_outputsliceoutput_tableentryvalue = (dst_negative_sum_decomp_outputsliceoutput_table) + ge_balance_positive_sum_decomp_outputsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_decomp_outputslice. (exists pvs_gap_sum_decomp_outputslicebound. pvs_gap_sum_decomp_outputslicebound + S (srs_index_sum_decomp_outputslice) = (l)) -> exists srs_value_sum_decomp_outputslice. (((exists dst_positive_code_sum_decomp_outputsliceentrysource dst_positive_scale_sum_decomp_outputsliceentrysource dst_negative_code_sum_decomp_outputsliceentrysource dst_negative_scale_sum_decomp_outputsliceentrysource dst_positive_sum_decomp_outputsliceentrysource dst_negative_sum_decomp_outputsliceentrysource. (((F) = (((((dst_positive_code_sum_decomp_outputsliceentrysource) + (dst_positive_scale_sum_decomp_outputsliceentrysource)) * S ((dst_positive_code_sum_decomp_outputsliceentrysource) + (dst_positive_scale_sum_decomp_outputsliceentrysource)) + ((dst_positive_scale_sum_decomp_outputsliceentrysource) + (dst_positive_scale_sum_decomp_outputsliceentrysource))) + (((dst_negative_code_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)) * S ((dst_negative_code_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)) + ((dst_negative_scale_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)))) * S ((((dst_positive_code_sum_decomp_outputsliceentrysource) + (dst_positive_scale_sum_decomp_outputsliceentrysource)) * S ((dst_positive_code_sum_decomp_outputsliceentrysource) + (dst_positive_scale_sum_decomp_outputsliceentrysource)) + ((dst_positive_scale_sum_decomp_outputsliceentrysource) + (dst_positive_scale_sum_decomp_outputsliceentrysource))) + (((dst_negative_code_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)) * S ((dst_negative_code_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)) + ((dst_negative_scale_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)))) + ((((dst_negative_code_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)) * S ((dst_negative_code_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)) + ((dst_negative_scale_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource))) + (((dst_negative_code_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)) * S ((dst_negative_code_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)) + ((dst_negative_scale_sum_decomp_outputsliceentrysource) + (dst_negative_scale_sum_decomp_outputsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_decomp_outputsliceentrysourcepositive. ff_h_pvs_sum_decomp_outputsliceentrysourcepositive + S (dst_positive_sum_decomp_outputsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_decomp_outputslice))))) * dst_positive_scale_sum_decomp_outputsliceentrysource)) /\ exists ff_q_pvs_sum_decomp_outputsliceentrysourcepositive. dst_positive_code_sum_decomp_outputsliceentrysource = ff_q_pvs_sum_decomp_outputsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_decomp_outputslice))))) * dst_positive_scale_sum_decomp_outputsliceentrysource) + (dst_positive_sum_decomp_outputsliceentrysource))) /\ (((((exists ff_h_pvs_sum_decomp_outputsliceentrysourcenegative. ff_h_pvs_sum_decomp_outputsliceentrysourcenegative + S (dst_negative_sum_decomp_outputsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_decomp_outputslice))))) * dst_negative_scale_sum_decomp_outputsliceentrysource)) /\ exists ff_q_pvs_sum_decomp_outputsliceentrysourcenegative. dst_negative_code_sum_decomp_outputsliceentrysource = ff_q_pvs_sum_decomp_outputsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_decomp_outputslice))))) * dst_negative_scale_sum_decomp_outputsliceentrysource) + (dst_negative_sum_decomp_outputsliceentrysource))) /\ (exists ge_balance_positive_sum_decomp_outputsliceentrysourcevalue ge_balance_negative_sum_decomp_outputsliceentrysourcevalue. (((((srs_value_sum_decomp_outputslice) = 2 * (ge_balance_positive_sum_decomp_outputsliceentrysourcevalue) /\ (ge_balance_negative_sum_decomp_outputsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_decomp_outputsliceentrysourcevaluedecode. (((srs_value_sum_decomp_outputslice) = 2 * ge_signed_half_sum_decomp_outputsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_decomp_outputsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_decomp_outputsliceentrysourcevalue) = S ge_signed_half_sum_decomp_outputsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_decomp_outputsliceentrysource) + ge_balance_negative_sum_decomp_outputsliceentrysourcevalue = (dst_negative_sum_decomp_outputsliceentrysource) + ge_balance_positive_sum_decomp_outputsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_decomp_outputsliceentryoutput dst_positive_scale_sum_decomp_outputsliceentryoutput dst_negative_code_sum_decomp_outputsliceentryoutput dst_negative_scale_sum_decomp_outputsliceentryoutput dst_positive_sum_decomp_outputsliceentryoutput dst_negative_sum_decomp_outputsliceentryoutput. (((srs_slice_sum_decomp_output) = (((((dst_positive_code_sum_decomp_outputsliceentryoutput) + (dst_positive_scale_sum_decomp_outputsliceentryoutput)) * S ((dst_positive_code_sum_decomp_outputsliceentryoutput) + (dst_positive_scale_sum_decomp_outputsliceentryoutput)) + ((dst_positive_scale_sum_decomp_outputsliceentryoutput) + (dst_positive_scale_sum_decomp_outputsliceentryoutput))) + (((dst_negative_code_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)) * S ((dst_negative_code_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)) + ((dst_negative_scale_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)))) * S ((((dst_positive_code_sum_decomp_outputsliceentryoutput) + (dst_positive_scale_sum_decomp_outputsliceentryoutput)) * S ((dst_positive_code_sum_decomp_outputsliceentryoutput) + (dst_positive_scale_sum_decomp_outputsliceentryoutput)) + ((dst_positive_scale_sum_decomp_outputsliceentryoutput) + (dst_positive_scale_sum_decomp_outputsliceentryoutput))) + (((dst_negative_code_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)) * S ((dst_negative_code_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)) + ((dst_negative_scale_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)))) + ((((dst_negative_code_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)) * S ((dst_negative_code_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)) + ((dst_negative_scale_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput))) + (((dst_negative_code_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)) * S ((dst_negative_code_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)) + ((dst_negative_scale_sum_decomp_outputsliceentryoutput) + (dst_negative_scale_sum_decomp_outputsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_decomp_outputsliceentryoutputpositive. ff_h_pvs_sum_decomp_outputsliceentryoutputpositive + S (dst_positive_sum_decomp_outputsliceentryoutput) = S ((S (srs_index_sum_decomp_outputslice)) * dst_positive_scale_sum_decomp_outputsliceentryoutput)) /\ exists ff_q_pvs_sum_decomp_outputsliceentryoutputpositive. dst_positive_code_sum_decomp_outputsliceentryoutput = ff_q_pvs_sum_decomp_outputsliceentryoutputpositive * S ((S (srs_index_sum_decomp_outputslice)) * dst_positive_scale_sum_decomp_outputsliceentryoutput) + (dst_positive_sum_decomp_outputsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_decomp_outputsliceentryoutputnegative. ff_h_pvs_sum_decomp_outputsliceentryoutputnegative + S (dst_negative_sum_decomp_outputsliceentryoutput) = S ((S (srs_index_sum_decomp_outputslice)) * dst_negative_scale_sum_decomp_outputsliceentryoutput)) /\ exists ff_q_pvs_sum_decomp_outputsliceentryoutputnegative. dst_negative_code_sum_decomp_outputsliceentryoutput = ff_q_pvs_sum_decomp_outputsliceentryoutputnegative * S ((S (srs_index_sum_decomp_outputslice)) * dst_negative_scale_sum_decomp_outputsliceentryoutput) + (dst_negative_sum_decomp_outputsliceentryoutput))) /\ (exists ge_balance_positive_sum_decomp_outputsliceentryoutputvalue ge_balance_negative_sum_decomp_outputsliceentryoutputvalue. (((((srs_value_sum_decomp_outputslice) = 2 * (ge_balance_positive_sum_decomp_outputsliceentryoutputvalue) /\ (ge_balance_negative_sum_decomp_outputsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_decomp_outputsliceentryoutputvaluedecode. (((srs_value_sum_decomp_outputslice) = 2 * ge_signed_half_sum_decomp_outputsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_decomp_outputsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_decomp_outputsliceentryoutputvalue) = S ge_signed_half_sum_decomp_outputsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_decomp_outputsliceentryoutput) + ge_balance_negative_sum_decomp_outputsliceentryoutputvalue = (dst_negative_sum_decomp_outputsliceentryoutput) + ge_balance_positive_sum_decomp_outputsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_decomp_outputsum dst_positive_scale_sum_decomp_outputsum dst_negative_code_sum_decomp_outputsum dst_negative_scale_sum_decomp_outputsum dst_positive_sum_sum_decomp_outputsum dst_negative_sum_sum_decomp_outputsum. (((srs_slice_sum_decomp_output) = (((((dst_positive_code_sum_decomp_outputsum) + (dst_positive_scale_sum_decomp_outputsum)) * S ((dst_positive_code_sum_decomp_outputsum) + (dst_positive_scale_sum_decomp_outputsum)) + ((dst_positive_scale_sum_decomp_outputsum) + (dst_positive_scale_sum_decomp_outputsum))) + (((dst_negative_code_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)) * S ((dst_negative_code_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)) + ((dst_negative_scale_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)))) * S ((((dst_positive_code_sum_decomp_outputsum) + (dst_positive_scale_sum_decomp_outputsum)) * S ((dst_positive_code_sum_decomp_outputsum) + (dst_positive_scale_sum_decomp_outputsum)) + ((dst_positive_scale_sum_decomp_outputsum) + (dst_positive_scale_sum_decomp_outputsum))) + (((dst_negative_code_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)) * S ((dst_negative_code_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)) + ((dst_negative_scale_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)))) + ((((dst_negative_code_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)) * S ((dst_negative_code_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)) + ((dst_negative_scale_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum))) + (((dst_negative_code_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)) * S ((dst_negative_code_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)) + ((dst_negative_scale_sum_decomp_outputsum) + (dst_negative_scale_sum_decomp_outputsum)))))) /\ (((exists fs_u_dst_sum_decomp_outputsumpositive fs_v_dst_sum_decomp_outputsumpositive. ((((exists fs_h_dst_sum_decomp_outputsumpositive_body_start. fs_h_dst_sum_decomp_outputsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_decomp_outputsumpositive)) /\ exists fs_q_dst_sum_decomp_outputsumpositive_body_start. fs_u_dst_sum_decomp_outputsumpositive = fs_q_dst_sum_decomp_outputsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_decomp_outputsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_decomp_outputsumpositive_body_terminal. fs_h_dst_sum_decomp_outputsumpositive_body_terminal + S (dst_positive_sum_sum_decomp_outputsum) = S ((S (l)) * fs_v_dst_sum_decomp_outputsumpositive)) /\ exists fs_q_dst_sum_decomp_outputsumpositive_body_terminal. fs_u_dst_sum_decomp_outputsumpositive = fs_q_dst_sum_decomp_outputsumpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_decomp_outputsumpositive) + (dst_positive_sum_sum_decomp_outputsum))) /\ forall fs_i_dst_sum_decomp_outputsumpositive_body_steps. (exists fs_lt_dst_sum_decomp_outputsumpositive_body_steps_bound. fs_lt_dst_sum_decomp_outputsumpositive_body_steps_bound + S fs_i_dst_sum_decomp_outputsumpositive_body_steps = l) -> exists fs_a_dst_sum_decomp_outputsumpositive_body_steps fs_r_dst_sum_decomp_outputsumpositive_body_steps fs_s_dst_sum_decomp_outputsumpositive_body_steps. ((((exists fs_h_dst_sum_decomp_outputsumpositive_body_steps_summand. fs_h_dst_sum_decomp_outputsumpositive_body_steps_summand + S (fs_a_dst_sum_decomp_outputsumpositive_body_steps) = S ((S (fs_i_dst_sum_decomp_outputsumpositive_body_steps)) * dst_positive_scale_sum_decomp_outputsum)) /\ exists fs_q_dst_sum_decomp_outputsumpositive_body_steps_summand. dst_positive_code_sum_decomp_outputsum = fs_q_dst_sum_decomp_outputsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_decomp_outputsumpositive_body_steps)) * dst_positive_scale_sum_decomp_outputsum) + (fs_a_dst_sum_decomp_outputsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_decomp_outputsumpositive_body_steps_partial. fs_h_dst_sum_decomp_outputsumpositive_body_steps_partial + S (fs_r_dst_sum_decomp_outputsumpositive_body_steps) = S ((S (fs_i_dst_sum_decomp_outputsumpositive_body_steps)) * fs_v_dst_sum_decomp_outputsumpositive)) /\ exists fs_q_dst_sum_decomp_outputsumpositive_body_steps_partial. fs_u_dst_sum_decomp_outputsumpositive = fs_q_dst_sum_decomp_outputsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_decomp_outputsumpositive_body_steps)) * fs_v_dst_sum_decomp_outputsumpositive) + (fs_r_dst_sum_decomp_outputsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_decomp_outputsumpositive_body_steps_successor. fs_h_dst_sum_decomp_outputsumpositive_body_steps_successor + S (fs_s_dst_sum_decomp_outputsumpositive_body_steps) = S ((S (S fs_i_dst_sum_decomp_outputsumpositive_body_steps)) * fs_v_dst_sum_decomp_outputsumpositive)) /\ exists fs_q_dst_sum_decomp_outputsumpositive_body_steps_successor. fs_u_dst_sum_decomp_outputsumpositive = fs_q_dst_sum_decomp_outputsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_decomp_outputsumpositive_body_steps)) * fs_v_dst_sum_decomp_outputsumpositive) + (fs_s_dst_sum_decomp_outputsumpositive_body_steps))) /\ fs_s_dst_sum_decomp_outputsumpositive_body_steps = fs_r_dst_sum_decomp_outputsumpositive_body_steps + fs_a_dst_sum_decomp_outputsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_decomp_outputsumnegative fs_v_dst_sum_decomp_outputsumnegative. ((((exists fs_h_dst_sum_decomp_outputsumnegative_body_start. fs_h_dst_sum_decomp_outputsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_decomp_outputsumnegative)) /\ exists fs_q_dst_sum_decomp_outputsumnegative_body_start. fs_u_dst_sum_decomp_outputsumnegative = fs_q_dst_sum_decomp_outputsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_decomp_outputsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_decomp_outputsumnegative_body_terminal. fs_h_dst_sum_decomp_outputsumnegative_body_terminal + S (dst_negative_sum_sum_decomp_outputsum) = S ((S (l)) * fs_v_dst_sum_decomp_outputsumnegative)) /\ exists fs_q_dst_sum_decomp_outputsumnegative_body_terminal. fs_u_dst_sum_decomp_outputsumnegative = fs_q_dst_sum_decomp_outputsumnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_decomp_outputsumnegative) + (dst_negative_sum_sum_decomp_outputsum))) /\ forall fs_i_dst_sum_decomp_outputsumnegative_body_steps. (exists fs_lt_dst_sum_decomp_outputsumnegative_body_steps_bound. fs_lt_dst_sum_decomp_outputsumnegative_body_steps_bound + S fs_i_dst_sum_decomp_outputsumnegative_body_steps = l) -> exists fs_a_dst_sum_decomp_outputsumnegative_body_steps fs_r_dst_sum_decomp_outputsumnegative_body_steps fs_s_dst_sum_decomp_outputsumnegative_body_steps. ((((exists fs_h_dst_sum_decomp_outputsumnegative_body_steps_summand. fs_h_dst_sum_decomp_outputsumnegative_body_steps_summand + S (fs_a_dst_sum_decomp_outputsumnegative_body_steps) = S ((S (fs_i_dst_sum_decomp_outputsumnegative_body_steps)) * dst_negative_scale_sum_decomp_outputsum)) /\ exists fs_q_dst_sum_decomp_outputsumnegative_body_steps_summand. dst_negative_code_sum_decomp_outputsum = fs_q_dst_sum_decomp_outputsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_decomp_outputsumnegative_body_steps)) * dst_negative_scale_sum_decomp_outputsum) + (fs_a_dst_sum_decomp_outputsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_decomp_outputsumnegative_body_steps_partial. fs_h_dst_sum_decomp_outputsumnegative_body_steps_partial + S (fs_r_dst_sum_decomp_outputsumnegative_body_steps) = S ((S (fs_i_dst_sum_decomp_outputsumnegative_body_steps)) * fs_v_dst_sum_decomp_outputsumnegative)) /\ exists fs_q_dst_sum_decomp_outputsumnegative_body_steps_partial. fs_u_dst_sum_decomp_outputsumnegative = fs_q_dst_sum_decomp_outputsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_decomp_outputsumnegative_body_steps)) * fs_v_dst_sum_decomp_outputsumnegative) + (fs_r_dst_sum_decomp_outputsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_decomp_outputsumnegative_body_steps_successor. fs_h_dst_sum_decomp_outputsumnegative_body_steps_successor + S (fs_s_dst_sum_decomp_outputsumnegative_body_steps) = S ((S (S fs_i_dst_sum_decomp_outputsumnegative_body_steps)) * fs_v_dst_sum_decomp_outputsumnegative)) /\ exists fs_q_dst_sum_decomp_outputsumnegative_body_steps_successor. fs_u_dst_sum_decomp_outputsumnegative = fs_q_dst_sum_decomp_outputsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_decomp_outputsumnegative_body_steps)) * fs_v_dst_sum_decomp_outputsumnegative) + (fs_s_dst_sum_decomp_outputsumnegative_body_steps))) /\ fs_s_dst_sum_decomp_outputsumnegative_body_steps = fs_r_dst_sum_decomp_outputsumnegative_body_steps + fs_a_dst_sum_decomp_outputsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_decomp_outputsumresult ge_balance_negative_sum_decomp_outputsumresult. (((((a) = 2 * (ge_balance_positive_sum_decomp_outputsumresult) /\ (ge_balance_negative_sum_decomp_outputsumresult) = 0) \/ exists ge_signed_half_sum_decomp_outputsumresultdecode. (((a) = 2 * ge_signed_half_sum_decomp_outputsumresultdecode + 1 /\ (ge_balance_positive_sum_decomp_outputsumresult) = 0) /\ (ge_balance_negative_sum_decomp_outputsumresult) = S ge_signed_half_sum_decomp_outputsumresultdecode))) /\ ((dst_positive_sum_sum_decomp_outputsum) + ge_balance_negative_sum_decomp_outputsumresult = (dst_negative_sum_sum_decomp_outputsum) + ge_balance_positive_sum_decomp_outputsumresult))))))))))) /\ (((exists dst_positive_code_sum_decomp_last dst_positive_scale_sum_decomp_last dst_negative_code_sum_decomp_last dst_negative_scale_sum_decomp_last dst_positive_sum_decomp_last dst_negative_sum_decomp_last. (((F) = (((((dst_positive_code_sum_decomp_last) + (dst_positive_scale_sum_decomp_last)) * S ((dst_positive_code_sum_decomp_last) + (dst_positive_scale_sum_decomp_last)) + ((dst_positive_scale_sum_decomp_last) + (dst_positive_scale_sum_decomp_last))) + (((dst_negative_code_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)) * S ((dst_negative_code_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)) + ((dst_negative_scale_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)))) * S ((((dst_positive_code_sum_decomp_last) + (dst_positive_scale_sum_decomp_last)) * S ((dst_positive_code_sum_decomp_last) + (dst_positive_scale_sum_decomp_last)) + ((dst_positive_scale_sum_decomp_last) + (dst_positive_scale_sum_decomp_last))) + (((dst_negative_code_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)) * S ((dst_negative_code_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)) + ((dst_negative_scale_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)))) + ((((dst_negative_code_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)) * S ((dst_negative_code_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)) + ((dst_negative_scale_sum_decomp_last) + (dst_negative_scale_sum_decomp_last))) + (((dst_negative_code_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)) * S ((dst_negative_code_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)) + ((dst_negative_scale_sum_decomp_last) + (dst_negative_scale_sum_decomp_last)))))) /\ (((((exists ff_h_pvs_sum_decomp_lastpositive. ff_h_pvs_sum_decomp_lastpositive + S (dst_positive_sum_decomp_last) = S ((S (((o) + ((s) * (l))))) * dst_positive_scale_sum_decomp_last)) /\ exists ff_q_pvs_sum_decomp_lastpositive. dst_positive_code_sum_decomp_last = ff_q_pvs_sum_decomp_lastpositive * S ((S (((o) + ((s) * (l))))) * dst_positive_scale_sum_decomp_last) + (dst_positive_sum_decomp_last))) /\ (((((exists ff_h_pvs_sum_decomp_lastnegative. ff_h_pvs_sum_decomp_lastnegative + S (dst_negative_sum_decomp_last) = S ((S (((o) + ((s) * (l))))) * dst_negative_scale_sum_decomp_last)) /\ exists ff_q_pvs_sum_decomp_lastnegative. dst_negative_code_sum_decomp_last = ff_q_pvs_sum_decomp_lastnegative * S ((S (((o) + ((s) * (l))))) * dst_negative_scale_sum_decomp_last) + (dst_negative_sum_decomp_last))) /\ (exists ge_balance_positive_sum_decomp_lastvalue ge_balance_negative_sum_decomp_lastvalue. (((((b) = 2 * (ge_balance_positive_sum_decomp_lastvalue) /\ (ge_balance_negative_sum_decomp_lastvalue) = 0) \/ exists ge_signed_half_sum_decomp_lastvaluedecode. (((b) = 2 * ge_signed_half_sum_decomp_lastvaluedecode + 1 /\ (ge_balance_positive_sum_decomp_lastvalue) = 0) /\ (ge_balance_negative_sum_decomp_lastvalue) = S ge_signed_half_sum_decomp_lastvaluedecode))) /\ ((dst_positive_sum_decomp_last) + ge_balance_negative_sum_decomp_lastvalue = (dst_negative_sum_decomp_last) + ge_balance_positive_sum_decomp_lastvalue))))))))) /\ (exists dsa_ap_sum_decomp_result dsa_an_sum_decomp_result dsa_bp_sum_decomp_result dsa_bn_sum_decomp_result dsa_cp_sum_decomp_result dsa_cn_sum_decomp_result. (((((a) = 2 * (dsa_ap_sum_decomp_result) /\ (dsa_an_sum_decomp_result) = 0) \/ exists ge_signed_half_sum_decomp_resultleft. (((a) = 2 * ge_signed_half_sum_decomp_resultleft + 1 /\ (dsa_ap_sum_decomp_result) = 0) /\ (dsa_an_sum_decomp_result) = S ge_signed_half_sum_decomp_resultleft))) /\ ((((((b) = 2 * (dsa_bp_sum_decomp_result) /\ (dsa_bn_sum_decomp_result) = 0) \/ exists ge_signed_half_sum_decomp_resultright. (((b) = 2 * ge_signed_half_sum_decomp_resultright + 1 /\ (dsa_bp_sum_decomp_result) = 0) /\ (dsa_bn_sum_decomp_result) = S ge_signed_half_sum_decomp_resultright))) /\ ((((((z) = 2 * (dsa_cp_sum_decomp_result) /\ (dsa_cn_sum_decomp_result) = 0) \/ exists ge_signed_half_sum_decomp_resultoutput. (((z) = 2 * ge_signed_half_sum_decomp_resultoutput + 1 /\ (dsa_cp_sum_decomp_result) = 0) /\ (dsa_cn_sum_decomp_result) = S ge_signed_half_sum_decomp_resultoutput))) /\ ((dsa_ap_sum_decomp_result + dsa_bp_sum_decomp_result) + dsa_cn_sum_decomp_result = (dsa_an_sum_decomp_result + dsa_bn_sum_decomp_result) + dsa_cp_sum_decomp_result))))))))))