signed_slice_sum_concatenate_values

Exact expanded first-order arithmetic statement

forall F o s p q a b c. (exists srs_slice_concat_value_first. ((((exists dst_positive_code_concat_value_firstslicesource_table dst_positive_scale_concat_value_firstslicesource_table dst_negative_code_concat_value_firstslicesource_table dst_negative_scale_concat_value_firstslicesource_table. (((F) = (((((dst_positive_code_concat_value_firstslicesource_table) + (dst_positive_scale_concat_value_firstslicesource_table)) * S ((dst_positive_code_concat_value_firstslicesource_table) + (dst_positive_scale_concat_value_firstslicesource_table)) + ((dst_positive_scale_concat_value_firstslicesource_table) + (dst_positive_scale_concat_value_firstslicesource_table))) + (((dst_negative_code_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)) * S ((dst_negative_code_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)) + ((dst_negative_scale_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)))) * S ((((dst_positive_code_concat_value_firstslicesource_table) + (dst_positive_scale_concat_value_firstslicesource_table)) * S ((dst_positive_code_concat_value_firstslicesource_table) + (dst_positive_scale_concat_value_firstslicesource_table)) + ((dst_positive_scale_concat_value_firstslicesource_table) + (dst_positive_scale_concat_value_firstslicesource_table))) + (((dst_negative_code_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)) * S ((dst_negative_code_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)) + ((dst_negative_scale_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)))) + ((((dst_negative_code_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)) * S ((dst_negative_code_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)) + ((dst_negative_scale_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table))) + (((dst_negative_code_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)) * S ((dst_negative_code_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)) + ((dst_negative_scale_concat_value_firstslicesource_table) + (dst_negative_scale_concat_value_firstslicesource_table)))))) /\ (forall dst_index_concat_value_firstslicesource_table. (exists pvs_le_gap_concat_value_firstslicesource_tabledomain. pvs_le_gap_concat_value_firstslicesource_tabledomain + (dst_index_concat_value_firstslicesource_table) = (0)) -> exists dst_positive_concat_value_firstslicesource_table dst_negative_concat_value_firstslicesource_table dst_value_concat_value_firstslicesource_table. ((((exists ff_h_pvs_concat_value_firstslicesource_tableentrypositive. ff_h_pvs_concat_value_firstslicesource_tableentrypositive + S (dst_positive_concat_value_firstslicesource_table) = S ((S (dst_index_concat_value_firstslicesource_table)) * dst_positive_scale_concat_value_firstslicesource_table)) /\ exists ff_q_pvs_concat_value_firstslicesource_tableentrypositive. dst_positive_code_concat_value_firstslicesource_table = ff_q_pvs_concat_value_firstslicesource_tableentrypositive * S ((S (dst_index_concat_value_firstslicesource_table)) * dst_positive_scale_concat_value_firstslicesource_table) + (dst_positive_concat_value_firstslicesource_table))) /\ (((((exists ff_h_pvs_concat_value_firstslicesource_tableentrynegative. ff_h_pvs_concat_value_firstslicesource_tableentrynegative + S (dst_negative_concat_value_firstslicesource_table) = S ((S (dst_index_concat_value_firstslicesource_table)) * dst_negative_scale_concat_value_firstslicesource_table)) /\ exists ff_q_pvs_concat_value_firstslicesource_tableentrynegative. dst_negative_code_concat_value_firstslicesource_table = ff_q_pvs_concat_value_firstslicesource_tableentrynegative * S ((S (dst_index_concat_value_firstslicesource_table)) * dst_negative_scale_concat_value_firstslicesource_table) + (dst_negative_concat_value_firstslicesource_table))) /\ (exists ge_balance_positive_concat_value_firstslicesource_tableentryvalue ge_balance_negative_concat_value_firstslicesource_tableentryvalue. (((((dst_value_concat_value_firstslicesource_table) = 2 * (ge_balance_positive_concat_value_firstslicesource_tableentryvalue) /\ (ge_balance_negative_concat_value_firstslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_concat_value_firstslicesource_tableentryvaluedecode. (((dst_value_concat_value_firstslicesource_table) = 2 * ge_signed_half_concat_value_firstslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_value_firstslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_concat_value_firstslicesource_tableentryvalue) = S ge_signed_half_concat_value_firstslicesource_tableentryvaluedecode))) /\ ((dst_positive_concat_value_firstslicesource_table) + ge_balance_negative_concat_value_firstslicesource_tableentryvalue = (dst_negative_concat_value_firstslicesource_table) + ge_balance_positive_concat_value_firstslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_concat_value_firstsliceoutput_table dst_positive_scale_concat_value_firstsliceoutput_table dst_negative_code_concat_value_firstsliceoutput_table dst_negative_scale_concat_value_firstsliceoutput_table. (((srs_slice_concat_value_first) = (((((dst_positive_code_concat_value_firstsliceoutput_table) + (dst_positive_scale_concat_value_firstsliceoutput_table)) * S ((dst_positive_code_concat_value_firstsliceoutput_table) + (dst_positive_scale_concat_value_firstsliceoutput_table)) + ((dst_positive_scale_concat_value_firstsliceoutput_table) + (dst_positive_scale_concat_value_firstsliceoutput_table))) + (((dst_negative_code_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)) * S ((dst_negative_code_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)) + ((dst_negative_scale_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)))) * S ((((dst_positive_code_concat_value_firstsliceoutput_table) + (dst_positive_scale_concat_value_firstsliceoutput_table)) * S ((dst_positive_code_concat_value_firstsliceoutput_table) + (dst_positive_scale_concat_value_firstsliceoutput_table)) + ((dst_positive_scale_concat_value_firstsliceoutput_table) + (dst_positive_scale_concat_value_firstsliceoutput_table))) + (((dst_negative_code_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)) * S ((dst_negative_code_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)) + ((dst_negative_scale_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)))) + ((((dst_negative_code_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)) * S ((dst_negative_code_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)) + ((dst_negative_scale_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table))) + (((dst_negative_code_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)) * S ((dst_negative_code_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)) + ((dst_negative_scale_concat_value_firstsliceoutput_table) + (dst_negative_scale_concat_value_firstsliceoutput_table)))))) /\ (forall dst_index_concat_value_firstsliceoutput_table. (exists pvs_le_gap_concat_value_firstsliceoutput_tabledomain. pvs_le_gap_concat_value_firstsliceoutput_tabledomain + (dst_index_concat_value_firstsliceoutput_table) = (p)) -> exists dst_positive_concat_value_firstsliceoutput_table dst_negative_concat_value_firstsliceoutput_table dst_value_concat_value_firstsliceoutput_table. ((((exists ff_h_pvs_concat_value_firstsliceoutput_tableentrypositive. ff_h_pvs_concat_value_firstsliceoutput_tableentrypositive + S (dst_positive_concat_value_firstsliceoutput_table) = S ((S (dst_index_concat_value_firstsliceoutput_table)) * dst_positive_scale_concat_value_firstsliceoutput_table)) /\ exists ff_q_pvs_concat_value_firstsliceoutput_tableentrypositive. dst_positive_code_concat_value_firstsliceoutput_table = ff_q_pvs_concat_value_firstsliceoutput_tableentrypositive * S ((S (dst_index_concat_value_firstsliceoutput_table)) * dst_positive_scale_concat_value_firstsliceoutput_table) + (dst_positive_concat_value_firstsliceoutput_table))) /\ (((((exists ff_h_pvs_concat_value_firstsliceoutput_tableentrynegative. ff_h_pvs_concat_value_firstsliceoutput_tableentrynegative + S (dst_negative_concat_value_firstsliceoutput_table) = S ((S (dst_index_concat_value_firstsliceoutput_table)) * dst_negative_scale_concat_value_firstsliceoutput_table)) /\ exists ff_q_pvs_concat_value_firstsliceoutput_tableentrynegative. dst_negative_code_concat_value_firstsliceoutput_table = ff_q_pvs_concat_value_firstsliceoutput_tableentrynegative * S ((S (dst_index_concat_value_firstsliceoutput_table)) * dst_negative_scale_concat_value_firstsliceoutput_table) + (dst_negative_concat_value_firstsliceoutput_table))) /\ (exists ge_balance_positive_concat_value_firstsliceoutput_tableentryvalue ge_balance_negative_concat_value_firstsliceoutput_tableentryvalue. (((((dst_value_concat_value_firstsliceoutput_table) = 2 * (ge_balance_positive_concat_value_firstsliceoutput_tableentryvalue) /\ (ge_balance_negative_concat_value_firstsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_concat_value_firstsliceoutput_tableentryvaluedecode. (((dst_value_concat_value_firstsliceoutput_table) = 2 * ge_signed_half_concat_value_firstsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_value_firstsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_concat_value_firstsliceoutput_tableentryvalue) = S ge_signed_half_concat_value_firstsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_concat_value_firstsliceoutput_table) + ge_balance_negative_concat_value_firstsliceoutput_tableentryvalue = (dst_negative_concat_value_firstsliceoutput_table) + ge_balance_positive_concat_value_firstsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_concat_value_firstslice. (exists pvs_gap_concat_value_firstslicebound. pvs_gap_concat_value_firstslicebound + S (srs_index_concat_value_firstslice) = (p)) -> exists srs_value_concat_value_firstslice. (((exists dst_positive_code_concat_value_firstsliceentrysource dst_positive_scale_concat_value_firstsliceentrysource dst_negative_code_concat_value_firstsliceentrysource dst_negative_scale_concat_value_firstsliceentrysource dst_positive_concat_value_firstsliceentrysource dst_negative_concat_value_firstsliceentrysource. (((F) = (((((dst_positive_code_concat_value_firstsliceentrysource) + (dst_positive_scale_concat_value_firstsliceentrysource)) * S ((dst_positive_code_concat_value_firstsliceentrysource) + (dst_positive_scale_concat_value_firstsliceentrysource)) + ((dst_positive_scale_concat_value_firstsliceentrysource) + (dst_positive_scale_concat_value_firstsliceentrysource))) + (((dst_negative_code_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)) * S ((dst_negative_code_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)) + ((dst_negative_scale_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)))) * S ((((dst_positive_code_concat_value_firstsliceentrysource) + (dst_positive_scale_concat_value_firstsliceentrysource)) * S ((dst_positive_code_concat_value_firstsliceentrysource) + (dst_positive_scale_concat_value_firstsliceentrysource)) + ((dst_positive_scale_concat_value_firstsliceentrysource) + (dst_positive_scale_concat_value_firstsliceentrysource))) + (((dst_negative_code_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)) * S ((dst_negative_code_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)) + ((dst_negative_scale_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)))) + ((((dst_negative_code_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)) * S ((dst_negative_code_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)) + ((dst_negative_scale_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource))) + (((dst_negative_code_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)) * S ((dst_negative_code_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)) + ((dst_negative_scale_concat_value_firstsliceentrysource) + (dst_negative_scale_concat_value_firstsliceentrysource)))))) /\ (((((exists ff_h_pvs_concat_value_firstsliceentrysourcepositive. ff_h_pvs_concat_value_firstsliceentrysourcepositive + S (dst_positive_concat_value_firstsliceentrysource) = S ((S (((o) + ((s) * (srs_index_concat_value_firstslice))))) * dst_positive_scale_concat_value_firstsliceentrysource)) /\ exists ff_q_pvs_concat_value_firstsliceentrysourcepositive. dst_positive_code_concat_value_firstsliceentrysource = ff_q_pvs_concat_value_firstsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_concat_value_firstslice))))) * dst_positive_scale_concat_value_firstsliceentrysource) + (dst_positive_concat_value_firstsliceentrysource))) /\ (((((exists ff_h_pvs_concat_value_firstsliceentrysourcenegative. ff_h_pvs_concat_value_firstsliceentrysourcenegative + S (dst_negative_concat_value_firstsliceentrysource) = S ((S (((o) + ((s) * (srs_index_concat_value_firstslice))))) * dst_negative_scale_concat_value_firstsliceentrysource)) /\ exists ff_q_pvs_concat_value_firstsliceentrysourcenegative. dst_negative_code_concat_value_firstsliceentrysource = ff_q_pvs_concat_value_firstsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_concat_value_firstslice))))) * dst_negative_scale_concat_value_firstsliceentrysource) + (dst_negative_concat_value_firstsliceentrysource))) /\ (exists ge_balance_positive_concat_value_firstsliceentrysourcevalue ge_balance_negative_concat_value_firstsliceentrysourcevalue. (((((srs_value_concat_value_firstslice) = 2 * (ge_balance_positive_concat_value_firstsliceentrysourcevalue) /\ (ge_balance_negative_concat_value_firstsliceentrysourcevalue) = 0) \/ exists ge_signed_half_concat_value_firstsliceentrysourcevaluedecode. (((srs_value_concat_value_firstslice) = 2 * ge_signed_half_concat_value_firstsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_concat_value_firstsliceentrysourcevalue) = 0) /\ (ge_balance_negative_concat_value_firstsliceentrysourcevalue) = S ge_signed_half_concat_value_firstsliceentrysourcevaluedecode))) /\ ((dst_positive_concat_value_firstsliceentrysource) + ge_balance_negative_concat_value_firstsliceentrysourcevalue = (dst_negative_concat_value_firstsliceentrysource) + ge_balance_positive_concat_value_firstsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_concat_value_firstsliceentryoutput dst_positive_scale_concat_value_firstsliceentryoutput dst_negative_code_concat_value_firstsliceentryoutput dst_negative_scale_concat_value_firstsliceentryoutput dst_positive_concat_value_firstsliceentryoutput dst_negative_concat_value_firstsliceentryoutput. (((srs_slice_concat_value_first) = (((((dst_positive_code_concat_value_firstsliceentryoutput) + (dst_positive_scale_concat_value_firstsliceentryoutput)) * S ((dst_positive_code_concat_value_firstsliceentryoutput) + (dst_positive_scale_concat_value_firstsliceentryoutput)) + ((dst_positive_scale_concat_value_firstsliceentryoutput) + (dst_positive_scale_concat_value_firstsliceentryoutput))) + (((dst_negative_code_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)) * S ((dst_negative_code_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)) + ((dst_negative_scale_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)))) * S ((((dst_positive_code_concat_value_firstsliceentryoutput) + (dst_positive_scale_concat_value_firstsliceentryoutput)) * S ((dst_positive_code_concat_value_firstsliceentryoutput) + (dst_positive_scale_concat_value_firstsliceentryoutput)) + ((dst_positive_scale_concat_value_firstsliceentryoutput) + (dst_positive_scale_concat_value_firstsliceentryoutput))) + (((dst_negative_code_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)) * S ((dst_negative_code_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)) + ((dst_negative_scale_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)))) + ((((dst_negative_code_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)) * S ((dst_negative_code_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)) + ((dst_negative_scale_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput))) + (((dst_negative_code_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)) * S ((dst_negative_code_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)) + ((dst_negative_scale_concat_value_firstsliceentryoutput) + (dst_negative_scale_concat_value_firstsliceentryoutput)))))) /\ (((((exists ff_h_pvs_concat_value_firstsliceentryoutputpositive. ff_h_pvs_concat_value_firstsliceentryoutputpositive + S (dst_positive_concat_value_firstsliceentryoutput) = S ((S (srs_index_concat_value_firstslice)) * dst_positive_scale_concat_value_firstsliceentryoutput)) /\ exists ff_q_pvs_concat_value_firstsliceentryoutputpositive. dst_positive_code_concat_value_firstsliceentryoutput = ff_q_pvs_concat_value_firstsliceentryoutputpositive * S ((S (srs_index_concat_value_firstslice)) * dst_positive_scale_concat_value_firstsliceentryoutput) + (dst_positive_concat_value_firstsliceentryoutput))) /\ (((((exists ff_h_pvs_concat_value_firstsliceentryoutputnegative. ff_h_pvs_concat_value_firstsliceentryoutputnegative + S (dst_negative_concat_value_firstsliceentryoutput) = S ((S (srs_index_concat_value_firstslice)) * dst_negative_scale_concat_value_firstsliceentryoutput)) /\ exists ff_q_pvs_concat_value_firstsliceentryoutputnegative. dst_negative_code_concat_value_firstsliceentryoutput = ff_q_pvs_concat_value_firstsliceentryoutputnegative * S ((S (srs_index_concat_value_firstslice)) * dst_negative_scale_concat_value_firstsliceentryoutput) + (dst_negative_concat_value_firstsliceentryoutput))) /\ (exists ge_balance_positive_concat_value_firstsliceentryoutputvalue ge_balance_negative_concat_value_firstsliceentryoutputvalue. (((((srs_value_concat_value_firstslice) = 2 * (ge_balance_positive_concat_value_firstsliceentryoutputvalue) /\ (ge_balance_negative_concat_value_firstsliceentryoutputvalue) = 0) \/ exists ge_signed_half_concat_value_firstsliceentryoutputvaluedecode. (((srs_value_concat_value_firstslice) = 2 * ge_signed_half_concat_value_firstsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_concat_value_firstsliceentryoutputvalue) = 0) /\ (ge_balance_negative_concat_value_firstsliceentryoutputvalue) = S ge_signed_half_concat_value_firstsliceentryoutputvaluedecode))) /\ ((dst_positive_concat_value_firstsliceentryoutput) + ge_balance_negative_concat_value_firstsliceentryoutputvalue = (dst_negative_concat_value_firstsliceentryoutput) + ge_balance_positive_concat_value_firstsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_concat_value_firstsum dst_positive_scale_concat_value_firstsum dst_negative_code_concat_value_firstsum dst_negative_scale_concat_value_firstsum dst_positive_sum_concat_value_firstsum dst_negative_sum_concat_value_firstsum. (((srs_slice_concat_value_first) = (((((dst_positive_code_concat_value_firstsum) + (dst_positive_scale_concat_value_firstsum)) * S ((dst_positive_code_concat_value_firstsum) + (dst_positive_scale_concat_value_firstsum)) + ((dst_positive_scale_concat_value_firstsum) + (dst_positive_scale_concat_value_firstsum))) + (((dst_negative_code_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)) * S ((dst_negative_code_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)) + ((dst_negative_scale_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)))) * S ((((dst_positive_code_concat_value_firstsum) + (dst_positive_scale_concat_value_firstsum)) * S ((dst_positive_code_concat_value_firstsum) + (dst_positive_scale_concat_value_firstsum)) + ((dst_positive_scale_concat_value_firstsum) + (dst_positive_scale_concat_value_firstsum))) + (((dst_negative_code_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)) * S ((dst_negative_code_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)) + ((dst_negative_scale_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)))) + ((((dst_negative_code_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)) * S ((dst_negative_code_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)) + ((dst_negative_scale_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum))) + (((dst_negative_code_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)) * S ((dst_negative_code_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)) + ((dst_negative_scale_concat_value_firstsum) + (dst_negative_scale_concat_value_firstsum)))))) /\ (((exists fs_u_dst_concat_value_firstsumpositive fs_v_dst_concat_value_firstsumpositive. ((((exists fs_h_dst_concat_value_firstsumpositive_body_start. fs_h_dst_concat_value_firstsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_value_firstsumpositive)) /\ exists fs_q_dst_concat_value_firstsumpositive_body_start. fs_u_dst_concat_value_firstsumpositive = fs_q_dst_concat_value_firstsumpositive_body_start * S ((S (0)) * fs_v_dst_concat_value_firstsumpositive) + (0))) /\ ((((exists fs_h_dst_concat_value_firstsumpositive_body_terminal. fs_h_dst_concat_value_firstsumpositive_body_terminal + S (dst_positive_sum_concat_value_firstsum) = S ((S (p)) * fs_v_dst_concat_value_firstsumpositive)) /\ exists fs_q_dst_concat_value_firstsumpositive_body_terminal. fs_u_dst_concat_value_firstsumpositive = fs_q_dst_concat_value_firstsumpositive_body_terminal * S ((S (p)) * fs_v_dst_concat_value_firstsumpositive) + (dst_positive_sum_concat_value_firstsum))) /\ forall fs_i_dst_concat_value_firstsumpositive_body_steps. (exists fs_lt_dst_concat_value_firstsumpositive_body_steps_bound. fs_lt_dst_concat_value_firstsumpositive_body_steps_bound + S fs_i_dst_concat_value_firstsumpositive_body_steps = p) -> exists fs_a_dst_concat_value_firstsumpositive_body_steps fs_r_dst_concat_value_firstsumpositive_body_steps fs_s_dst_concat_value_firstsumpositive_body_steps. ((((exists fs_h_dst_concat_value_firstsumpositive_body_steps_summand. fs_h_dst_concat_value_firstsumpositive_body_steps_summand + S (fs_a_dst_concat_value_firstsumpositive_body_steps) = S ((S (fs_i_dst_concat_value_firstsumpositive_body_steps)) * dst_positive_scale_concat_value_firstsum)) /\ exists fs_q_dst_concat_value_firstsumpositive_body_steps_summand. dst_positive_code_concat_value_firstsum = fs_q_dst_concat_value_firstsumpositive_body_steps_summand * S ((S (fs_i_dst_concat_value_firstsumpositive_body_steps)) * dst_positive_scale_concat_value_firstsum) + (fs_a_dst_concat_value_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_value_firstsumpositive_body_steps_partial. fs_h_dst_concat_value_firstsumpositive_body_steps_partial + S (fs_r_dst_concat_value_firstsumpositive_body_steps) = S ((S (fs_i_dst_concat_value_firstsumpositive_body_steps)) * fs_v_dst_concat_value_firstsumpositive)) /\ exists fs_q_dst_concat_value_firstsumpositive_body_steps_partial. fs_u_dst_concat_value_firstsumpositive = fs_q_dst_concat_value_firstsumpositive_body_steps_partial * S ((S (fs_i_dst_concat_value_firstsumpositive_body_steps)) * fs_v_dst_concat_value_firstsumpositive) + (fs_r_dst_concat_value_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_value_firstsumpositive_body_steps_successor. fs_h_dst_concat_value_firstsumpositive_body_steps_successor + S (fs_s_dst_concat_value_firstsumpositive_body_steps) = S ((S (S fs_i_dst_concat_value_firstsumpositive_body_steps)) * fs_v_dst_concat_value_firstsumpositive)) /\ exists fs_q_dst_concat_value_firstsumpositive_body_steps_successor. fs_u_dst_concat_value_firstsumpositive = fs_q_dst_concat_value_firstsumpositive_body_steps_successor * S ((S (S fs_i_dst_concat_value_firstsumpositive_body_steps)) * fs_v_dst_concat_value_firstsumpositive) + (fs_s_dst_concat_value_firstsumpositive_body_steps))) /\ fs_s_dst_concat_value_firstsumpositive_body_steps = fs_r_dst_concat_value_firstsumpositive_body_steps + fs_a_dst_concat_value_firstsumpositive_body_steps)))))) /\ (((exists fs_u_dst_concat_value_firstsumnegative fs_v_dst_concat_value_firstsumnegative. ((((exists fs_h_dst_concat_value_firstsumnegative_body_start. fs_h_dst_concat_value_firstsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_value_firstsumnegative)) /\ exists fs_q_dst_concat_value_firstsumnegative_body_start. fs_u_dst_concat_value_firstsumnegative = fs_q_dst_concat_value_firstsumnegative_body_start * S ((S (0)) * fs_v_dst_concat_value_firstsumnegative) + (0))) /\ ((((exists fs_h_dst_concat_value_firstsumnegative_body_terminal. fs_h_dst_concat_value_firstsumnegative_body_terminal + S (dst_negative_sum_concat_value_firstsum) = S ((S (p)) * fs_v_dst_concat_value_firstsumnegative)) /\ exists fs_q_dst_concat_value_firstsumnegative_body_terminal. fs_u_dst_concat_value_firstsumnegative = fs_q_dst_concat_value_firstsumnegative_body_terminal * S ((S (p)) * fs_v_dst_concat_value_firstsumnegative) + (dst_negative_sum_concat_value_firstsum))) /\ forall fs_i_dst_concat_value_firstsumnegative_body_steps. (exists fs_lt_dst_concat_value_firstsumnegative_body_steps_bound. fs_lt_dst_concat_value_firstsumnegative_body_steps_bound + S fs_i_dst_concat_value_firstsumnegative_body_steps = p) -> exists fs_a_dst_concat_value_firstsumnegative_body_steps fs_r_dst_concat_value_firstsumnegative_body_steps fs_s_dst_concat_value_firstsumnegative_body_steps. ((((exists fs_h_dst_concat_value_firstsumnegative_body_steps_summand. fs_h_dst_concat_value_firstsumnegative_body_steps_summand + S (fs_a_dst_concat_value_firstsumnegative_body_steps) = S ((S (fs_i_dst_concat_value_firstsumnegative_body_steps)) * dst_negative_scale_concat_value_firstsum)) /\ exists fs_q_dst_concat_value_firstsumnegative_body_steps_summand. dst_negative_code_concat_value_firstsum = fs_q_dst_concat_value_firstsumnegative_body_steps_summand * S ((S (fs_i_dst_concat_value_firstsumnegative_body_steps)) * dst_negative_scale_concat_value_firstsum) + (fs_a_dst_concat_value_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_value_firstsumnegative_body_steps_partial. fs_h_dst_concat_value_firstsumnegative_body_steps_partial + S (fs_r_dst_concat_value_firstsumnegative_body_steps) = S ((S (fs_i_dst_concat_value_firstsumnegative_body_steps)) * fs_v_dst_concat_value_firstsumnegative)) /\ exists fs_q_dst_concat_value_firstsumnegative_body_steps_partial. fs_u_dst_concat_value_firstsumnegative = fs_q_dst_concat_value_firstsumnegative_body_steps_partial * S ((S (fs_i_dst_concat_value_firstsumnegative_body_steps)) * fs_v_dst_concat_value_firstsumnegative) + (fs_r_dst_concat_value_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_value_firstsumnegative_body_steps_successor. fs_h_dst_concat_value_firstsumnegative_body_steps_successor + S (fs_s_dst_concat_value_firstsumnegative_body_steps) = S ((S (S fs_i_dst_concat_value_firstsumnegative_body_steps)) * fs_v_dst_concat_value_firstsumnegative)) /\ exists fs_q_dst_concat_value_firstsumnegative_body_steps_successor. fs_u_dst_concat_value_firstsumnegative = fs_q_dst_concat_value_firstsumnegative_body_steps_successor * S ((S (S fs_i_dst_concat_value_firstsumnegative_body_steps)) * fs_v_dst_concat_value_firstsumnegative) + (fs_s_dst_concat_value_firstsumnegative_body_steps))) /\ fs_s_dst_concat_value_firstsumnegative_body_steps = fs_r_dst_concat_value_firstsumnegative_body_steps + fs_a_dst_concat_value_firstsumnegative_body_steps)))))) /\ (exists ge_balance_positive_concat_value_firstsumresult ge_balance_negative_concat_value_firstsumresult. (((((a) = 2 * (ge_balance_positive_concat_value_firstsumresult) /\ (ge_balance_negative_concat_value_firstsumresult) = 0) \/ exists ge_signed_half_concat_value_firstsumresultdecode. (((a) = 2 * ge_signed_half_concat_value_firstsumresultdecode + 1 /\ (ge_balance_positive_concat_value_firstsumresult) = 0) /\ (ge_balance_negative_concat_value_firstsumresult) = S ge_signed_half_concat_value_firstsumresultdecode))) /\ ((dst_positive_sum_concat_value_firstsum) + ge_balance_negative_concat_value_firstsumresult = (dst_negative_sum_concat_value_firstsum) + ge_balance_positive_concat_value_firstsumresult))))))))))) -> (exists srs_slice_concat_value_second. ((((exists dst_positive_code_concat_value_secondslicesource_table dst_positive_scale_concat_value_secondslicesource_table dst_negative_code_concat_value_secondslicesource_table dst_negative_scale_concat_value_secondslicesource_table. (((F) = (((((dst_positive_code_concat_value_secondslicesource_table) + (dst_positive_scale_concat_value_secondslicesource_table)) * S ((dst_positive_code_concat_value_secondslicesource_table) + (dst_positive_scale_concat_value_secondslicesource_table)) + ((dst_positive_scale_concat_value_secondslicesource_table) + (dst_positive_scale_concat_value_secondslicesource_table))) + (((dst_negative_code_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)) * S ((dst_negative_code_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)) + ((dst_negative_scale_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)))) * S ((((dst_positive_code_concat_value_secondslicesource_table) + (dst_positive_scale_concat_value_secondslicesource_table)) * S ((dst_positive_code_concat_value_secondslicesource_table) + (dst_positive_scale_concat_value_secondslicesource_table)) + ((dst_positive_scale_concat_value_secondslicesource_table) + (dst_positive_scale_concat_value_secondslicesource_table))) + (((dst_negative_code_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)) * S ((dst_negative_code_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)) + ((dst_negative_scale_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)))) + ((((dst_negative_code_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)) * S ((dst_negative_code_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)) + ((dst_negative_scale_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table))) + (((dst_negative_code_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)) * S ((dst_negative_code_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)) + ((dst_negative_scale_concat_value_secondslicesource_table) + (dst_negative_scale_concat_value_secondslicesource_table)))))) /\ (forall dst_index_concat_value_secondslicesource_table. (exists pvs_le_gap_concat_value_secondslicesource_tabledomain. pvs_le_gap_concat_value_secondslicesource_tabledomain + (dst_index_concat_value_secondslicesource_table) = (0)) -> exists dst_positive_concat_value_secondslicesource_table dst_negative_concat_value_secondslicesource_table dst_value_concat_value_secondslicesource_table. ((((exists ff_h_pvs_concat_value_secondslicesource_tableentrypositive. ff_h_pvs_concat_value_secondslicesource_tableentrypositive + S (dst_positive_concat_value_secondslicesource_table) = S ((S (dst_index_concat_value_secondslicesource_table)) * dst_positive_scale_concat_value_secondslicesource_table)) /\ exists ff_q_pvs_concat_value_secondslicesource_tableentrypositive. dst_positive_code_concat_value_secondslicesource_table = ff_q_pvs_concat_value_secondslicesource_tableentrypositive * S ((S (dst_index_concat_value_secondslicesource_table)) * dst_positive_scale_concat_value_secondslicesource_table) + (dst_positive_concat_value_secondslicesource_table))) /\ (((((exists ff_h_pvs_concat_value_secondslicesource_tableentrynegative. ff_h_pvs_concat_value_secondslicesource_tableentrynegative + S (dst_negative_concat_value_secondslicesource_table) = S ((S (dst_index_concat_value_secondslicesource_table)) * dst_negative_scale_concat_value_secondslicesource_table)) /\ exists ff_q_pvs_concat_value_secondslicesource_tableentrynegative. dst_negative_code_concat_value_secondslicesource_table = ff_q_pvs_concat_value_secondslicesource_tableentrynegative * S ((S (dst_index_concat_value_secondslicesource_table)) * dst_negative_scale_concat_value_secondslicesource_table) + (dst_negative_concat_value_secondslicesource_table))) /\ (exists ge_balance_positive_concat_value_secondslicesource_tableentryvalue ge_balance_negative_concat_value_secondslicesource_tableentryvalue. (((((dst_value_concat_value_secondslicesource_table) = 2 * (ge_balance_positive_concat_value_secondslicesource_tableentryvalue) /\ (ge_balance_negative_concat_value_secondslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_concat_value_secondslicesource_tableentryvaluedecode. (((dst_value_concat_value_secondslicesource_table) = 2 * ge_signed_half_concat_value_secondslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_value_secondslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_concat_value_secondslicesource_tableentryvalue) = S ge_signed_half_concat_value_secondslicesource_tableentryvaluedecode))) /\ ((dst_positive_concat_value_secondslicesource_table) + ge_balance_negative_concat_value_secondslicesource_tableentryvalue = (dst_negative_concat_value_secondslicesource_table) + ge_balance_positive_concat_value_secondslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_concat_value_secondsliceoutput_table dst_positive_scale_concat_value_secondsliceoutput_table dst_negative_code_concat_value_secondsliceoutput_table dst_negative_scale_concat_value_secondsliceoutput_table. (((srs_slice_concat_value_second) = (((((dst_positive_code_concat_value_secondsliceoutput_table) + (dst_positive_scale_concat_value_secondsliceoutput_table)) * S ((dst_positive_code_concat_value_secondsliceoutput_table) + (dst_positive_scale_concat_value_secondsliceoutput_table)) + ((dst_positive_scale_concat_value_secondsliceoutput_table) + (dst_positive_scale_concat_value_secondsliceoutput_table))) + (((dst_negative_code_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)) * S ((dst_negative_code_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)) + ((dst_negative_scale_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)))) * S ((((dst_positive_code_concat_value_secondsliceoutput_table) + (dst_positive_scale_concat_value_secondsliceoutput_table)) * S ((dst_positive_code_concat_value_secondsliceoutput_table) + (dst_positive_scale_concat_value_secondsliceoutput_table)) + ((dst_positive_scale_concat_value_secondsliceoutput_table) + (dst_positive_scale_concat_value_secondsliceoutput_table))) + (((dst_negative_code_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)) * S ((dst_negative_code_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)) + ((dst_negative_scale_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)))) + ((((dst_negative_code_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)) * S ((dst_negative_code_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)) + ((dst_negative_scale_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table))) + (((dst_negative_code_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)) * S ((dst_negative_code_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)) + ((dst_negative_scale_concat_value_secondsliceoutput_table) + (dst_negative_scale_concat_value_secondsliceoutput_table)))))) /\ (forall dst_index_concat_value_secondsliceoutput_table. (exists pvs_le_gap_concat_value_secondsliceoutput_tabledomain. pvs_le_gap_concat_value_secondsliceoutput_tabledomain + (dst_index_concat_value_secondsliceoutput_table) = (q)) -> exists dst_positive_concat_value_secondsliceoutput_table dst_negative_concat_value_secondsliceoutput_table dst_value_concat_value_secondsliceoutput_table. ((((exists ff_h_pvs_concat_value_secondsliceoutput_tableentrypositive. ff_h_pvs_concat_value_secondsliceoutput_tableentrypositive + S (dst_positive_concat_value_secondsliceoutput_table) = S ((S (dst_index_concat_value_secondsliceoutput_table)) * dst_positive_scale_concat_value_secondsliceoutput_table)) /\ exists ff_q_pvs_concat_value_secondsliceoutput_tableentrypositive. dst_positive_code_concat_value_secondsliceoutput_table = ff_q_pvs_concat_value_secondsliceoutput_tableentrypositive * S ((S (dst_index_concat_value_secondsliceoutput_table)) * dst_positive_scale_concat_value_secondsliceoutput_table) + (dst_positive_concat_value_secondsliceoutput_table))) /\ (((((exists ff_h_pvs_concat_value_secondsliceoutput_tableentrynegative. ff_h_pvs_concat_value_secondsliceoutput_tableentrynegative + S (dst_negative_concat_value_secondsliceoutput_table) = S ((S (dst_index_concat_value_secondsliceoutput_table)) * dst_negative_scale_concat_value_secondsliceoutput_table)) /\ exists ff_q_pvs_concat_value_secondsliceoutput_tableentrynegative. dst_negative_code_concat_value_secondsliceoutput_table = ff_q_pvs_concat_value_secondsliceoutput_tableentrynegative * S ((S (dst_index_concat_value_secondsliceoutput_table)) * dst_negative_scale_concat_value_secondsliceoutput_table) + (dst_negative_concat_value_secondsliceoutput_table))) /\ (exists ge_balance_positive_concat_value_secondsliceoutput_tableentryvalue ge_balance_negative_concat_value_secondsliceoutput_tableentryvalue. (((((dst_value_concat_value_secondsliceoutput_table) = 2 * (ge_balance_positive_concat_value_secondsliceoutput_tableentryvalue) /\ (ge_balance_negative_concat_value_secondsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_concat_value_secondsliceoutput_tableentryvaluedecode. (((dst_value_concat_value_secondsliceoutput_table) = 2 * ge_signed_half_concat_value_secondsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_value_secondsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_concat_value_secondsliceoutput_tableentryvalue) = S ge_signed_half_concat_value_secondsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_concat_value_secondsliceoutput_table) + ge_balance_negative_concat_value_secondsliceoutput_tableentryvalue = (dst_negative_concat_value_secondsliceoutput_table) + ge_balance_positive_concat_value_secondsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_concat_value_secondslice. (exists pvs_gap_concat_value_secondslicebound. pvs_gap_concat_value_secondslicebound + S (srs_index_concat_value_secondslice) = (q)) -> exists srs_value_concat_value_secondslice. (((exists dst_positive_code_concat_value_secondsliceentrysource dst_positive_scale_concat_value_secondsliceentrysource dst_negative_code_concat_value_secondsliceentrysource dst_negative_scale_concat_value_secondsliceentrysource dst_positive_concat_value_secondsliceentrysource dst_negative_concat_value_secondsliceentrysource. (((F) = (((((dst_positive_code_concat_value_secondsliceentrysource) + (dst_positive_scale_concat_value_secondsliceentrysource)) * S ((dst_positive_code_concat_value_secondsliceentrysource) + (dst_positive_scale_concat_value_secondsliceentrysource)) + ((dst_positive_scale_concat_value_secondsliceentrysource) + (dst_positive_scale_concat_value_secondsliceentrysource))) + (((dst_negative_code_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)) * S ((dst_negative_code_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)) + ((dst_negative_scale_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)))) * S ((((dst_positive_code_concat_value_secondsliceentrysource) + (dst_positive_scale_concat_value_secondsliceentrysource)) * S ((dst_positive_code_concat_value_secondsliceentrysource) + (dst_positive_scale_concat_value_secondsliceentrysource)) + ((dst_positive_scale_concat_value_secondsliceentrysource) + (dst_positive_scale_concat_value_secondsliceentrysource))) + (((dst_negative_code_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)) * S ((dst_negative_code_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)) + ((dst_negative_scale_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)))) + ((((dst_negative_code_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)) * S ((dst_negative_code_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)) + ((dst_negative_scale_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource))) + (((dst_negative_code_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)) * S ((dst_negative_code_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)) + ((dst_negative_scale_concat_value_secondsliceentrysource) + (dst_negative_scale_concat_value_secondsliceentrysource)))))) /\ (((((exists ff_h_pvs_concat_value_secondsliceentrysourcepositive. ff_h_pvs_concat_value_secondsliceentrysourcepositive + S (dst_positive_concat_value_secondsliceentrysource) = S ((S (((((o) + ((s) * (p)))) + ((s) * (srs_index_concat_value_secondslice))))) * dst_positive_scale_concat_value_secondsliceentrysource)) /\ exists ff_q_pvs_concat_value_secondsliceentrysourcepositive. dst_positive_code_concat_value_secondsliceentrysource = ff_q_pvs_concat_value_secondsliceentrysourcepositive * S ((S (((((o) + ((s) * (p)))) + ((s) * (srs_index_concat_value_secondslice))))) * dst_positive_scale_concat_value_secondsliceentrysource) + (dst_positive_concat_value_secondsliceentrysource))) /\ (((((exists ff_h_pvs_concat_value_secondsliceentrysourcenegative. ff_h_pvs_concat_value_secondsliceentrysourcenegative + S (dst_negative_concat_value_secondsliceentrysource) = S ((S (((((o) + ((s) * (p)))) + ((s) * (srs_index_concat_value_secondslice))))) * dst_negative_scale_concat_value_secondsliceentrysource)) /\ exists ff_q_pvs_concat_value_secondsliceentrysourcenegative. dst_negative_code_concat_value_secondsliceentrysource = ff_q_pvs_concat_value_secondsliceentrysourcenegative * S ((S (((((o) + ((s) * (p)))) + ((s) * (srs_index_concat_value_secondslice))))) * dst_negative_scale_concat_value_secondsliceentrysource) + (dst_negative_concat_value_secondsliceentrysource))) /\ (exists ge_balance_positive_concat_value_secondsliceentrysourcevalue ge_balance_negative_concat_value_secondsliceentrysourcevalue. (((((srs_value_concat_value_secondslice) = 2 * (ge_balance_positive_concat_value_secondsliceentrysourcevalue) /\ (ge_balance_negative_concat_value_secondsliceentrysourcevalue) = 0) \/ exists ge_signed_half_concat_value_secondsliceentrysourcevaluedecode. (((srs_value_concat_value_secondslice) = 2 * ge_signed_half_concat_value_secondsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_concat_value_secondsliceentrysourcevalue) = 0) /\ (ge_balance_negative_concat_value_secondsliceentrysourcevalue) = S ge_signed_half_concat_value_secondsliceentrysourcevaluedecode))) /\ ((dst_positive_concat_value_secondsliceentrysource) + ge_balance_negative_concat_value_secondsliceentrysourcevalue = (dst_negative_concat_value_secondsliceentrysource) + ge_balance_positive_concat_value_secondsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_concat_value_secondsliceentryoutput dst_positive_scale_concat_value_secondsliceentryoutput dst_negative_code_concat_value_secondsliceentryoutput dst_negative_scale_concat_value_secondsliceentryoutput dst_positive_concat_value_secondsliceentryoutput dst_negative_concat_value_secondsliceentryoutput. (((srs_slice_concat_value_second) = (((((dst_positive_code_concat_value_secondsliceentryoutput) + (dst_positive_scale_concat_value_secondsliceentryoutput)) * S ((dst_positive_code_concat_value_secondsliceentryoutput) + (dst_positive_scale_concat_value_secondsliceentryoutput)) + ((dst_positive_scale_concat_value_secondsliceentryoutput) + (dst_positive_scale_concat_value_secondsliceentryoutput))) + (((dst_negative_code_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)) * S ((dst_negative_code_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)) + ((dst_negative_scale_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)))) * S ((((dst_positive_code_concat_value_secondsliceentryoutput) + (dst_positive_scale_concat_value_secondsliceentryoutput)) * S ((dst_positive_code_concat_value_secondsliceentryoutput) + (dst_positive_scale_concat_value_secondsliceentryoutput)) + ((dst_positive_scale_concat_value_secondsliceentryoutput) + (dst_positive_scale_concat_value_secondsliceentryoutput))) + (((dst_negative_code_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)) * S ((dst_negative_code_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)) + ((dst_negative_scale_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)))) + ((((dst_negative_code_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)) * S ((dst_negative_code_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)) + ((dst_negative_scale_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput))) + (((dst_negative_code_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)) * S ((dst_negative_code_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)) + ((dst_negative_scale_concat_value_secondsliceentryoutput) + (dst_negative_scale_concat_value_secondsliceentryoutput)))))) /\ (((((exists ff_h_pvs_concat_value_secondsliceentryoutputpositive. ff_h_pvs_concat_value_secondsliceentryoutputpositive + S (dst_positive_concat_value_secondsliceentryoutput) = S ((S (srs_index_concat_value_secondslice)) * dst_positive_scale_concat_value_secondsliceentryoutput)) /\ exists ff_q_pvs_concat_value_secondsliceentryoutputpositive. dst_positive_code_concat_value_secondsliceentryoutput = ff_q_pvs_concat_value_secondsliceentryoutputpositive * S ((S (srs_index_concat_value_secondslice)) * dst_positive_scale_concat_value_secondsliceentryoutput) + (dst_positive_concat_value_secondsliceentryoutput))) /\ (((((exists ff_h_pvs_concat_value_secondsliceentryoutputnegative. ff_h_pvs_concat_value_secondsliceentryoutputnegative + S (dst_negative_concat_value_secondsliceentryoutput) = S ((S (srs_index_concat_value_secondslice)) * dst_negative_scale_concat_value_secondsliceentryoutput)) /\ exists ff_q_pvs_concat_value_secondsliceentryoutputnegative. dst_negative_code_concat_value_secondsliceentryoutput = ff_q_pvs_concat_value_secondsliceentryoutputnegative * S ((S (srs_index_concat_value_secondslice)) * dst_negative_scale_concat_value_secondsliceentryoutput) + (dst_negative_concat_value_secondsliceentryoutput))) /\ (exists ge_balance_positive_concat_value_secondsliceentryoutputvalue ge_balance_negative_concat_value_secondsliceentryoutputvalue. (((((srs_value_concat_value_secondslice) = 2 * (ge_balance_positive_concat_value_secondsliceentryoutputvalue) /\ (ge_balance_negative_concat_value_secondsliceentryoutputvalue) = 0) \/ exists ge_signed_half_concat_value_secondsliceentryoutputvaluedecode. (((srs_value_concat_value_secondslice) = 2 * ge_signed_half_concat_value_secondsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_concat_value_secondsliceentryoutputvalue) = 0) /\ (ge_balance_negative_concat_value_secondsliceentryoutputvalue) = S ge_signed_half_concat_value_secondsliceentryoutputvaluedecode))) /\ ((dst_positive_concat_value_secondsliceentryoutput) + ge_balance_negative_concat_value_secondsliceentryoutputvalue = (dst_negative_concat_value_secondsliceentryoutput) + ge_balance_positive_concat_value_secondsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_concat_value_secondsum dst_positive_scale_concat_value_secondsum dst_negative_code_concat_value_secondsum dst_negative_scale_concat_value_secondsum dst_positive_sum_concat_value_secondsum dst_negative_sum_concat_value_secondsum. (((srs_slice_concat_value_second) = (((((dst_positive_code_concat_value_secondsum) + (dst_positive_scale_concat_value_secondsum)) * S ((dst_positive_code_concat_value_secondsum) + (dst_positive_scale_concat_value_secondsum)) + ((dst_positive_scale_concat_value_secondsum) + (dst_positive_scale_concat_value_secondsum))) + (((dst_negative_code_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)) * S ((dst_negative_code_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)) + ((dst_negative_scale_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)))) * S ((((dst_positive_code_concat_value_secondsum) + (dst_positive_scale_concat_value_secondsum)) * S ((dst_positive_code_concat_value_secondsum) + (dst_positive_scale_concat_value_secondsum)) + ((dst_positive_scale_concat_value_secondsum) + (dst_positive_scale_concat_value_secondsum))) + (((dst_negative_code_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)) * S ((dst_negative_code_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)) + ((dst_negative_scale_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)))) + ((((dst_negative_code_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)) * S ((dst_negative_code_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)) + ((dst_negative_scale_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum))) + (((dst_negative_code_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)) * S ((dst_negative_code_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)) + ((dst_negative_scale_concat_value_secondsum) + (dst_negative_scale_concat_value_secondsum)))))) /\ (((exists fs_u_dst_concat_value_secondsumpositive fs_v_dst_concat_value_secondsumpositive. ((((exists fs_h_dst_concat_value_secondsumpositive_body_start. fs_h_dst_concat_value_secondsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_value_secondsumpositive)) /\ exists fs_q_dst_concat_value_secondsumpositive_body_start. fs_u_dst_concat_value_secondsumpositive = fs_q_dst_concat_value_secondsumpositive_body_start * S ((S (0)) * fs_v_dst_concat_value_secondsumpositive) + (0))) /\ ((((exists fs_h_dst_concat_value_secondsumpositive_body_terminal. fs_h_dst_concat_value_secondsumpositive_body_terminal + S (dst_positive_sum_concat_value_secondsum) = S ((S (q)) * fs_v_dst_concat_value_secondsumpositive)) /\ exists fs_q_dst_concat_value_secondsumpositive_body_terminal. fs_u_dst_concat_value_secondsumpositive = fs_q_dst_concat_value_secondsumpositive_body_terminal * S ((S (q)) * fs_v_dst_concat_value_secondsumpositive) + (dst_positive_sum_concat_value_secondsum))) /\ forall fs_i_dst_concat_value_secondsumpositive_body_steps. (exists fs_lt_dst_concat_value_secondsumpositive_body_steps_bound. fs_lt_dst_concat_value_secondsumpositive_body_steps_bound + S fs_i_dst_concat_value_secondsumpositive_body_steps = q) -> exists fs_a_dst_concat_value_secondsumpositive_body_steps fs_r_dst_concat_value_secondsumpositive_body_steps fs_s_dst_concat_value_secondsumpositive_body_steps. ((((exists fs_h_dst_concat_value_secondsumpositive_body_steps_summand. fs_h_dst_concat_value_secondsumpositive_body_steps_summand + S (fs_a_dst_concat_value_secondsumpositive_body_steps) = S ((S (fs_i_dst_concat_value_secondsumpositive_body_steps)) * dst_positive_scale_concat_value_secondsum)) /\ exists fs_q_dst_concat_value_secondsumpositive_body_steps_summand. dst_positive_code_concat_value_secondsum = fs_q_dst_concat_value_secondsumpositive_body_steps_summand * S ((S (fs_i_dst_concat_value_secondsumpositive_body_steps)) * dst_positive_scale_concat_value_secondsum) + (fs_a_dst_concat_value_secondsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_value_secondsumpositive_body_steps_partial. fs_h_dst_concat_value_secondsumpositive_body_steps_partial + S (fs_r_dst_concat_value_secondsumpositive_body_steps) = S ((S (fs_i_dst_concat_value_secondsumpositive_body_steps)) * fs_v_dst_concat_value_secondsumpositive)) /\ exists fs_q_dst_concat_value_secondsumpositive_body_steps_partial. fs_u_dst_concat_value_secondsumpositive = fs_q_dst_concat_value_secondsumpositive_body_steps_partial * S ((S (fs_i_dst_concat_value_secondsumpositive_body_steps)) * fs_v_dst_concat_value_secondsumpositive) + (fs_r_dst_concat_value_secondsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_value_secondsumpositive_body_steps_successor. fs_h_dst_concat_value_secondsumpositive_body_steps_successor + S (fs_s_dst_concat_value_secondsumpositive_body_steps) = S ((S (S fs_i_dst_concat_value_secondsumpositive_body_steps)) * fs_v_dst_concat_value_secondsumpositive)) /\ exists fs_q_dst_concat_value_secondsumpositive_body_steps_successor. fs_u_dst_concat_value_secondsumpositive = fs_q_dst_concat_value_secondsumpositive_body_steps_successor * S ((S (S fs_i_dst_concat_value_secondsumpositive_body_steps)) * fs_v_dst_concat_value_secondsumpositive) + (fs_s_dst_concat_value_secondsumpositive_body_steps))) /\ fs_s_dst_concat_value_secondsumpositive_body_steps = fs_r_dst_concat_value_secondsumpositive_body_steps + fs_a_dst_concat_value_secondsumpositive_body_steps)))))) /\ (((exists fs_u_dst_concat_value_secondsumnegative fs_v_dst_concat_value_secondsumnegative. ((((exists fs_h_dst_concat_value_secondsumnegative_body_start. fs_h_dst_concat_value_secondsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_value_secondsumnegative)) /\ exists fs_q_dst_concat_value_secondsumnegative_body_start. fs_u_dst_concat_value_secondsumnegative = fs_q_dst_concat_value_secondsumnegative_body_start * S ((S (0)) * fs_v_dst_concat_value_secondsumnegative) + (0))) /\ ((((exists fs_h_dst_concat_value_secondsumnegative_body_terminal. fs_h_dst_concat_value_secondsumnegative_body_terminal + S (dst_negative_sum_concat_value_secondsum) = S ((S (q)) * fs_v_dst_concat_value_secondsumnegative)) /\ exists fs_q_dst_concat_value_secondsumnegative_body_terminal. fs_u_dst_concat_value_secondsumnegative = fs_q_dst_concat_value_secondsumnegative_body_terminal * S ((S (q)) * fs_v_dst_concat_value_secondsumnegative) + (dst_negative_sum_concat_value_secondsum))) /\ forall fs_i_dst_concat_value_secondsumnegative_body_steps. (exists fs_lt_dst_concat_value_secondsumnegative_body_steps_bound. fs_lt_dst_concat_value_secondsumnegative_body_steps_bound + S fs_i_dst_concat_value_secondsumnegative_body_steps = q) -> exists fs_a_dst_concat_value_secondsumnegative_body_steps fs_r_dst_concat_value_secondsumnegative_body_steps fs_s_dst_concat_value_secondsumnegative_body_steps. ((((exists fs_h_dst_concat_value_secondsumnegative_body_steps_summand. fs_h_dst_concat_value_secondsumnegative_body_steps_summand + S (fs_a_dst_concat_value_secondsumnegative_body_steps) = S ((S (fs_i_dst_concat_value_secondsumnegative_body_steps)) * dst_negative_scale_concat_value_secondsum)) /\ exists fs_q_dst_concat_value_secondsumnegative_body_steps_summand. dst_negative_code_concat_value_secondsum = fs_q_dst_concat_value_secondsumnegative_body_steps_summand * S ((S (fs_i_dst_concat_value_secondsumnegative_body_steps)) * dst_negative_scale_concat_value_secondsum) + (fs_a_dst_concat_value_secondsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_value_secondsumnegative_body_steps_partial. fs_h_dst_concat_value_secondsumnegative_body_steps_partial + S (fs_r_dst_concat_value_secondsumnegative_body_steps) = S ((S (fs_i_dst_concat_value_secondsumnegative_body_steps)) * fs_v_dst_concat_value_secondsumnegative)) /\ exists fs_q_dst_concat_value_secondsumnegative_body_steps_partial. fs_u_dst_concat_value_secondsumnegative = fs_q_dst_concat_value_secondsumnegative_body_steps_partial * S ((S (fs_i_dst_concat_value_secondsumnegative_body_steps)) * fs_v_dst_concat_value_secondsumnegative) + (fs_r_dst_concat_value_secondsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_value_secondsumnegative_body_steps_successor. fs_h_dst_concat_value_secondsumnegative_body_steps_successor + S (fs_s_dst_concat_value_secondsumnegative_body_steps) = S ((S (S fs_i_dst_concat_value_secondsumnegative_body_steps)) * fs_v_dst_concat_value_secondsumnegative)) /\ exists fs_q_dst_concat_value_secondsumnegative_body_steps_successor. fs_u_dst_concat_value_secondsumnegative = fs_q_dst_concat_value_secondsumnegative_body_steps_successor * S ((S (S fs_i_dst_concat_value_secondsumnegative_body_steps)) * fs_v_dst_concat_value_secondsumnegative) + (fs_s_dst_concat_value_secondsumnegative_body_steps))) /\ fs_s_dst_concat_value_secondsumnegative_body_steps = fs_r_dst_concat_value_secondsumnegative_body_steps + fs_a_dst_concat_value_secondsumnegative_body_steps)))))) /\ (exists ge_balance_positive_concat_value_secondsumresult ge_balance_negative_concat_value_secondsumresult. (((((b) = 2 * (ge_balance_positive_concat_value_secondsumresult) /\ (ge_balance_negative_concat_value_secondsumresult) = 0) \/ exists ge_signed_half_concat_value_secondsumresultdecode. (((b) = 2 * ge_signed_half_concat_value_secondsumresultdecode + 1 /\ (ge_balance_positive_concat_value_secondsumresult) = 0) /\ (ge_balance_negative_concat_value_secondsumresult) = S ge_signed_half_concat_value_secondsumresultdecode))) /\ ((dst_positive_sum_concat_value_secondsum) + ge_balance_negative_concat_value_secondsumresult = (dst_negative_sum_concat_value_secondsum) + ge_balance_positive_concat_value_secondsumresult))))))))))) -> (exists srs_slice_concat_value_total. ((((exists dst_positive_code_concat_value_totalslicesource_table dst_positive_scale_concat_value_totalslicesource_table dst_negative_code_concat_value_totalslicesource_table dst_negative_scale_concat_value_totalslicesource_table. (((F) = (((((dst_positive_code_concat_value_totalslicesource_table) + (dst_positive_scale_concat_value_totalslicesource_table)) * S ((dst_positive_code_concat_value_totalslicesource_table) + (dst_positive_scale_concat_value_totalslicesource_table)) + ((dst_positive_scale_concat_value_totalslicesource_table) + (dst_positive_scale_concat_value_totalslicesource_table))) + (((dst_negative_code_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)) * S ((dst_negative_code_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)) + ((dst_negative_scale_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)))) * S ((((dst_positive_code_concat_value_totalslicesource_table) + (dst_positive_scale_concat_value_totalslicesource_table)) * S ((dst_positive_code_concat_value_totalslicesource_table) + (dst_positive_scale_concat_value_totalslicesource_table)) + ((dst_positive_scale_concat_value_totalslicesource_table) + (dst_positive_scale_concat_value_totalslicesource_table))) + (((dst_negative_code_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)) * S ((dst_negative_code_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)) + ((dst_negative_scale_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)))) + ((((dst_negative_code_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)) * S ((dst_negative_code_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)) + ((dst_negative_scale_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table))) + (((dst_negative_code_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)) * S ((dst_negative_code_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)) + ((dst_negative_scale_concat_value_totalslicesource_table) + (dst_negative_scale_concat_value_totalslicesource_table)))))) /\ (forall dst_index_concat_value_totalslicesource_table. (exists pvs_le_gap_concat_value_totalslicesource_tabledomain. pvs_le_gap_concat_value_totalslicesource_tabledomain + (dst_index_concat_value_totalslicesource_table) = (0)) -> exists dst_positive_concat_value_totalslicesource_table dst_negative_concat_value_totalslicesource_table dst_value_concat_value_totalslicesource_table. ((((exists ff_h_pvs_concat_value_totalslicesource_tableentrypositive. ff_h_pvs_concat_value_totalslicesource_tableentrypositive + S (dst_positive_concat_value_totalslicesource_table) = S ((S (dst_index_concat_value_totalslicesource_table)) * dst_positive_scale_concat_value_totalslicesource_table)) /\ exists ff_q_pvs_concat_value_totalslicesource_tableentrypositive. dst_positive_code_concat_value_totalslicesource_table = ff_q_pvs_concat_value_totalslicesource_tableentrypositive * S ((S (dst_index_concat_value_totalslicesource_table)) * dst_positive_scale_concat_value_totalslicesource_table) + (dst_positive_concat_value_totalslicesource_table))) /\ (((((exists ff_h_pvs_concat_value_totalslicesource_tableentrynegative. ff_h_pvs_concat_value_totalslicesource_tableentrynegative + S (dst_negative_concat_value_totalslicesource_table) = S ((S (dst_index_concat_value_totalslicesource_table)) * dst_negative_scale_concat_value_totalslicesource_table)) /\ exists ff_q_pvs_concat_value_totalslicesource_tableentrynegative. dst_negative_code_concat_value_totalslicesource_table = ff_q_pvs_concat_value_totalslicesource_tableentrynegative * S ((S (dst_index_concat_value_totalslicesource_table)) * dst_negative_scale_concat_value_totalslicesource_table) + (dst_negative_concat_value_totalslicesource_table))) /\ (exists ge_balance_positive_concat_value_totalslicesource_tableentryvalue ge_balance_negative_concat_value_totalslicesource_tableentryvalue. (((((dst_value_concat_value_totalslicesource_table) = 2 * (ge_balance_positive_concat_value_totalslicesource_tableentryvalue) /\ (ge_balance_negative_concat_value_totalslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_concat_value_totalslicesource_tableentryvaluedecode. (((dst_value_concat_value_totalslicesource_table) = 2 * ge_signed_half_concat_value_totalslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_value_totalslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_concat_value_totalslicesource_tableentryvalue) = S ge_signed_half_concat_value_totalslicesource_tableentryvaluedecode))) /\ ((dst_positive_concat_value_totalslicesource_table) + ge_balance_negative_concat_value_totalslicesource_tableentryvalue = (dst_negative_concat_value_totalslicesource_table) + ge_balance_positive_concat_value_totalslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_concat_value_totalsliceoutput_table dst_positive_scale_concat_value_totalsliceoutput_table dst_negative_code_concat_value_totalsliceoutput_table dst_negative_scale_concat_value_totalsliceoutput_table. (((srs_slice_concat_value_total) = (((((dst_positive_code_concat_value_totalsliceoutput_table) + (dst_positive_scale_concat_value_totalsliceoutput_table)) * S ((dst_positive_code_concat_value_totalsliceoutput_table) + (dst_positive_scale_concat_value_totalsliceoutput_table)) + ((dst_positive_scale_concat_value_totalsliceoutput_table) + (dst_positive_scale_concat_value_totalsliceoutput_table))) + (((dst_negative_code_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)) * S ((dst_negative_code_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)) + ((dst_negative_scale_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)))) * S ((((dst_positive_code_concat_value_totalsliceoutput_table) + (dst_positive_scale_concat_value_totalsliceoutput_table)) * S ((dst_positive_code_concat_value_totalsliceoutput_table) + (dst_positive_scale_concat_value_totalsliceoutput_table)) + ((dst_positive_scale_concat_value_totalsliceoutput_table) + (dst_positive_scale_concat_value_totalsliceoutput_table))) + (((dst_negative_code_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)) * S ((dst_negative_code_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)) + ((dst_negative_scale_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)))) + ((((dst_negative_code_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)) * S ((dst_negative_code_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)) + ((dst_negative_scale_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table))) + (((dst_negative_code_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)) * S ((dst_negative_code_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)) + ((dst_negative_scale_concat_value_totalsliceoutput_table) + (dst_negative_scale_concat_value_totalsliceoutput_table)))))) /\ (forall dst_index_concat_value_totalsliceoutput_table. (exists pvs_le_gap_concat_value_totalsliceoutput_tabledomain. pvs_le_gap_concat_value_totalsliceoutput_tabledomain + (dst_index_concat_value_totalsliceoutput_table) = (p+q)) -> exists dst_positive_concat_value_totalsliceoutput_table dst_negative_concat_value_totalsliceoutput_table dst_value_concat_value_totalsliceoutput_table. ((((exists ff_h_pvs_concat_value_totalsliceoutput_tableentrypositive. ff_h_pvs_concat_value_totalsliceoutput_tableentrypositive + S (dst_positive_concat_value_totalsliceoutput_table) = S ((S (dst_index_concat_value_totalsliceoutput_table)) * dst_positive_scale_concat_value_totalsliceoutput_table)) /\ exists ff_q_pvs_concat_value_totalsliceoutput_tableentrypositive. dst_positive_code_concat_value_totalsliceoutput_table = ff_q_pvs_concat_value_totalsliceoutput_tableentrypositive * S ((S (dst_index_concat_value_totalsliceoutput_table)) * dst_positive_scale_concat_value_totalsliceoutput_table) + (dst_positive_concat_value_totalsliceoutput_table))) /\ (((((exists ff_h_pvs_concat_value_totalsliceoutput_tableentrynegative. ff_h_pvs_concat_value_totalsliceoutput_tableentrynegative + S (dst_negative_concat_value_totalsliceoutput_table) = S ((S (dst_index_concat_value_totalsliceoutput_table)) * dst_negative_scale_concat_value_totalsliceoutput_table)) /\ exists ff_q_pvs_concat_value_totalsliceoutput_tableentrynegative. dst_negative_code_concat_value_totalsliceoutput_table = ff_q_pvs_concat_value_totalsliceoutput_tableentrynegative * S ((S (dst_index_concat_value_totalsliceoutput_table)) * dst_negative_scale_concat_value_totalsliceoutput_table) + (dst_negative_concat_value_totalsliceoutput_table))) /\ (exists ge_balance_positive_concat_value_totalsliceoutput_tableentryvalue ge_balance_negative_concat_value_totalsliceoutput_tableentryvalue. (((((dst_value_concat_value_totalsliceoutput_table) = 2 * (ge_balance_positive_concat_value_totalsliceoutput_tableentryvalue) /\ (ge_balance_negative_concat_value_totalsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_concat_value_totalsliceoutput_tableentryvaluedecode. (((dst_value_concat_value_totalsliceoutput_table) = 2 * ge_signed_half_concat_value_totalsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_value_totalsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_concat_value_totalsliceoutput_tableentryvalue) = S ge_signed_half_concat_value_totalsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_concat_value_totalsliceoutput_table) + ge_balance_negative_concat_value_totalsliceoutput_tableentryvalue = (dst_negative_concat_value_totalsliceoutput_table) + ge_balance_positive_concat_value_totalsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_concat_value_totalslice. (exists pvs_gap_concat_value_totalslicebound. pvs_gap_concat_value_totalslicebound + S (srs_index_concat_value_totalslice) = (p+q)) -> exists srs_value_concat_value_totalslice. (((exists dst_positive_code_concat_value_totalsliceentrysource dst_positive_scale_concat_value_totalsliceentrysource dst_negative_code_concat_value_totalsliceentrysource dst_negative_scale_concat_value_totalsliceentrysource dst_positive_concat_value_totalsliceentrysource dst_negative_concat_value_totalsliceentrysource. (((F) = (((((dst_positive_code_concat_value_totalsliceentrysource) + (dst_positive_scale_concat_value_totalsliceentrysource)) * S ((dst_positive_code_concat_value_totalsliceentrysource) + (dst_positive_scale_concat_value_totalsliceentrysource)) + ((dst_positive_scale_concat_value_totalsliceentrysource) + (dst_positive_scale_concat_value_totalsliceentrysource))) + (((dst_negative_code_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)) * S ((dst_negative_code_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)) + ((dst_negative_scale_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)))) * S ((((dst_positive_code_concat_value_totalsliceentrysource) + (dst_positive_scale_concat_value_totalsliceentrysource)) * S ((dst_positive_code_concat_value_totalsliceentrysource) + (dst_positive_scale_concat_value_totalsliceentrysource)) + ((dst_positive_scale_concat_value_totalsliceentrysource) + (dst_positive_scale_concat_value_totalsliceentrysource))) + (((dst_negative_code_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)) * S ((dst_negative_code_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)) + ((dst_negative_scale_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)))) + ((((dst_negative_code_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)) * S ((dst_negative_code_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)) + ((dst_negative_scale_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource))) + (((dst_negative_code_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)) * S ((dst_negative_code_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)) + ((dst_negative_scale_concat_value_totalsliceentrysource) + (dst_negative_scale_concat_value_totalsliceentrysource)))))) /\ (((((exists ff_h_pvs_concat_value_totalsliceentrysourcepositive. ff_h_pvs_concat_value_totalsliceentrysourcepositive + S (dst_positive_concat_value_totalsliceentrysource) = S ((S (((o) + ((s) * (srs_index_concat_value_totalslice))))) * dst_positive_scale_concat_value_totalsliceentrysource)) /\ exists ff_q_pvs_concat_value_totalsliceentrysourcepositive. dst_positive_code_concat_value_totalsliceentrysource = ff_q_pvs_concat_value_totalsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_concat_value_totalslice))))) * dst_positive_scale_concat_value_totalsliceentrysource) + (dst_positive_concat_value_totalsliceentrysource))) /\ (((((exists ff_h_pvs_concat_value_totalsliceentrysourcenegative. ff_h_pvs_concat_value_totalsliceentrysourcenegative + S (dst_negative_concat_value_totalsliceentrysource) = S ((S (((o) + ((s) * (srs_index_concat_value_totalslice))))) * dst_negative_scale_concat_value_totalsliceentrysource)) /\ exists ff_q_pvs_concat_value_totalsliceentrysourcenegative. dst_negative_code_concat_value_totalsliceentrysource = ff_q_pvs_concat_value_totalsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_concat_value_totalslice))))) * dst_negative_scale_concat_value_totalsliceentrysource) + (dst_negative_concat_value_totalsliceentrysource))) /\ (exists ge_balance_positive_concat_value_totalsliceentrysourcevalue ge_balance_negative_concat_value_totalsliceentrysourcevalue. (((((srs_value_concat_value_totalslice) = 2 * (ge_balance_positive_concat_value_totalsliceentrysourcevalue) /\ (ge_balance_negative_concat_value_totalsliceentrysourcevalue) = 0) \/ exists ge_signed_half_concat_value_totalsliceentrysourcevaluedecode. (((srs_value_concat_value_totalslice) = 2 * ge_signed_half_concat_value_totalsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_concat_value_totalsliceentrysourcevalue) = 0) /\ (ge_balance_negative_concat_value_totalsliceentrysourcevalue) = S ge_signed_half_concat_value_totalsliceentrysourcevaluedecode))) /\ ((dst_positive_concat_value_totalsliceentrysource) + ge_balance_negative_concat_value_totalsliceentrysourcevalue = (dst_negative_concat_value_totalsliceentrysource) + ge_balance_positive_concat_value_totalsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_concat_value_totalsliceentryoutput dst_positive_scale_concat_value_totalsliceentryoutput dst_negative_code_concat_value_totalsliceentryoutput dst_negative_scale_concat_value_totalsliceentryoutput dst_positive_concat_value_totalsliceentryoutput dst_negative_concat_value_totalsliceentryoutput. (((srs_slice_concat_value_total) = (((((dst_positive_code_concat_value_totalsliceentryoutput) + (dst_positive_scale_concat_value_totalsliceentryoutput)) * S ((dst_positive_code_concat_value_totalsliceentryoutput) + (dst_positive_scale_concat_value_totalsliceentryoutput)) + ((dst_positive_scale_concat_value_totalsliceentryoutput) + (dst_positive_scale_concat_value_totalsliceentryoutput))) + (((dst_negative_code_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)) * S ((dst_negative_code_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)) + ((dst_negative_scale_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)))) * S ((((dst_positive_code_concat_value_totalsliceentryoutput) + (dst_positive_scale_concat_value_totalsliceentryoutput)) * S ((dst_positive_code_concat_value_totalsliceentryoutput) + (dst_positive_scale_concat_value_totalsliceentryoutput)) + ((dst_positive_scale_concat_value_totalsliceentryoutput) + (dst_positive_scale_concat_value_totalsliceentryoutput))) + (((dst_negative_code_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)) * S ((dst_negative_code_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)) + ((dst_negative_scale_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)))) + ((((dst_negative_code_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)) * S ((dst_negative_code_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)) + ((dst_negative_scale_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput))) + (((dst_negative_code_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)) * S ((dst_negative_code_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)) + ((dst_negative_scale_concat_value_totalsliceentryoutput) + (dst_negative_scale_concat_value_totalsliceentryoutput)))))) /\ (((((exists ff_h_pvs_concat_value_totalsliceentryoutputpositive. ff_h_pvs_concat_value_totalsliceentryoutputpositive + S (dst_positive_concat_value_totalsliceentryoutput) = S ((S (srs_index_concat_value_totalslice)) * dst_positive_scale_concat_value_totalsliceentryoutput)) /\ exists ff_q_pvs_concat_value_totalsliceentryoutputpositive. dst_positive_code_concat_value_totalsliceentryoutput = ff_q_pvs_concat_value_totalsliceentryoutputpositive * S ((S (srs_index_concat_value_totalslice)) * dst_positive_scale_concat_value_totalsliceentryoutput) + (dst_positive_concat_value_totalsliceentryoutput))) /\ (((((exists ff_h_pvs_concat_value_totalsliceentryoutputnegative. ff_h_pvs_concat_value_totalsliceentryoutputnegative + S (dst_negative_concat_value_totalsliceentryoutput) = S ((S (srs_index_concat_value_totalslice)) * dst_negative_scale_concat_value_totalsliceentryoutput)) /\ exists ff_q_pvs_concat_value_totalsliceentryoutputnegative. dst_negative_code_concat_value_totalsliceentryoutput = ff_q_pvs_concat_value_totalsliceentryoutputnegative * S ((S (srs_index_concat_value_totalslice)) * dst_negative_scale_concat_value_totalsliceentryoutput) + (dst_negative_concat_value_totalsliceentryoutput))) /\ (exists ge_balance_positive_concat_value_totalsliceentryoutputvalue ge_balance_negative_concat_value_totalsliceentryoutputvalue. (((((srs_value_concat_value_totalslice) = 2 * (ge_balance_positive_concat_value_totalsliceentryoutputvalue) /\ (ge_balance_negative_concat_value_totalsliceentryoutputvalue) = 0) \/ exists ge_signed_half_concat_value_totalsliceentryoutputvaluedecode. (((srs_value_concat_value_totalslice) = 2 * ge_signed_half_concat_value_totalsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_concat_value_totalsliceentryoutputvalue) = 0) /\ (ge_balance_negative_concat_value_totalsliceentryoutputvalue) = S ge_signed_half_concat_value_totalsliceentryoutputvaluedecode))) /\ ((dst_positive_concat_value_totalsliceentryoutput) + ge_balance_negative_concat_value_totalsliceentryoutputvalue = (dst_negative_concat_value_totalsliceentryoutput) + ge_balance_positive_concat_value_totalsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_concat_value_totalsum dst_positive_scale_concat_value_totalsum dst_negative_code_concat_value_totalsum dst_negative_scale_concat_value_totalsum dst_positive_sum_concat_value_totalsum dst_negative_sum_concat_value_totalsum. (((srs_slice_concat_value_total) = (((((dst_positive_code_concat_value_totalsum) + (dst_positive_scale_concat_value_totalsum)) * S ((dst_positive_code_concat_value_totalsum) + (dst_positive_scale_concat_value_totalsum)) + ((dst_positive_scale_concat_value_totalsum) + (dst_positive_scale_concat_value_totalsum))) + (((dst_negative_code_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)) * S ((dst_negative_code_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)) + ((dst_negative_scale_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)))) * S ((((dst_positive_code_concat_value_totalsum) + (dst_positive_scale_concat_value_totalsum)) * S ((dst_positive_code_concat_value_totalsum) + (dst_positive_scale_concat_value_totalsum)) + ((dst_positive_scale_concat_value_totalsum) + (dst_positive_scale_concat_value_totalsum))) + (((dst_negative_code_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)) * S ((dst_negative_code_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)) + ((dst_negative_scale_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)))) + ((((dst_negative_code_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)) * S ((dst_negative_code_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)) + ((dst_negative_scale_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum))) + (((dst_negative_code_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)) * S ((dst_negative_code_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)) + ((dst_negative_scale_concat_value_totalsum) + (dst_negative_scale_concat_value_totalsum)))))) /\ (((exists fs_u_dst_concat_value_totalsumpositive fs_v_dst_concat_value_totalsumpositive. ((((exists fs_h_dst_concat_value_totalsumpositive_body_start. fs_h_dst_concat_value_totalsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_value_totalsumpositive)) /\ exists fs_q_dst_concat_value_totalsumpositive_body_start. fs_u_dst_concat_value_totalsumpositive = fs_q_dst_concat_value_totalsumpositive_body_start * S ((S (0)) * fs_v_dst_concat_value_totalsumpositive) + (0))) /\ ((((exists fs_h_dst_concat_value_totalsumpositive_body_terminal. fs_h_dst_concat_value_totalsumpositive_body_terminal + S (dst_positive_sum_concat_value_totalsum) = S ((S (p+q)) * fs_v_dst_concat_value_totalsumpositive)) /\ exists fs_q_dst_concat_value_totalsumpositive_body_terminal. fs_u_dst_concat_value_totalsumpositive = fs_q_dst_concat_value_totalsumpositive_body_terminal * S ((S (p+q)) * fs_v_dst_concat_value_totalsumpositive) + (dst_positive_sum_concat_value_totalsum))) /\ forall fs_i_dst_concat_value_totalsumpositive_body_steps. (exists fs_lt_dst_concat_value_totalsumpositive_body_steps_bound. fs_lt_dst_concat_value_totalsumpositive_body_steps_bound + S fs_i_dst_concat_value_totalsumpositive_body_steps = p+q) -> exists fs_a_dst_concat_value_totalsumpositive_body_steps fs_r_dst_concat_value_totalsumpositive_body_steps fs_s_dst_concat_value_totalsumpositive_body_steps. ((((exists fs_h_dst_concat_value_totalsumpositive_body_steps_summand. fs_h_dst_concat_value_totalsumpositive_body_steps_summand + S (fs_a_dst_concat_value_totalsumpositive_body_steps) = S ((S (fs_i_dst_concat_value_totalsumpositive_body_steps)) * dst_positive_scale_concat_value_totalsum)) /\ exists fs_q_dst_concat_value_totalsumpositive_body_steps_summand. dst_positive_code_concat_value_totalsum = fs_q_dst_concat_value_totalsumpositive_body_steps_summand * S ((S (fs_i_dst_concat_value_totalsumpositive_body_steps)) * dst_positive_scale_concat_value_totalsum) + (fs_a_dst_concat_value_totalsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_value_totalsumpositive_body_steps_partial. fs_h_dst_concat_value_totalsumpositive_body_steps_partial + S (fs_r_dst_concat_value_totalsumpositive_body_steps) = S ((S (fs_i_dst_concat_value_totalsumpositive_body_steps)) * fs_v_dst_concat_value_totalsumpositive)) /\ exists fs_q_dst_concat_value_totalsumpositive_body_steps_partial. fs_u_dst_concat_value_totalsumpositive = fs_q_dst_concat_value_totalsumpositive_body_steps_partial * S ((S (fs_i_dst_concat_value_totalsumpositive_body_steps)) * fs_v_dst_concat_value_totalsumpositive) + (fs_r_dst_concat_value_totalsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_value_totalsumpositive_body_steps_successor. fs_h_dst_concat_value_totalsumpositive_body_steps_successor + S (fs_s_dst_concat_value_totalsumpositive_body_steps) = S ((S (S fs_i_dst_concat_value_totalsumpositive_body_steps)) * fs_v_dst_concat_value_totalsumpositive)) /\ exists fs_q_dst_concat_value_totalsumpositive_body_steps_successor. fs_u_dst_concat_value_totalsumpositive = fs_q_dst_concat_value_totalsumpositive_body_steps_successor * S ((S (S fs_i_dst_concat_value_totalsumpositive_body_steps)) * fs_v_dst_concat_value_totalsumpositive) + (fs_s_dst_concat_value_totalsumpositive_body_steps))) /\ fs_s_dst_concat_value_totalsumpositive_body_steps = fs_r_dst_concat_value_totalsumpositive_body_steps + fs_a_dst_concat_value_totalsumpositive_body_steps)))))) /\ (((exists fs_u_dst_concat_value_totalsumnegative fs_v_dst_concat_value_totalsumnegative. ((((exists fs_h_dst_concat_value_totalsumnegative_body_start. fs_h_dst_concat_value_totalsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_value_totalsumnegative)) /\ exists fs_q_dst_concat_value_totalsumnegative_body_start. fs_u_dst_concat_value_totalsumnegative = fs_q_dst_concat_value_totalsumnegative_body_start * S ((S (0)) * fs_v_dst_concat_value_totalsumnegative) + (0))) /\ ((((exists fs_h_dst_concat_value_totalsumnegative_body_terminal. fs_h_dst_concat_value_totalsumnegative_body_terminal + S (dst_negative_sum_concat_value_totalsum) = S ((S (p+q)) * fs_v_dst_concat_value_totalsumnegative)) /\ exists fs_q_dst_concat_value_totalsumnegative_body_terminal. fs_u_dst_concat_value_totalsumnegative = fs_q_dst_concat_value_totalsumnegative_body_terminal * S ((S (p+q)) * fs_v_dst_concat_value_totalsumnegative) + (dst_negative_sum_concat_value_totalsum))) /\ forall fs_i_dst_concat_value_totalsumnegative_body_steps. (exists fs_lt_dst_concat_value_totalsumnegative_body_steps_bound. fs_lt_dst_concat_value_totalsumnegative_body_steps_bound + S fs_i_dst_concat_value_totalsumnegative_body_steps = p+q) -> exists fs_a_dst_concat_value_totalsumnegative_body_steps fs_r_dst_concat_value_totalsumnegative_body_steps fs_s_dst_concat_value_totalsumnegative_body_steps. ((((exists fs_h_dst_concat_value_totalsumnegative_body_steps_summand. fs_h_dst_concat_value_totalsumnegative_body_steps_summand + S (fs_a_dst_concat_value_totalsumnegative_body_steps) = S ((S (fs_i_dst_concat_value_totalsumnegative_body_steps)) * dst_negative_scale_concat_value_totalsum)) /\ exists fs_q_dst_concat_value_totalsumnegative_body_steps_summand. dst_negative_code_concat_value_totalsum = fs_q_dst_concat_value_totalsumnegative_body_steps_summand * S ((S (fs_i_dst_concat_value_totalsumnegative_body_steps)) * dst_negative_scale_concat_value_totalsum) + (fs_a_dst_concat_value_totalsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_value_totalsumnegative_body_steps_partial. fs_h_dst_concat_value_totalsumnegative_body_steps_partial + S (fs_r_dst_concat_value_totalsumnegative_body_steps) = S ((S (fs_i_dst_concat_value_totalsumnegative_body_steps)) * fs_v_dst_concat_value_totalsumnegative)) /\ exists fs_q_dst_concat_value_totalsumnegative_body_steps_partial. fs_u_dst_concat_value_totalsumnegative = fs_q_dst_concat_value_totalsumnegative_body_steps_partial * S ((S (fs_i_dst_concat_value_totalsumnegative_body_steps)) * fs_v_dst_concat_value_totalsumnegative) + (fs_r_dst_concat_value_totalsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_value_totalsumnegative_body_steps_successor. fs_h_dst_concat_value_totalsumnegative_body_steps_successor + S (fs_s_dst_concat_value_totalsumnegative_body_steps) = S ((S (S fs_i_dst_concat_value_totalsumnegative_body_steps)) * fs_v_dst_concat_value_totalsumnegative)) /\ exists fs_q_dst_concat_value_totalsumnegative_body_steps_successor. fs_u_dst_concat_value_totalsumnegative = fs_q_dst_concat_value_totalsumnegative_body_steps_successor * S ((S (S fs_i_dst_concat_value_totalsumnegative_body_steps)) * fs_v_dst_concat_value_totalsumnegative) + (fs_s_dst_concat_value_totalsumnegative_body_steps))) /\ fs_s_dst_concat_value_totalsumnegative_body_steps = fs_r_dst_concat_value_totalsumnegative_body_steps + fs_a_dst_concat_value_totalsumnegative_body_steps)))))) /\ (exists ge_balance_positive_concat_value_totalsumresult ge_balance_negative_concat_value_totalsumresult. (((((c) = 2 * (ge_balance_positive_concat_value_totalsumresult) /\ (ge_balance_negative_concat_value_totalsumresult) = 0) \/ exists ge_signed_half_concat_value_totalsumresultdecode. (((c) = 2 * ge_signed_half_concat_value_totalsumresultdecode + 1 /\ (ge_balance_positive_concat_value_totalsumresult) = 0) /\ (ge_balance_negative_concat_value_totalsumresult) = S ge_signed_half_concat_value_totalsumresultdecode))) /\ ((dst_positive_sum_concat_value_totalsum) + ge_balance_negative_concat_value_totalsumresult = (dst_negative_sum_concat_value_totalsum) + ge_balance_positive_concat_value_totalsumresult))))))))))) -> (exists dsa_ap_concat_value_result dsa_an_concat_value_result dsa_bp_concat_value_result dsa_bn_concat_value_result dsa_cp_concat_value_result dsa_cn_concat_value_result. (((((a) = 2 * (dsa_ap_concat_value_result) /\ (dsa_an_concat_value_result) = 0) \/ exists ge_signed_half_concat_value_resultleft. (((a) = 2 * ge_signed_half_concat_value_resultleft + 1 /\ (dsa_ap_concat_value_result) = 0) /\ (dsa_an_concat_value_result) = S ge_signed_half_concat_value_resultleft))) /\ ((((((b) = 2 * (dsa_bp_concat_value_result) /\ (dsa_bn_concat_value_result) = 0) \/ exists ge_signed_half_concat_value_resultright. (((b) = 2 * ge_signed_half_concat_value_resultright + 1 /\ (dsa_bp_concat_value_result) = 0) /\ (dsa_bn_concat_value_result) = S ge_signed_half_concat_value_resultright))) /\ ((((((c) = 2 * (dsa_cp_concat_value_result) /\ (dsa_cn_concat_value_result) = 0) \/ exists ge_signed_half_concat_value_resultoutput. (((c) = 2 * ge_signed_half_concat_value_resultoutput + 1 /\ (dsa_cp_concat_value_result) = 0) /\ (dsa_cn_concat_value_result) = S ge_signed_half_concat_value_resultoutput))) /\ ((dsa_ap_concat_value_result + dsa_bp_concat_value_result) + dsa_cn_concat_value_result = (dsa_an_concat_value_result + dsa_bn_concat_value_result) + dsa_cp_concat_value_result)))))))