signed_slice_sum_concatenate

Exact expanded first-order arithmetic statement

forall q F o s p a b c. (exists srs_slice_concat_first. ((((exists dst_positive_code_concat_firstslicesource_table dst_positive_scale_concat_firstslicesource_table dst_negative_code_concat_firstslicesource_table dst_negative_scale_concat_firstslicesource_table. (((F) = (((((dst_positive_code_concat_firstslicesource_table) + (dst_positive_scale_concat_firstslicesource_table)) * S ((dst_positive_code_concat_firstslicesource_table) + (dst_positive_scale_concat_firstslicesource_table)) + ((dst_positive_scale_concat_firstslicesource_table) + (dst_positive_scale_concat_firstslicesource_table))) + (((dst_negative_code_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)) * S ((dst_negative_code_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)) + ((dst_negative_scale_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)))) * S ((((dst_positive_code_concat_firstslicesource_table) + (dst_positive_scale_concat_firstslicesource_table)) * S ((dst_positive_code_concat_firstslicesource_table) + (dst_positive_scale_concat_firstslicesource_table)) + ((dst_positive_scale_concat_firstslicesource_table) + (dst_positive_scale_concat_firstslicesource_table))) + (((dst_negative_code_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)) * S ((dst_negative_code_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)) + ((dst_negative_scale_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)))) + ((((dst_negative_code_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)) * S ((dst_negative_code_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)) + ((dst_negative_scale_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table))) + (((dst_negative_code_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)) * S ((dst_negative_code_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)) + ((dst_negative_scale_concat_firstslicesource_table) + (dst_negative_scale_concat_firstslicesource_table)))))) /\ (forall dst_index_concat_firstslicesource_table. (exists pvs_le_gap_concat_firstslicesource_tabledomain. pvs_le_gap_concat_firstslicesource_tabledomain + (dst_index_concat_firstslicesource_table) = (0)) -> exists dst_positive_concat_firstslicesource_table dst_negative_concat_firstslicesource_table dst_value_concat_firstslicesource_table. ((((exists ff_h_pvs_concat_firstslicesource_tableentrypositive. ff_h_pvs_concat_firstslicesource_tableentrypositive + S (dst_positive_concat_firstslicesource_table) = S ((S (dst_index_concat_firstslicesource_table)) * dst_positive_scale_concat_firstslicesource_table)) /\ exists ff_q_pvs_concat_firstslicesource_tableentrypositive. dst_positive_code_concat_firstslicesource_table = ff_q_pvs_concat_firstslicesource_tableentrypositive * S ((S (dst_index_concat_firstslicesource_table)) * dst_positive_scale_concat_firstslicesource_table) + (dst_positive_concat_firstslicesource_table))) /\ (((((exists ff_h_pvs_concat_firstslicesource_tableentrynegative. ff_h_pvs_concat_firstslicesource_tableentrynegative + S (dst_negative_concat_firstslicesource_table) = S ((S (dst_index_concat_firstslicesource_table)) * dst_negative_scale_concat_firstslicesource_table)) /\ exists ff_q_pvs_concat_firstslicesource_tableentrynegative. dst_negative_code_concat_firstslicesource_table = ff_q_pvs_concat_firstslicesource_tableentrynegative * S ((S (dst_index_concat_firstslicesource_table)) * dst_negative_scale_concat_firstslicesource_table) + (dst_negative_concat_firstslicesource_table))) /\ (exists ge_balance_positive_concat_firstslicesource_tableentryvalue ge_balance_negative_concat_firstslicesource_tableentryvalue. (((((dst_value_concat_firstslicesource_table) = 2 * (ge_balance_positive_concat_firstslicesource_tableentryvalue) /\ (ge_balance_negative_concat_firstslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_concat_firstslicesource_tableentryvaluedecode. (((dst_value_concat_firstslicesource_table) = 2 * ge_signed_half_concat_firstslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_firstslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_concat_firstslicesource_tableentryvalue) = S ge_signed_half_concat_firstslicesource_tableentryvaluedecode))) /\ ((dst_positive_concat_firstslicesource_table) + ge_balance_negative_concat_firstslicesource_tableentryvalue = (dst_negative_concat_firstslicesource_table) + ge_balance_positive_concat_firstslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_concat_firstsliceoutput_table dst_positive_scale_concat_firstsliceoutput_table dst_negative_code_concat_firstsliceoutput_table dst_negative_scale_concat_firstsliceoutput_table. (((srs_slice_concat_first) = (((((dst_positive_code_concat_firstsliceoutput_table) + (dst_positive_scale_concat_firstsliceoutput_table)) * S ((dst_positive_code_concat_firstsliceoutput_table) + (dst_positive_scale_concat_firstsliceoutput_table)) + ((dst_positive_scale_concat_firstsliceoutput_table) + (dst_positive_scale_concat_firstsliceoutput_table))) + (((dst_negative_code_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)) * S ((dst_negative_code_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)) + ((dst_negative_scale_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)))) * S ((((dst_positive_code_concat_firstsliceoutput_table) + (dst_positive_scale_concat_firstsliceoutput_table)) * S ((dst_positive_code_concat_firstsliceoutput_table) + (dst_positive_scale_concat_firstsliceoutput_table)) + ((dst_positive_scale_concat_firstsliceoutput_table) + (dst_positive_scale_concat_firstsliceoutput_table))) + (((dst_negative_code_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)) * S ((dst_negative_code_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)) + ((dst_negative_scale_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)))) + ((((dst_negative_code_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)) * S ((dst_negative_code_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)) + ((dst_negative_scale_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table))) + (((dst_negative_code_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)) * S ((dst_negative_code_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)) + ((dst_negative_scale_concat_firstsliceoutput_table) + (dst_negative_scale_concat_firstsliceoutput_table)))))) /\ (forall dst_index_concat_firstsliceoutput_table. (exists pvs_le_gap_concat_firstsliceoutput_tabledomain. pvs_le_gap_concat_firstsliceoutput_tabledomain + (dst_index_concat_firstsliceoutput_table) = (p)) -> exists dst_positive_concat_firstsliceoutput_table dst_negative_concat_firstsliceoutput_table dst_value_concat_firstsliceoutput_table. ((((exists ff_h_pvs_concat_firstsliceoutput_tableentrypositive. ff_h_pvs_concat_firstsliceoutput_tableentrypositive + S (dst_positive_concat_firstsliceoutput_table) = S ((S (dst_index_concat_firstsliceoutput_table)) * dst_positive_scale_concat_firstsliceoutput_table)) /\ exists ff_q_pvs_concat_firstsliceoutput_tableentrypositive. dst_positive_code_concat_firstsliceoutput_table = ff_q_pvs_concat_firstsliceoutput_tableentrypositive * S ((S (dst_index_concat_firstsliceoutput_table)) * dst_positive_scale_concat_firstsliceoutput_table) + (dst_positive_concat_firstsliceoutput_table))) /\ (((((exists ff_h_pvs_concat_firstsliceoutput_tableentrynegative. ff_h_pvs_concat_firstsliceoutput_tableentrynegative + S (dst_negative_concat_firstsliceoutput_table) = S ((S (dst_index_concat_firstsliceoutput_table)) * dst_negative_scale_concat_firstsliceoutput_table)) /\ exists ff_q_pvs_concat_firstsliceoutput_tableentrynegative. dst_negative_code_concat_firstsliceoutput_table = ff_q_pvs_concat_firstsliceoutput_tableentrynegative * S ((S (dst_index_concat_firstsliceoutput_table)) * dst_negative_scale_concat_firstsliceoutput_table) + (dst_negative_concat_firstsliceoutput_table))) /\ (exists ge_balance_positive_concat_firstsliceoutput_tableentryvalue ge_balance_negative_concat_firstsliceoutput_tableentryvalue. (((((dst_value_concat_firstsliceoutput_table) = 2 * (ge_balance_positive_concat_firstsliceoutput_tableentryvalue) /\ (ge_balance_negative_concat_firstsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_concat_firstsliceoutput_tableentryvaluedecode. (((dst_value_concat_firstsliceoutput_table) = 2 * ge_signed_half_concat_firstsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_firstsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_concat_firstsliceoutput_tableentryvalue) = S ge_signed_half_concat_firstsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_concat_firstsliceoutput_table) + ge_balance_negative_concat_firstsliceoutput_tableentryvalue = (dst_negative_concat_firstsliceoutput_table) + ge_balance_positive_concat_firstsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_concat_firstslice. (exists pvs_gap_concat_firstslicebound. pvs_gap_concat_firstslicebound + S (srs_index_concat_firstslice) = (p)) -> exists srs_value_concat_firstslice. (((exists dst_positive_code_concat_firstsliceentrysource dst_positive_scale_concat_firstsliceentrysource dst_negative_code_concat_firstsliceentrysource dst_negative_scale_concat_firstsliceentrysource dst_positive_concat_firstsliceentrysource dst_negative_concat_firstsliceentrysource. (((F) = (((((dst_positive_code_concat_firstsliceentrysource) + (dst_positive_scale_concat_firstsliceentrysource)) * S ((dst_positive_code_concat_firstsliceentrysource) + (dst_positive_scale_concat_firstsliceentrysource)) + ((dst_positive_scale_concat_firstsliceentrysource) + (dst_positive_scale_concat_firstsliceentrysource))) + (((dst_negative_code_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)) * S ((dst_negative_code_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)) + ((dst_negative_scale_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)))) * S ((((dst_positive_code_concat_firstsliceentrysource) + (dst_positive_scale_concat_firstsliceentrysource)) * S ((dst_positive_code_concat_firstsliceentrysource) + (dst_positive_scale_concat_firstsliceentrysource)) + ((dst_positive_scale_concat_firstsliceentrysource) + (dst_positive_scale_concat_firstsliceentrysource))) + (((dst_negative_code_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)) * S ((dst_negative_code_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)) + ((dst_negative_scale_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)))) + ((((dst_negative_code_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)) * S ((dst_negative_code_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)) + ((dst_negative_scale_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource))) + (((dst_negative_code_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)) * S ((dst_negative_code_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)) + ((dst_negative_scale_concat_firstsliceentrysource) + (dst_negative_scale_concat_firstsliceentrysource)))))) /\ (((((exists ff_h_pvs_concat_firstsliceentrysourcepositive. ff_h_pvs_concat_firstsliceentrysourcepositive + S (dst_positive_concat_firstsliceentrysource) = S ((S (((o) + ((s) * (srs_index_concat_firstslice))))) * dst_positive_scale_concat_firstsliceentrysource)) /\ exists ff_q_pvs_concat_firstsliceentrysourcepositive. dst_positive_code_concat_firstsliceentrysource = ff_q_pvs_concat_firstsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_concat_firstslice))))) * dst_positive_scale_concat_firstsliceentrysource) + (dst_positive_concat_firstsliceentrysource))) /\ (((((exists ff_h_pvs_concat_firstsliceentrysourcenegative. ff_h_pvs_concat_firstsliceentrysourcenegative + S (dst_negative_concat_firstsliceentrysource) = S ((S (((o) + ((s) * (srs_index_concat_firstslice))))) * dst_negative_scale_concat_firstsliceentrysource)) /\ exists ff_q_pvs_concat_firstsliceentrysourcenegative. dst_negative_code_concat_firstsliceentrysource = ff_q_pvs_concat_firstsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_concat_firstslice))))) * dst_negative_scale_concat_firstsliceentrysource) + (dst_negative_concat_firstsliceentrysource))) /\ (exists ge_balance_positive_concat_firstsliceentrysourcevalue ge_balance_negative_concat_firstsliceentrysourcevalue. (((((srs_value_concat_firstslice) = 2 * (ge_balance_positive_concat_firstsliceentrysourcevalue) /\ (ge_balance_negative_concat_firstsliceentrysourcevalue) = 0) \/ exists ge_signed_half_concat_firstsliceentrysourcevaluedecode. (((srs_value_concat_firstslice) = 2 * ge_signed_half_concat_firstsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_concat_firstsliceentrysourcevalue) = 0) /\ (ge_balance_negative_concat_firstsliceentrysourcevalue) = S ge_signed_half_concat_firstsliceentrysourcevaluedecode))) /\ ((dst_positive_concat_firstsliceentrysource) + ge_balance_negative_concat_firstsliceentrysourcevalue = (dst_negative_concat_firstsliceentrysource) + ge_balance_positive_concat_firstsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_concat_firstsliceentryoutput dst_positive_scale_concat_firstsliceentryoutput dst_negative_code_concat_firstsliceentryoutput dst_negative_scale_concat_firstsliceentryoutput dst_positive_concat_firstsliceentryoutput dst_negative_concat_firstsliceentryoutput. (((srs_slice_concat_first) = (((((dst_positive_code_concat_firstsliceentryoutput) + (dst_positive_scale_concat_firstsliceentryoutput)) * S ((dst_positive_code_concat_firstsliceentryoutput) + (dst_positive_scale_concat_firstsliceentryoutput)) + ((dst_positive_scale_concat_firstsliceentryoutput) + (dst_positive_scale_concat_firstsliceentryoutput))) + (((dst_negative_code_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)) * S ((dst_negative_code_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)) + ((dst_negative_scale_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)))) * S ((((dst_positive_code_concat_firstsliceentryoutput) + (dst_positive_scale_concat_firstsliceentryoutput)) * S ((dst_positive_code_concat_firstsliceentryoutput) + (dst_positive_scale_concat_firstsliceentryoutput)) + ((dst_positive_scale_concat_firstsliceentryoutput) + (dst_positive_scale_concat_firstsliceentryoutput))) + (((dst_negative_code_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)) * S ((dst_negative_code_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)) + ((dst_negative_scale_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)))) + ((((dst_negative_code_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)) * S ((dst_negative_code_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)) + ((dst_negative_scale_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput))) + (((dst_negative_code_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)) * S ((dst_negative_code_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)) + ((dst_negative_scale_concat_firstsliceentryoutput) + (dst_negative_scale_concat_firstsliceentryoutput)))))) /\ (((((exists ff_h_pvs_concat_firstsliceentryoutputpositive. ff_h_pvs_concat_firstsliceentryoutputpositive + S (dst_positive_concat_firstsliceentryoutput) = S ((S (srs_index_concat_firstslice)) * dst_positive_scale_concat_firstsliceentryoutput)) /\ exists ff_q_pvs_concat_firstsliceentryoutputpositive. dst_positive_code_concat_firstsliceentryoutput = ff_q_pvs_concat_firstsliceentryoutputpositive * S ((S (srs_index_concat_firstslice)) * dst_positive_scale_concat_firstsliceentryoutput) + (dst_positive_concat_firstsliceentryoutput))) /\ (((((exists ff_h_pvs_concat_firstsliceentryoutputnegative. ff_h_pvs_concat_firstsliceentryoutputnegative + S (dst_negative_concat_firstsliceentryoutput) = S ((S (srs_index_concat_firstslice)) * dst_negative_scale_concat_firstsliceentryoutput)) /\ exists ff_q_pvs_concat_firstsliceentryoutputnegative. dst_negative_code_concat_firstsliceentryoutput = ff_q_pvs_concat_firstsliceentryoutputnegative * S ((S (srs_index_concat_firstslice)) * dst_negative_scale_concat_firstsliceentryoutput) + (dst_negative_concat_firstsliceentryoutput))) /\ (exists ge_balance_positive_concat_firstsliceentryoutputvalue ge_balance_negative_concat_firstsliceentryoutputvalue. (((((srs_value_concat_firstslice) = 2 * (ge_balance_positive_concat_firstsliceentryoutputvalue) /\ (ge_balance_negative_concat_firstsliceentryoutputvalue) = 0) \/ exists ge_signed_half_concat_firstsliceentryoutputvaluedecode. (((srs_value_concat_firstslice) = 2 * ge_signed_half_concat_firstsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_concat_firstsliceentryoutputvalue) = 0) /\ (ge_balance_negative_concat_firstsliceentryoutputvalue) = S ge_signed_half_concat_firstsliceentryoutputvaluedecode))) /\ ((dst_positive_concat_firstsliceentryoutput) + ge_balance_negative_concat_firstsliceentryoutputvalue = (dst_negative_concat_firstsliceentryoutput) + ge_balance_positive_concat_firstsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_concat_firstsum dst_positive_scale_concat_firstsum dst_negative_code_concat_firstsum dst_negative_scale_concat_firstsum dst_positive_sum_concat_firstsum dst_negative_sum_concat_firstsum. (((srs_slice_concat_first) = (((((dst_positive_code_concat_firstsum) + (dst_positive_scale_concat_firstsum)) * S ((dst_positive_code_concat_firstsum) + (dst_positive_scale_concat_firstsum)) + ((dst_positive_scale_concat_firstsum) + (dst_positive_scale_concat_firstsum))) + (((dst_negative_code_concat_firstsum) + (dst_negative_scale_concat_firstsum)) * S ((dst_negative_code_concat_firstsum) + (dst_negative_scale_concat_firstsum)) + ((dst_negative_scale_concat_firstsum) + (dst_negative_scale_concat_firstsum)))) * S ((((dst_positive_code_concat_firstsum) + (dst_positive_scale_concat_firstsum)) * S ((dst_positive_code_concat_firstsum) + (dst_positive_scale_concat_firstsum)) + ((dst_positive_scale_concat_firstsum) + (dst_positive_scale_concat_firstsum))) + (((dst_negative_code_concat_firstsum) + (dst_negative_scale_concat_firstsum)) * S ((dst_negative_code_concat_firstsum) + (dst_negative_scale_concat_firstsum)) + ((dst_negative_scale_concat_firstsum) + (dst_negative_scale_concat_firstsum)))) + ((((dst_negative_code_concat_firstsum) + (dst_negative_scale_concat_firstsum)) * S ((dst_negative_code_concat_firstsum) + (dst_negative_scale_concat_firstsum)) + ((dst_negative_scale_concat_firstsum) + (dst_negative_scale_concat_firstsum))) + (((dst_negative_code_concat_firstsum) + (dst_negative_scale_concat_firstsum)) * S ((dst_negative_code_concat_firstsum) + (dst_negative_scale_concat_firstsum)) + ((dst_negative_scale_concat_firstsum) + (dst_negative_scale_concat_firstsum)))))) /\ (((exists fs_u_dst_concat_firstsumpositive fs_v_dst_concat_firstsumpositive. ((((exists fs_h_dst_concat_firstsumpositive_body_start. fs_h_dst_concat_firstsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_firstsumpositive)) /\ exists fs_q_dst_concat_firstsumpositive_body_start. fs_u_dst_concat_firstsumpositive = fs_q_dst_concat_firstsumpositive_body_start * S ((S (0)) * fs_v_dst_concat_firstsumpositive) + (0))) /\ ((((exists fs_h_dst_concat_firstsumpositive_body_terminal. fs_h_dst_concat_firstsumpositive_body_terminal + S (dst_positive_sum_concat_firstsum) = S ((S (p)) * fs_v_dst_concat_firstsumpositive)) /\ exists fs_q_dst_concat_firstsumpositive_body_terminal. fs_u_dst_concat_firstsumpositive = fs_q_dst_concat_firstsumpositive_body_terminal * S ((S (p)) * fs_v_dst_concat_firstsumpositive) + (dst_positive_sum_concat_firstsum))) /\ forall fs_i_dst_concat_firstsumpositive_body_steps. (exists fs_lt_dst_concat_firstsumpositive_body_steps_bound. fs_lt_dst_concat_firstsumpositive_body_steps_bound + S fs_i_dst_concat_firstsumpositive_body_steps = p) -> exists fs_a_dst_concat_firstsumpositive_body_steps fs_r_dst_concat_firstsumpositive_body_steps fs_s_dst_concat_firstsumpositive_body_steps. ((((exists fs_h_dst_concat_firstsumpositive_body_steps_summand. fs_h_dst_concat_firstsumpositive_body_steps_summand + S (fs_a_dst_concat_firstsumpositive_body_steps) = S ((S (fs_i_dst_concat_firstsumpositive_body_steps)) * dst_positive_scale_concat_firstsum)) /\ exists fs_q_dst_concat_firstsumpositive_body_steps_summand. dst_positive_code_concat_firstsum = fs_q_dst_concat_firstsumpositive_body_steps_summand * S ((S (fs_i_dst_concat_firstsumpositive_body_steps)) * dst_positive_scale_concat_firstsum) + (fs_a_dst_concat_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_firstsumpositive_body_steps_partial. fs_h_dst_concat_firstsumpositive_body_steps_partial + S (fs_r_dst_concat_firstsumpositive_body_steps) = S ((S (fs_i_dst_concat_firstsumpositive_body_steps)) * fs_v_dst_concat_firstsumpositive)) /\ exists fs_q_dst_concat_firstsumpositive_body_steps_partial. fs_u_dst_concat_firstsumpositive = fs_q_dst_concat_firstsumpositive_body_steps_partial * S ((S (fs_i_dst_concat_firstsumpositive_body_steps)) * fs_v_dst_concat_firstsumpositive) + (fs_r_dst_concat_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_firstsumpositive_body_steps_successor. fs_h_dst_concat_firstsumpositive_body_steps_successor + S (fs_s_dst_concat_firstsumpositive_body_steps) = S ((S (S fs_i_dst_concat_firstsumpositive_body_steps)) * fs_v_dst_concat_firstsumpositive)) /\ exists fs_q_dst_concat_firstsumpositive_body_steps_successor. fs_u_dst_concat_firstsumpositive = fs_q_dst_concat_firstsumpositive_body_steps_successor * S ((S (S fs_i_dst_concat_firstsumpositive_body_steps)) * fs_v_dst_concat_firstsumpositive) + (fs_s_dst_concat_firstsumpositive_body_steps))) /\ fs_s_dst_concat_firstsumpositive_body_steps = fs_r_dst_concat_firstsumpositive_body_steps + fs_a_dst_concat_firstsumpositive_body_steps)))))) /\ (((exists fs_u_dst_concat_firstsumnegative fs_v_dst_concat_firstsumnegative. ((((exists fs_h_dst_concat_firstsumnegative_body_start. fs_h_dst_concat_firstsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_firstsumnegative)) /\ exists fs_q_dst_concat_firstsumnegative_body_start. fs_u_dst_concat_firstsumnegative = fs_q_dst_concat_firstsumnegative_body_start * S ((S (0)) * fs_v_dst_concat_firstsumnegative) + (0))) /\ ((((exists fs_h_dst_concat_firstsumnegative_body_terminal. fs_h_dst_concat_firstsumnegative_body_terminal + S (dst_negative_sum_concat_firstsum) = S ((S (p)) * fs_v_dst_concat_firstsumnegative)) /\ exists fs_q_dst_concat_firstsumnegative_body_terminal. fs_u_dst_concat_firstsumnegative = fs_q_dst_concat_firstsumnegative_body_terminal * S ((S (p)) * fs_v_dst_concat_firstsumnegative) + (dst_negative_sum_concat_firstsum))) /\ forall fs_i_dst_concat_firstsumnegative_body_steps. (exists fs_lt_dst_concat_firstsumnegative_body_steps_bound. fs_lt_dst_concat_firstsumnegative_body_steps_bound + S fs_i_dst_concat_firstsumnegative_body_steps = p) -> exists fs_a_dst_concat_firstsumnegative_body_steps fs_r_dst_concat_firstsumnegative_body_steps fs_s_dst_concat_firstsumnegative_body_steps. ((((exists fs_h_dst_concat_firstsumnegative_body_steps_summand. fs_h_dst_concat_firstsumnegative_body_steps_summand + S (fs_a_dst_concat_firstsumnegative_body_steps) = S ((S (fs_i_dst_concat_firstsumnegative_body_steps)) * dst_negative_scale_concat_firstsum)) /\ exists fs_q_dst_concat_firstsumnegative_body_steps_summand. dst_negative_code_concat_firstsum = fs_q_dst_concat_firstsumnegative_body_steps_summand * S ((S (fs_i_dst_concat_firstsumnegative_body_steps)) * dst_negative_scale_concat_firstsum) + (fs_a_dst_concat_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_firstsumnegative_body_steps_partial. fs_h_dst_concat_firstsumnegative_body_steps_partial + S (fs_r_dst_concat_firstsumnegative_body_steps) = S ((S (fs_i_dst_concat_firstsumnegative_body_steps)) * fs_v_dst_concat_firstsumnegative)) /\ exists fs_q_dst_concat_firstsumnegative_body_steps_partial. fs_u_dst_concat_firstsumnegative = fs_q_dst_concat_firstsumnegative_body_steps_partial * S ((S (fs_i_dst_concat_firstsumnegative_body_steps)) * fs_v_dst_concat_firstsumnegative) + (fs_r_dst_concat_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_firstsumnegative_body_steps_successor. fs_h_dst_concat_firstsumnegative_body_steps_successor + S (fs_s_dst_concat_firstsumnegative_body_steps) = S ((S (S fs_i_dst_concat_firstsumnegative_body_steps)) * fs_v_dst_concat_firstsumnegative)) /\ exists fs_q_dst_concat_firstsumnegative_body_steps_successor. fs_u_dst_concat_firstsumnegative = fs_q_dst_concat_firstsumnegative_body_steps_successor * S ((S (S fs_i_dst_concat_firstsumnegative_body_steps)) * fs_v_dst_concat_firstsumnegative) + (fs_s_dst_concat_firstsumnegative_body_steps))) /\ fs_s_dst_concat_firstsumnegative_body_steps = fs_r_dst_concat_firstsumnegative_body_steps + fs_a_dst_concat_firstsumnegative_body_steps)))))) /\ (exists ge_balance_positive_concat_firstsumresult ge_balance_negative_concat_firstsumresult. (((((a) = 2 * (ge_balance_positive_concat_firstsumresult) /\ (ge_balance_negative_concat_firstsumresult) = 0) \/ exists ge_signed_half_concat_firstsumresultdecode. (((a) = 2 * ge_signed_half_concat_firstsumresultdecode + 1 /\ (ge_balance_positive_concat_firstsumresult) = 0) /\ (ge_balance_negative_concat_firstsumresult) = S ge_signed_half_concat_firstsumresultdecode))) /\ ((dst_positive_sum_concat_firstsum) + ge_balance_negative_concat_firstsumresult = (dst_negative_sum_concat_firstsum) + ge_balance_positive_concat_firstsumresult))))))))))) -> (exists srs_slice_concat_second. ((((exists dst_positive_code_concat_secondslicesource_table dst_positive_scale_concat_secondslicesource_table dst_negative_code_concat_secondslicesource_table dst_negative_scale_concat_secondslicesource_table. (((F) = (((((dst_positive_code_concat_secondslicesource_table) + (dst_positive_scale_concat_secondslicesource_table)) * S ((dst_positive_code_concat_secondslicesource_table) + (dst_positive_scale_concat_secondslicesource_table)) + ((dst_positive_scale_concat_secondslicesource_table) + (dst_positive_scale_concat_secondslicesource_table))) + (((dst_negative_code_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)) * S ((dst_negative_code_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)) + ((dst_negative_scale_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)))) * S ((((dst_positive_code_concat_secondslicesource_table) + (dst_positive_scale_concat_secondslicesource_table)) * S ((dst_positive_code_concat_secondslicesource_table) + (dst_positive_scale_concat_secondslicesource_table)) + ((dst_positive_scale_concat_secondslicesource_table) + (dst_positive_scale_concat_secondslicesource_table))) + (((dst_negative_code_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)) * S ((dst_negative_code_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)) + ((dst_negative_scale_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)))) + ((((dst_negative_code_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)) * S ((dst_negative_code_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)) + ((dst_negative_scale_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table))) + (((dst_negative_code_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)) * S ((dst_negative_code_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)) + ((dst_negative_scale_concat_secondslicesource_table) + (dst_negative_scale_concat_secondslicesource_table)))))) /\ (forall dst_index_concat_secondslicesource_table. (exists pvs_le_gap_concat_secondslicesource_tabledomain. pvs_le_gap_concat_secondslicesource_tabledomain + (dst_index_concat_secondslicesource_table) = (0)) -> exists dst_positive_concat_secondslicesource_table dst_negative_concat_secondslicesource_table dst_value_concat_secondslicesource_table. ((((exists ff_h_pvs_concat_secondslicesource_tableentrypositive. ff_h_pvs_concat_secondslicesource_tableentrypositive + S (dst_positive_concat_secondslicesource_table) = S ((S (dst_index_concat_secondslicesource_table)) * dst_positive_scale_concat_secondslicesource_table)) /\ exists ff_q_pvs_concat_secondslicesource_tableentrypositive. dst_positive_code_concat_secondslicesource_table = ff_q_pvs_concat_secondslicesource_tableentrypositive * S ((S (dst_index_concat_secondslicesource_table)) * dst_positive_scale_concat_secondslicesource_table) + (dst_positive_concat_secondslicesource_table))) /\ (((((exists ff_h_pvs_concat_secondslicesource_tableentrynegative. ff_h_pvs_concat_secondslicesource_tableentrynegative + S (dst_negative_concat_secondslicesource_table) = S ((S (dst_index_concat_secondslicesource_table)) * dst_negative_scale_concat_secondslicesource_table)) /\ exists ff_q_pvs_concat_secondslicesource_tableentrynegative. dst_negative_code_concat_secondslicesource_table = ff_q_pvs_concat_secondslicesource_tableentrynegative * S ((S (dst_index_concat_secondslicesource_table)) * dst_negative_scale_concat_secondslicesource_table) + (dst_negative_concat_secondslicesource_table))) /\ (exists ge_balance_positive_concat_secondslicesource_tableentryvalue ge_balance_negative_concat_secondslicesource_tableentryvalue. (((((dst_value_concat_secondslicesource_table) = 2 * (ge_balance_positive_concat_secondslicesource_tableentryvalue) /\ (ge_balance_negative_concat_secondslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_concat_secondslicesource_tableentryvaluedecode. (((dst_value_concat_secondslicesource_table) = 2 * ge_signed_half_concat_secondslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_secondslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_concat_secondslicesource_tableentryvalue) = S ge_signed_half_concat_secondslicesource_tableentryvaluedecode))) /\ ((dst_positive_concat_secondslicesource_table) + ge_balance_negative_concat_secondslicesource_tableentryvalue = (dst_negative_concat_secondslicesource_table) + ge_balance_positive_concat_secondslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_concat_secondsliceoutput_table dst_positive_scale_concat_secondsliceoutput_table dst_negative_code_concat_secondsliceoutput_table dst_negative_scale_concat_secondsliceoutput_table. (((srs_slice_concat_second) = (((((dst_positive_code_concat_secondsliceoutput_table) + (dst_positive_scale_concat_secondsliceoutput_table)) * S ((dst_positive_code_concat_secondsliceoutput_table) + (dst_positive_scale_concat_secondsliceoutput_table)) + ((dst_positive_scale_concat_secondsliceoutput_table) + (dst_positive_scale_concat_secondsliceoutput_table))) + (((dst_negative_code_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)) * S ((dst_negative_code_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)) + ((dst_negative_scale_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)))) * S ((((dst_positive_code_concat_secondsliceoutput_table) + (dst_positive_scale_concat_secondsliceoutput_table)) * S ((dst_positive_code_concat_secondsliceoutput_table) + (dst_positive_scale_concat_secondsliceoutput_table)) + ((dst_positive_scale_concat_secondsliceoutput_table) + (dst_positive_scale_concat_secondsliceoutput_table))) + (((dst_negative_code_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)) * S ((dst_negative_code_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)) + ((dst_negative_scale_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)))) + ((((dst_negative_code_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)) * S ((dst_negative_code_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)) + ((dst_negative_scale_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table))) + (((dst_negative_code_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)) * S ((dst_negative_code_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)) + ((dst_negative_scale_concat_secondsliceoutput_table) + (dst_negative_scale_concat_secondsliceoutput_table)))))) /\ (forall dst_index_concat_secondsliceoutput_table. (exists pvs_le_gap_concat_secondsliceoutput_tabledomain. pvs_le_gap_concat_secondsliceoutput_tabledomain + (dst_index_concat_secondsliceoutput_table) = (q)) -> exists dst_positive_concat_secondsliceoutput_table dst_negative_concat_secondsliceoutput_table dst_value_concat_secondsliceoutput_table. ((((exists ff_h_pvs_concat_secondsliceoutput_tableentrypositive. ff_h_pvs_concat_secondsliceoutput_tableentrypositive + S (dst_positive_concat_secondsliceoutput_table) = S ((S (dst_index_concat_secondsliceoutput_table)) * dst_positive_scale_concat_secondsliceoutput_table)) /\ exists ff_q_pvs_concat_secondsliceoutput_tableentrypositive. dst_positive_code_concat_secondsliceoutput_table = ff_q_pvs_concat_secondsliceoutput_tableentrypositive * S ((S (dst_index_concat_secondsliceoutput_table)) * dst_positive_scale_concat_secondsliceoutput_table) + (dst_positive_concat_secondsliceoutput_table))) /\ (((((exists ff_h_pvs_concat_secondsliceoutput_tableentrynegative. ff_h_pvs_concat_secondsliceoutput_tableentrynegative + S (dst_negative_concat_secondsliceoutput_table) = S ((S (dst_index_concat_secondsliceoutput_table)) * dst_negative_scale_concat_secondsliceoutput_table)) /\ exists ff_q_pvs_concat_secondsliceoutput_tableentrynegative. dst_negative_code_concat_secondsliceoutput_table = ff_q_pvs_concat_secondsliceoutput_tableentrynegative * S ((S (dst_index_concat_secondsliceoutput_table)) * dst_negative_scale_concat_secondsliceoutput_table) + (dst_negative_concat_secondsliceoutput_table))) /\ (exists ge_balance_positive_concat_secondsliceoutput_tableentryvalue ge_balance_negative_concat_secondsliceoutput_tableentryvalue. (((((dst_value_concat_secondsliceoutput_table) = 2 * (ge_balance_positive_concat_secondsliceoutput_tableentryvalue) /\ (ge_balance_negative_concat_secondsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_concat_secondsliceoutput_tableentryvaluedecode. (((dst_value_concat_secondsliceoutput_table) = 2 * ge_signed_half_concat_secondsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_secondsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_concat_secondsliceoutput_tableentryvalue) = S ge_signed_half_concat_secondsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_concat_secondsliceoutput_table) + ge_balance_negative_concat_secondsliceoutput_tableentryvalue = (dst_negative_concat_secondsliceoutput_table) + ge_balance_positive_concat_secondsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_concat_secondslice. (exists pvs_gap_concat_secondslicebound. pvs_gap_concat_secondslicebound + S (srs_index_concat_secondslice) = (q)) -> exists srs_value_concat_secondslice. (((exists dst_positive_code_concat_secondsliceentrysource dst_positive_scale_concat_secondsliceentrysource dst_negative_code_concat_secondsliceentrysource dst_negative_scale_concat_secondsliceentrysource dst_positive_concat_secondsliceentrysource dst_negative_concat_secondsliceentrysource. (((F) = (((((dst_positive_code_concat_secondsliceentrysource) + (dst_positive_scale_concat_secondsliceentrysource)) * S ((dst_positive_code_concat_secondsliceentrysource) + (dst_positive_scale_concat_secondsliceentrysource)) + ((dst_positive_scale_concat_secondsliceentrysource) + (dst_positive_scale_concat_secondsliceentrysource))) + (((dst_negative_code_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)) * S ((dst_negative_code_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)) + ((dst_negative_scale_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)))) * S ((((dst_positive_code_concat_secondsliceentrysource) + (dst_positive_scale_concat_secondsliceentrysource)) * S ((dst_positive_code_concat_secondsliceentrysource) + (dst_positive_scale_concat_secondsliceentrysource)) + ((dst_positive_scale_concat_secondsliceentrysource) + (dst_positive_scale_concat_secondsliceentrysource))) + (((dst_negative_code_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)) * S ((dst_negative_code_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)) + ((dst_negative_scale_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)))) + ((((dst_negative_code_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)) * S ((dst_negative_code_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)) + ((dst_negative_scale_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource))) + (((dst_negative_code_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)) * S ((dst_negative_code_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)) + ((dst_negative_scale_concat_secondsliceentrysource) + (dst_negative_scale_concat_secondsliceentrysource)))))) /\ (((((exists ff_h_pvs_concat_secondsliceentrysourcepositive. ff_h_pvs_concat_secondsliceentrysourcepositive + S (dst_positive_concat_secondsliceentrysource) = S ((S (((((o) + ((s) * (p)))) + ((s) * (srs_index_concat_secondslice))))) * dst_positive_scale_concat_secondsliceentrysource)) /\ exists ff_q_pvs_concat_secondsliceentrysourcepositive. dst_positive_code_concat_secondsliceentrysource = ff_q_pvs_concat_secondsliceentrysourcepositive * S ((S (((((o) + ((s) * (p)))) + ((s) * (srs_index_concat_secondslice))))) * dst_positive_scale_concat_secondsliceentrysource) + (dst_positive_concat_secondsliceentrysource))) /\ (((((exists ff_h_pvs_concat_secondsliceentrysourcenegative. ff_h_pvs_concat_secondsliceentrysourcenegative + S (dst_negative_concat_secondsliceentrysource) = S ((S (((((o) + ((s) * (p)))) + ((s) * (srs_index_concat_secondslice))))) * dst_negative_scale_concat_secondsliceentrysource)) /\ exists ff_q_pvs_concat_secondsliceentrysourcenegative. dst_negative_code_concat_secondsliceentrysource = ff_q_pvs_concat_secondsliceentrysourcenegative * S ((S (((((o) + ((s) * (p)))) + ((s) * (srs_index_concat_secondslice))))) * dst_negative_scale_concat_secondsliceentrysource) + (dst_negative_concat_secondsliceentrysource))) /\ (exists ge_balance_positive_concat_secondsliceentrysourcevalue ge_balance_negative_concat_secondsliceentrysourcevalue. (((((srs_value_concat_secondslice) = 2 * (ge_balance_positive_concat_secondsliceentrysourcevalue) /\ (ge_balance_negative_concat_secondsliceentrysourcevalue) = 0) \/ exists ge_signed_half_concat_secondsliceentrysourcevaluedecode. (((srs_value_concat_secondslice) = 2 * ge_signed_half_concat_secondsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_concat_secondsliceentrysourcevalue) = 0) /\ (ge_balance_negative_concat_secondsliceentrysourcevalue) = S ge_signed_half_concat_secondsliceentrysourcevaluedecode))) /\ ((dst_positive_concat_secondsliceentrysource) + ge_balance_negative_concat_secondsliceentrysourcevalue = (dst_negative_concat_secondsliceentrysource) + ge_balance_positive_concat_secondsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_concat_secondsliceentryoutput dst_positive_scale_concat_secondsliceentryoutput dst_negative_code_concat_secondsliceentryoutput dst_negative_scale_concat_secondsliceentryoutput dst_positive_concat_secondsliceentryoutput dst_negative_concat_secondsliceentryoutput. (((srs_slice_concat_second) = (((((dst_positive_code_concat_secondsliceentryoutput) + (dst_positive_scale_concat_secondsliceentryoutput)) * S ((dst_positive_code_concat_secondsliceentryoutput) + (dst_positive_scale_concat_secondsliceentryoutput)) + ((dst_positive_scale_concat_secondsliceentryoutput) + (dst_positive_scale_concat_secondsliceentryoutput))) + (((dst_negative_code_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)) * S ((dst_negative_code_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)) + ((dst_negative_scale_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)))) * S ((((dst_positive_code_concat_secondsliceentryoutput) + (dst_positive_scale_concat_secondsliceentryoutput)) * S ((dst_positive_code_concat_secondsliceentryoutput) + (dst_positive_scale_concat_secondsliceentryoutput)) + ((dst_positive_scale_concat_secondsliceentryoutput) + (dst_positive_scale_concat_secondsliceentryoutput))) + (((dst_negative_code_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)) * S ((dst_negative_code_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)) + ((dst_negative_scale_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)))) + ((((dst_negative_code_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)) * S ((dst_negative_code_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)) + ((dst_negative_scale_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput))) + (((dst_negative_code_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)) * S ((dst_negative_code_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)) + ((dst_negative_scale_concat_secondsliceentryoutput) + (dst_negative_scale_concat_secondsliceentryoutput)))))) /\ (((((exists ff_h_pvs_concat_secondsliceentryoutputpositive. ff_h_pvs_concat_secondsliceentryoutputpositive + S (dst_positive_concat_secondsliceentryoutput) = S ((S (srs_index_concat_secondslice)) * dst_positive_scale_concat_secondsliceentryoutput)) /\ exists ff_q_pvs_concat_secondsliceentryoutputpositive. dst_positive_code_concat_secondsliceentryoutput = ff_q_pvs_concat_secondsliceentryoutputpositive * S ((S (srs_index_concat_secondslice)) * dst_positive_scale_concat_secondsliceentryoutput) + (dst_positive_concat_secondsliceentryoutput))) /\ (((((exists ff_h_pvs_concat_secondsliceentryoutputnegative. ff_h_pvs_concat_secondsliceentryoutputnegative + S (dst_negative_concat_secondsliceentryoutput) = S ((S (srs_index_concat_secondslice)) * dst_negative_scale_concat_secondsliceentryoutput)) /\ exists ff_q_pvs_concat_secondsliceentryoutputnegative. dst_negative_code_concat_secondsliceentryoutput = ff_q_pvs_concat_secondsliceentryoutputnegative * S ((S (srs_index_concat_secondslice)) * dst_negative_scale_concat_secondsliceentryoutput) + (dst_negative_concat_secondsliceentryoutput))) /\ (exists ge_balance_positive_concat_secondsliceentryoutputvalue ge_balance_negative_concat_secondsliceentryoutputvalue. (((((srs_value_concat_secondslice) = 2 * (ge_balance_positive_concat_secondsliceentryoutputvalue) /\ (ge_balance_negative_concat_secondsliceentryoutputvalue) = 0) \/ exists ge_signed_half_concat_secondsliceentryoutputvaluedecode. (((srs_value_concat_secondslice) = 2 * ge_signed_half_concat_secondsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_concat_secondsliceentryoutputvalue) = 0) /\ (ge_balance_negative_concat_secondsliceentryoutputvalue) = S ge_signed_half_concat_secondsliceentryoutputvaluedecode))) /\ ((dst_positive_concat_secondsliceentryoutput) + ge_balance_negative_concat_secondsliceentryoutputvalue = (dst_negative_concat_secondsliceentryoutput) + ge_balance_positive_concat_secondsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_concat_secondsum dst_positive_scale_concat_secondsum dst_negative_code_concat_secondsum dst_negative_scale_concat_secondsum dst_positive_sum_concat_secondsum dst_negative_sum_concat_secondsum. (((srs_slice_concat_second) = (((((dst_positive_code_concat_secondsum) + (dst_positive_scale_concat_secondsum)) * S ((dst_positive_code_concat_secondsum) + (dst_positive_scale_concat_secondsum)) + ((dst_positive_scale_concat_secondsum) + (dst_positive_scale_concat_secondsum))) + (((dst_negative_code_concat_secondsum) + (dst_negative_scale_concat_secondsum)) * S ((dst_negative_code_concat_secondsum) + (dst_negative_scale_concat_secondsum)) + ((dst_negative_scale_concat_secondsum) + (dst_negative_scale_concat_secondsum)))) * S ((((dst_positive_code_concat_secondsum) + (dst_positive_scale_concat_secondsum)) * S ((dst_positive_code_concat_secondsum) + (dst_positive_scale_concat_secondsum)) + ((dst_positive_scale_concat_secondsum) + (dst_positive_scale_concat_secondsum))) + (((dst_negative_code_concat_secondsum) + (dst_negative_scale_concat_secondsum)) * S ((dst_negative_code_concat_secondsum) + (dst_negative_scale_concat_secondsum)) + ((dst_negative_scale_concat_secondsum) + (dst_negative_scale_concat_secondsum)))) + ((((dst_negative_code_concat_secondsum) + (dst_negative_scale_concat_secondsum)) * S ((dst_negative_code_concat_secondsum) + (dst_negative_scale_concat_secondsum)) + ((dst_negative_scale_concat_secondsum) + (dst_negative_scale_concat_secondsum))) + (((dst_negative_code_concat_secondsum) + (dst_negative_scale_concat_secondsum)) * S ((dst_negative_code_concat_secondsum) + (dst_negative_scale_concat_secondsum)) + ((dst_negative_scale_concat_secondsum) + (dst_negative_scale_concat_secondsum)))))) /\ (((exists fs_u_dst_concat_secondsumpositive fs_v_dst_concat_secondsumpositive. ((((exists fs_h_dst_concat_secondsumpositive_body_start. fs_h_dst_concat_secondsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_secondsumpositive)) /\ exists fs_q_dst_concat_secondsumpositive_body_start. fs_u_dst_concat_secondsumpositive = fs_q_dst_concat_secondsumpositive_body_start * S ((S (0)) * fs_v_dst_concat_secondsumpositive) + (0))) /\ ((((exists fs_h_dst_concat_secondsumpositive_body_terminal. fs_h_dst_concat_secondsumpositive_body_terminal + S (dst_positive_sum_concat_secondsum) = S ((S (q)) * fs_v_dst_concat_secondsumpositive)) /\ exists fs_q_dst_concat_secondsumpositive_body_terminal. fs_u_dst_concat_secondsumpositive = fs_q_dst_concat_secondsumpositive_body_terminal * S ((S (q)) * fs_v_dst_concat_secondsumpositive) + (dst_positive_sum_concat_secondsum))) /\ forall fs_i_dst_concat_secondsumpositive_body_steps. (exists fs_lt_dst_concat_secondsumpositive_body_steps_bound. fs_lt_dst_concat_secondsumpositive_body_steps_bound + S fs_i_dst_concat_secondsumpositive_body_steps = q) -> exists fs_a_dst_concat_secondsumpositive_body_steps fs_r_dst_concat_secondsumpositive_body_steps fs_s_dst_concat_secondsumpositive_body_steps. ((((exists fs_h_dst_concat_secondsumpositive_body_steps_summand. fs_h_dst_concat_secondsumpositive_body_steps_summand + S (fs_a_dst_concat_secondsumpositive_body_steps) = S ((S (fs_i_dst_concat_secondsumpositive_body_steps)) * dst_positive_scale_concat_secondsum)) /\ exists fs_q_dst_concat_secondsumpositive_body_steps_summand. dst_positive_code_concat_secondsum = fs_q_dst_concat_secondsumpositive_body_steps_summand * S ((S (fs_i_dst_concat_secondsumpositive_body_steps)) * dst_positive_scale_concat_secondsum) + (fs_a_dst_concat_secondsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_secondsumpositive_body_steps_partial. fs_h_dst_concat_secondsumpositive_body_steps_partial + S (fs_r_dst_concat_secondsumpositive_body_steps) = S ((S (fs_i_dst_concat_secondsumpositive_body_steps)) * fs_v_dst_concat_secondsumpositive)) /\ exists fs_q_dst_concat_secondsumpositive_body_steps_partial. fs_u_dst_concat_secondsumpositive = fs_q_dst_concat_secondsumpositive_body_steps_partial * S ((S (fs_i_dst_concat_secondsumpositive_body_steps)) * fs_v_dst_concat_secondsumpositive) + (fs_r_dst_concat_secondsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_secondsumpositive_body_steps_successor. fs_h_dst_concat_secondsumpositive_body_steps_successor + S (fs_s_dst_concat_secondsumpositive_body_steps) = S ((S (S fs_i_dst_concat_secondsumpositive_body_steps)) * fs_v_dst_concat_secondsumpositive)) /\ exists fs_q_dst_concat_secondsumpositive_body_steps_successor. fs_u_dst_concat_secondsumpositive = fs_q_dst_concat_secondsumpositive_body_steps_successor * S ((S (S fs_i_dst_concat_secondsumpositive_body_steps)) * fs_v_dst_concat_secondsumpositive) + (fs_s_dst_concat_secondsumpositive_body_steps))) /\ fs_s_dst_concat_secondsumpositive_body_steps = fs_r_dst_concat_secondsumpositive_body_steps + fs_a_dst_concat_secondsumpositive_body_steps)))))) /\ (((exists fs_u_dst_concat_secondsumnegative fs_v_dst_concat_secondsumnegative. ((((exists fs_h_dst_concat_secondsumnegative_body_start. fs_h_dst_concat_secondsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_secondsumnegative)) /\ exists fs_q_dst_concat_secondsumnegative_body_start. fs_u_dst_concat_secondsumnegative = fs_q_dst_concat_secondsumnegative_body_start * S ((S (0)) * fs_v_dst_concat_secondsumnegative) + (0))) /\ ((((exists fs_h_dst_concat_secondsumnegative_body_terminal. fs_h_dst_concat_secondsumnegative_body_terminal + S (dst_negative_sum_concat_secondsum) = S ((S (q)) * fs_v_dst_concat_secondsumnegative)) /\ exists fs_q_dst_concat_secondsumnegative_body_terminal. fs_u_dst_concat_secondsumnegative = fs_q_dst_concat_secondsumnegative_body_terminal * S ((S (q)) * fs_v_dst_concat_secondsumnegative) + (dst_negative_sum_concat_secondsum))) /\ forall fs_i_dst_concat_secondsumnegative_body_steps. (exists fs_lt_dst_concat_secondsumnegative_body_steps_bound. fs_lt_dst_concat_secondsumnegative_body_steps_bound + S fs_i_dst_concat_secondsumnegative_body_steps = q) -> exists fs_a_dst_concat_secondsumnegative_body_steps fs_r_dst_concat_secondsumnegative_body_steps fs_s_dst_concat_secondsumnegative_body_steps. ((((exists fs_h_dst_concat_secondsumnegative_body_steps_summand. fs_h_dst_concat_secondsumnegative_body_steps_summand + S (fs_a_dst_concat_secondsumnegative_body_steps) = S ((S (fs_i_dst_concat_secondsumnegative_body_steps)) * dst_negative_scale_concat_secondsum)) /\ exists fs_q_dst_concat_secondsumnegative_body_steps_summand. dst_negative_code_concat_secondsum = fs_q_dst_concat_secondsumnegative_body_steps_summand * S ((S (fs_i_dst_concat_secondsumnegative_body_steps)) * dst_negative_scale_concat_secondsum) + (fs_a_dst_concat_secondsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_secondsumnegative_body_steps_partial. fs_h_dst_concat_secondsumnegative_body_steps_partial + S (fs_r_dst_concat_secondsumnegative_body_steps) = S ((S (fs_i_dst_concat_secondsumnegative_body_steps)) * fs_v_dst_concat_secondsumnegative)) /\ exists fs_q_dst_concat_secondsumnegative_body_steps_partial. fs_u_dst_concat_secondsumnegative = fs_q_dst_concat_secondsumnegative_body_steps_partial * S ((S (fs_i_dst_concat_secondsumnegative_body_steps)) * fs_v_dst_concat_secondsumnegative) + (fs_r_dst_concat_secondsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_secondsumnegative_body_steps_successor. fs_h_dst_concat_secondsumnegative_body_steps_successor + S (fs_s_dst_concat_secondsumnegative_body_steps) = S ((S (S fs_i_dst_concat_secondsumnegative_body_steps)) * fs_v_dst_concat_secondsumnegative)) /\ exists fs_q_dst_concat_secondsumnegative_body_steps_successor. fs_u_dst_concat_secondsumnegative = fs_q_dst_concat_secondsumnegative_body_steps_successor * S ((S (S fs_i_dst_concat_secondsumnegative_body_steps)) * fs_v_dst_concat_secondsumnegative) + (fs_s_dst_concat_secondsumnegative_body_steps))) /\ fs_s_dst_concat_secondsumnegative_body_steps = fs_r_dst_concat_secondsumnegative_body_steps + fs_a_dst_concat_secondsumnegative_body_steps)))))) /\ (exists ge_balance_positive_concat_secondsumresult ge_balance_negative_concat_secondsumresult. (((((b) = 2 * (ge_balance_positive_concat_secondsumresult) /\ (ge_balance_negative_concat_secondsumresult) = 0) \/ exists ge_signed_half_concat_secondsumresultdecode. (((b) = 2 * ge_signed_half_concat_secondsumresultdecode + 1 /\ (ge_balance_positive_concat_secondsumresult) = 0) /\ (ge_balance_negative_concat_secondsumresult) = S ge_signed_half_concat_secondsumresultdecode))) /\ ((dst_positive_sum_concat_secondsum) + ge_balance_negative_concat_secondsumresult = (dst_negative_sum_concat_secondsum) + ge_balance_positive_concat_secondsumresult))))))))))) -> (exists dsa_ap_concat_add dsa_an_concat_add dsa_bp_concat_add dsa_bn_concat_add dsa_cp_concat_add dsa_cn_concat_add. (((((a) = 2 * (dsa_ap_concat_add) /\ (dsa_an_concat_add) = 0) \/ exists ge_signed_half_concat_addleft. (((a) = 2 * ge_signed_half_concat_addleft + 1 /\ (dsa_ap_concat_add) = 0) /\ (dsa_an_concat_add) = S ge_signed_half_concat_addleft))) /\ ((((((b) = 2 * (dsa_bp_concat_add) /\ (dsa_bn_concat_add) = 0) \/ exists ge_signed_half_concat_addright. (((b) = 2 * ge_signed_half_concat_addright + 1 /\ (dsa_bp_concat_add) = 0) /\ (dsa_bn_concat_add) = S ge_signed_half_concat_addright))) /\ ((((((c) = 2 * (dsa_cp_concat_add) /\ (dsa_cn_concat_add) = 0) \/ exists ge_signed_half_concat_addoutput. (((c) = 2 * ge_signed_half_concat_addoutput + 1 /\ (dsa_cp_concat_add) = 0) /\ (dsa_cn_concat_add) = S ge_signed_half_concat_addoutput))) /\ ((dsa_ap_concat_add + dsa_bp_concat_add) + dsa_cn_concat_add = (dsa_an_concat_add + dsa_bn_concat_add) + dsa_cp_concat_add))))))) -> (exists srs_slice_concat_result. ((((exists dst_positive_code_concat_resultslicesource_table dst_positive_scale_concat_resultslicesource_table dst_negative_code_concat_resultslicesource_table dst_negative_scale_concat_resultslicesource_table. (((F) = (((((dst_positive_code_concat_resultslicesource_table) + (dst_positive_scale_concat_resultslicesource_table)) * S ((dst_positive_code_concat_resultslicesource_table) + (dst_positive_scale_concat_resultslicesource_table)) + ((dst_positive_scale_concat_resultslicesource_table) + (dst_positive_scale_concat_resultslicesource_table))) + (((dst_negative_code_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)) * S ((dst_negative_code_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)) + ((dst_negative_scale_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)))) * S ((((dst_positive_code_concat_resultslicesource_table) + (dst_positive_scale_concat_resultslicesource_table)) * S ((dst_positive_code_concat_resultslicesource_table) + (dst_positive_scale_concat_resultslicesource_table)) + ((dst_positive_scale_concat_resultslicesource_table) + (dst_positive_scale_concat_resultslicesource_table))) + (((dst_negative_code_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)) * S ((dst_negative_code_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)) + ((dst_negative_scale_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)))) + ((((dst_negative_code_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)) * S ((dst_negative_code_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)) + ((dst_negative_scale_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table))) + (((dst_negative_code_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)) * S ((dst_negative_code_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)) + ((dst_negative_scale_concat_resultslicesource_table) + (dst_negative_scale_concat_resultslicesource_table)))))) /\ (forall dst_index_concat_resultslicesource_table. (exists pvs_le_gap_concat_resultslicesource_tabledomain. pvs_le_gap_concat_resultslicesource_tabledomain + (dst_index_concat_resultslicesource_table) = (0)) -> exists dst_positive_concat_resultslicesource_table dst_negative_concat_resultslicesource_table dst_value_concat_resultslicesource_table. ((((exists ff_h_pvs_concat_resultslicesource_tableentrypositive. ff_h_pvs_concat_resultslicesource_tableentrypositive + S (dst_positive_concat_resultslicesource_table) = S ((S (dst_index_concat_resultslicesource_table)) * dst_positive_scale_concat_resultslicesource_table)) /\ exists ff_q_pvs_concat_resultslicesource_tableentrypositive. dst_positive_code_concat_resultslicesource_table = ff_q_pvs_concat_resultslicesource_tableentrypositive * S ((S (dst_index_concat_resultslicesource_table)) * dst_positive_scale_concat_resultslicesource_table) + (dst_positive_concat_resultslicesource_table))) /\ (((((exists ff_h_pvs_concat_resultslicesource_tableentrynegative. ff_h_pvs_concat_resultslicesource_tableentrynegative + S (dst_negative_concat_resultslicesource_table) = S ((S (dst_index_concat_resultslicesource_table)) * dst_negative_scale_concat_resultslicesource_table)) /\ exists ff_q_pvs_concat_resultslicesource_tableentrynegative. dst_negative_code_concat_resultslicesource_table = ff_q_pvs_concat_resultslicesource_tableentrynegative * S ((S (dst_index_concat_resultslicesource_table)) * dst_negative_scale_concat_resultslicesource_table) + (dst_negative_concat_resultslicesource_table))) /\ (exists ge_balance_positive_concat_resultslicesource_tableentryvalue ge_balance_negative_concat_resultslicesource_tableentryvalue. (((((dst_value_concat_resultslicesource_table) = 2 * (ge_balance_positive_concat_resultslicesource_tableentryvalue) /\ (ge_balance_negative_concat_resultslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_concat_resultslicesource_tableentryvaluedecode. (((dst_value_concat_resultslicesource_table) = 2 * ge_signed_half_concat_resultslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_resultslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_concat_resultslicesource_tableentryvalue) = S ge_signed_half_concat_resultslicesource_tableentryvaluedecode))) /\ ((dst_positive_concat_resultslicesource_table) + ge_balance_negative_concat_resultslicesource_tableentryvalue = (dst_negative_concat_resultslicesource_table) + ge_balance_positive_concat_resultslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_concat_resultsliceoutput_table dst_positive_scale_concat_resultsliceoutput_table dst_negative_code_concat_resultsliceoutput_table dst_negative_scale_concat_resultsliceoutput_table. (((srs_slice_concat_result) = (((((dst_positive_code_concat_resultsliceoutput_table) + (dst_positive_scale_concat_resultsliceoutput_table)) * S ((dst_positive_code_concat_resultsliceoutput_table) + (dst_positive_scale_concat_resultsliceoutput_table)) + ((dst_positive_scale_concat_resultsliceoutput_table) + (dst_positive_scale_concat_resultsliceoutput_table))) + (((dst_negative_code_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)) * S ((dst_negative_code_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)) + ((dst_negative_scale_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)))) * S ((((dst_positive_code_concat_resultsliceoutput_table) + (dst_positive_scale_concat_resultsliceoutput_table)) * S ((dst_positive_code_concat_resultsliceoutput_table) + (dst_positive_scale_concat_resultsliceoutput_table)) + ((dst_positive_scale_concat_resultsliceoutput_table) + (dst_positive_scale_concat_resultsliceoutput_table))) + (((dst_negative_code_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)) * S ((dst_negative_code_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)) + ((dst_negative_scale_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)))) + ((((dst_negative_code_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)) * S ((dst_negative_code_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)) + ((dst_negative_scale_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table))) + (((dst_negative_code_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)) * S ((dst_negative_code_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)) + ((dst_negative_scale_concat_resultsliceoutput_table) + (dst_negative_scale_concat_resultsliceoutput_table)))))) /\ (forall dst_index_concat_resultsliceoutput_table. (exists pvs_le_gap_concat_resultsliceoutput_tabledomain. pvs_le_gap_concat_resultsliceoutput_tabledomain + (dst_index_concat_resultsliceoutput_table) = (p+q)) -> exists dst_positive_concat_resultsliceoutput_table dst_negative_concat_resultsliceoutput_table dst_value_concat_resultsliceoutput_table. ((((exists ff_h_pvs_concat_resultsliceoutput_tableentrypositive. ff_h_pvs_concat_resultsliceoutput_tableentrypositive + S (dst_positive_concat_resultsliceoutput_table) = S ((S (dst_index_concat_resultsliceoutput_table)) * dst_positive_scale_concat_resultsliceoutput_table)) /\ exists ff_q_pvs_concat_resultsliceoutput_tableentrypositive. dst_positive_code_concat_resultsliceoutput_table = ff_q_pvs_concat_resultsliceoutput_tableentrypositive * S ((S (dst_index_concat_resultsliceoutput_table)) * dst_positive_scale_concat_resultsliceoutput_table) + (dst_positive_concat_resultsliceoutput_table))) /\ (((((exists ff_h_pvs_concat_resultsliceoutput_tableentrynegative. ff_h_pvs_concat_resultsliceoutput_tableentrynegative + S (dst_negative_concat_resultsliceoutput_table) = S ((S (dst_index_concat_resultsliceoutput_table)) * dst_negative_scale_concat_resultsliceoutput_table)) /\ exists ff_q_pvs_concat_resultsliceoutput_tableentrynegative. dst_negative_code_concat_resultsliceoutput_table = ff_q_pvs_concat_resultsliceoutput_tableentrynegative * S ((S (dst_index_concat_resultsliceoutput_table)) * dst_negative_scale_concat_resultsliceoutput_table) + (dst_negative_concat_resultsliceoutput_table))) /\ (exists ge_balance_positive_concat_resultsliceoutput_tableentryvalue ge_balance_negative_concat_resultsliceoutput_tableentryvalue. (((((dst_value_concat_resultsliceoutput_table) = 2 * (ge_balance_positive_concat_resultsliceoutput_tableentryvalue) /\ (ge_balance_negative_concat_resultsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_concat_resultsliceoutput_tableentryvaluedecode. (((dst_value_concat_resultsliceoutput_table) = 2 * ge_signed_half_concat_resultsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_concat_resultsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_concat_resultsliceoutput_tableentryvalue) = S ge_signed_half_concat_resultsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_concat_resultsliceoutput_table) + ge_balance_negative_concat_resultsliceoutput_tableentryvalue = (dst_negative_concat_resultsliceoutput_table) + ge_balance_positive_concat_resultsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_concat_resultslice. (exists pvs_gap_concat_resultslicebound. pvs_gap_concat_resultslicebound + S (srs_index_concat_resultslice) = (p+q)) -> exists srs_value_concat_resultslice. (((exists dst_positive_code_concat_resultsliceentrysource dst_positive_scale_concat_resultsliceentrysource dst_negative_code_concat_resultsliceentrysource dst_negative_scale_concat_resultsliceentrysource dst_positive_concat_resultsliceentrysource dst_negative_concat_resultsliceentrysource. (((F) = (((((dst_positive_code_concat_resultsliceentrysource) + (dst_positive_scale_concat_resultsliceentrysource)) * S ((dst_positive_code_concat_resultsliceentrysource) + (dst_positive_scale_concat_resultsliceentrysource)) + ((dst_positive_scale_concat_resultsliceentrysource) + (dst_positive_scale_concat_resultsliceentrysource))) + (((dst_negative_code_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)) * S ((dst_negative_code_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)) + ((dst_negative_scale_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)))) * S ((((dst_positive_code_concat_resultsliceentrysource) + (dst_positive_scale_concat_resultsliceentrysource)) * S ((dst_positive_code_concat_resultsliceentrysource) + (dst_positive_scale_concat_resultsliceentrysource)) + ((dst_positive_scale_concat_resultsliceentrysource) + (dst_positive_scale_concat_resultsliceentrysource))) + (((dst_negative_code_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)) * S ((dst_negative_code_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)) + ((dst_negative_scale_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)))) + ((((dst_negative_code_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)) * S ((dst_negative_code_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)) + ((dst_negative_scale_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource))) + (((dst_negative_code_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)) * S ((dst_negative_code_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)) + ((dst_negative_scale_concat_resultsliceentrysource) + (dst_negative_scale_concat_resultsliceentrysource)))))) /\ (((((exists ff_h_pvs_concat_resultsliceentrysourcepositive. ff_h_pvs_concat_resultsliceentrysourcepositive + S (dst_positive_concat_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_concat_resultslice))))) * dst_positive_scale_concat_resultsliceentrysource)) /\ exists ff_q_pvs_concat_resultsliceentrysourcepositive. dst_positive_code_concat_resultsliceentrysource = ff_q_pvs_concat_resultsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_concat_resultslice))))) * dst_positive_scale_concat_resultsliceentrysource) + (dst_positive_concat_resultsliceentrysource))) /\ (((((exists ff_h_pvs_concat_resultsliceentrysourcenegative. ff_h_pvs_concat_resultsliceentrysourcenegative + S (dst_negative_concat_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_concat_resultslice))))) * dst_negative_scale_concat_resultsliceentrysource)) /\ exists ff_q_pvs_concat_resultsliceentrysourcenegative. dst_negative_code_concat_resultsliceentrysource = ff_q_pvs_concat_resultsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_concat_resultslice))))) * dst_negative_scale_concat_resultsliceentrysource) + (dst_negative_concat_resultsliceentrysource))) /\ (exists ge_balance_positive_concat_resultsliceentrysourcevalue ge_balance_negative_concat_resultsliceentrysourcevalue. (((((srs_value_concat_resultslice) = 2 * (ge_balance_positive_concat_resultsliceentrysourcevalue) /\ (ge_balance_negative_concat_resultsliceentrysourcevalue) = 0) \/ exists ge_signed_half_concat_resultsliceentrysourcevaluedecode. (((srs_value_concat_resultslice) = 2 * ge_signed_half_concat_resultsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_concat_resultsliceentrysourcevalue) = 0) /\ (ge_balance_negative_concat_resultsliceentrysourcevalue) = S ge_signed_half_concat_resultsliceentrysourcevaluedecode))) /\ ((dst_positive_concat_resultsliceentrysource) + ge_balance_negative_concat_resultsliceentrysourcevalue = (dst_negative_concat_resultsliceentrysource) + ge_balance_positive_concat_resultsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_concat_resultsliceentryoutput dst_positive_scale_concat_resultsliceentryoutput dst_negative_code_concat_resultsliceentryoutput dst_negative_scale_concat_resultsliceentryoutput dst_positive_concat_resultsliceentryoutput dst_negative_concat_resultsliceentryoutput. (((srs_slice_concat_result) = (((((dst_positive_code_concat_resultsliceentryoutput) + (dst_positive_scale_concat_resultsliceentryoutput)) * S ((dst_positive_code_concat_resultsliceentryoutput) + (dst_positive_scale_concat_resultsliceentryoutput)) + ((dst_positive_scale_concat_resultsliceentryoutput) + (dst_positive_scale_concat_resultsliceentryoutput))) + (((dst_negative_code_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)) * S ((dst_negative_code_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)) + ((dst_negative_scale_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)))) * S ((((dst_positive_code_concat_resultsliceentryoutput) + (dst_positive_scale_concat_resultsliceentryoutput)) * S ((dst_positive_code_concat_resultsliceentryoutput) + (dst_positive_scale_concat_resultsliceentryoutput)) + ((dst_positive_scale_concat_resultsliceentryoutput) + (dst_positive_scale_concat_resultsliceentryoutput))) + (((dst_negative_code_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)) * S ((dst_negative_code_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)) + ((dst_negative_scale_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)))) + ((((dst_negative_code_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)) * S ((dst_negative_code_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)) + ((dst_negative_scale_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput))) + (((dst_negative_code_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)) * S ((dst_negative_code_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)) + ((dst_negative_scale_concat_resultsliceentryoutput) + (dst_negative_scale_concat_resultsliceentryoutput)))))) /\ (((((exists ff_h_pvs_concat_resultsliceentryoutputpositive. ff_h_pvs_concat_resultsliceentryoutputpositive + S (dst_positive_concat_resultsliceentryoutput) = S ((S (srs_index_concat_resultslice)) * dst_positive_scale_concat_resultsliceentryoutput)) /\ exists ff_q_pvs_concat_resultsliceentryoutputpositive. dst_positive_code_concat_resultsliceentryoutput = ff_q_pvs_concat_resultsliceentryoutputpositive * S ((S (srs_index_concat_resultslice)) * dst_positive_scale_concat_resultsliceentryoutput) + (dst_positive_concat_resultsliceentryoutput))) /\ (((((exists ff_h_pvs_concat_resultsliceentryoutputnegative. ff_h_pvs_concat_resultsliceentryoutputnegative + S (dst_negative_concat_resultsliceentryoutput) = S ((S (srs_index_concat_resultslice)) * dst_negative_scale_concat_resultsliceentryoutput)) /\ exists ff_q_pvs_concat_resultsliceentryoutputnegative. dst_negative_code_concat_resultsliceentryoutput = ff_q_pvs_concat_resultsliceentryoutputnegative * S ((S (srs_index_concat_resultslice)) * dst_negative_scale_concat_resultsliceentryoutput) + (dst_negative_concat_resultsliceentryoutput))) /\ (exists ge_balance_positive_concat_resultsliceentryoutputvalue ge_balance_negative_concat_resultsliceentryoutputvalue. (((((srs_value_concat_resultslice) = 2 * (ge_balance_positive_concat_resultsliceentryoutputvalue) /\ (ge_balance_negative_concat_resultsliceentryoutputvalue) = 0) \/ exists ge_signed_half_concat_resultsliceentryoutputvaluedecode. (((srs_value_concat_resultslice) = 2 * ge_signed_half_concat_resultsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_concat_resultsliceentryoutputvalue) = 0) /\ (ge_balance_negative_concat_resultsliceentryoutputvalue) = S ge_signed_half_concat_resultsliceentryoutputvaluedecode))) /\ ((dst_positive_concat_resultsliceentryoutput) + ge_balance_negative_concat_resultsliceentryoutputvalue = (dst_negative_concat_resultsliceentryoutput) + ge_balance_positive_concat_resultsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_concat_resultsum dst_positive_scale_concat_resultsum dst_negative_code_concat_resultsum dst_negative_scale_concat_resultsum dst_positive_sum_concat_resultsum dst_negative_sum_concat_resultsum. (((srs_slice_concat_result) = (((((dst_positive_code_concat_resultsum) + (dst_positive_scale_concat_resultsum)) * S ((dst_positive_code_concat_resultsum) + (dst_positive_scale_concat_resultsum)) + ((dst_positive_scale_concat_resultsum) + (dst_positive_scale_concat_resultsum))) + (((dst_negative_code_concat_resultsum) + (dst_negative_scale_concat_resultsum)) * S ((dst_negative_code_concat_resultsum) + (dst_negative_scale_concat_resultsum)) + ((dst_negative_scale_concat_resultsum) + (dst_negative_scale_concat_resultsum)))) * S ((((dst_positive_code_concat_resultsum) + (dst_positive_scale_concat_resultsum)) * S ((dst_positive_code_concat_resultsum) + (dst_positive_scale_concat_resultsum)) + ((dst_positive_scale_concat_resultsum) + (dst_positive_scale_concat_resultsum))) + (((dst_negative_code_concat_resultsum) + (dst_negative_scale_concat_resultsum)) * S ((dst_negative_code_concat_resultsum) + (dst_negative_scale_concat_resultsum)) + ((dst_negative_scale_concat_resultsum) + (dst_negative_scale_concat_resultsum)))) + ((((dst_negative_code_concat_resultsum) + (dst_negative_scale_concat_resultsum)) * S ((dst_negative_code_concat_resultsum) + (dst_negative_scale_concat_resultsum)) + ((dst_negative_scale_concat_resultsum) + (dst_negative_scale_concat_resultsum))) + (((dst_negative_code_concat_resultsum) + (dst_negative_scale_concat_resultsum)) * S ((dst_negative_code_concat_resultsum) + (dst_negative_scale_concat_resultsum)) + ((dst_negative_scale_concat_resultsum) + (dst_negative_scale_concat_resultsum)))))) /\ (((exists fs_u_dst_concat_resultsumpositive fs_v_dst_concat_resultsumpositive. ((((exists fs_h_dst_concat_resultsumpositive_body_start. fs_h_dst_concat_resultsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_resultsumpositive)) /\ exists fs_q_dst_concat_resultsumpositive_body_start. fs_u_dst_concat_resultsumpositive = fs_q_dst_concat_resultsumpositive_body_start * S ((S (0)) * fs_v_dst_concat_resultsumpositive) + (0))) /\ ((((exists fs_h_dst_concat_resultsumpositive_body_terminal. fs_h_dst_concat_resultsumpositive_body_terminal + S (dst_positive_sum_concat_resultsum) = S ((S (p+q)) * fs_v_dst_concat_resultsumpositive)) /\ exists fs_q_dst_concat_resultsumpositive_body_terminal. fs_u_dst_concat_resultsumpositive = fs_q_dst_concat_resultsumpositive_body_terminal * S ((S (p+q)) * fs_v_dst_concat_resultsumpositive) + (dst_positive_sum_concat_resultsum))) /\ forall fs_i_dst_concat_resultsumpositive_body_steps. (exists fs_lt_dst_concat_resultsumpositive_body_steps_bound. fs_lt_dst_concat_resultsumpositive_body_steps_bound + S fs_i_dst_concat_resultsumpositive_body_steps = p+q) -> exists fs_a_dst_concat_resultsumpositive_body_steps fs_r_dst_concat_resultsumpositive_body_steps fs_s_dst_concat_resultsumpositive_body_steps. ((((exists fs_h_dst_concat_resultsumpositive_body_steps_summand. fs_h_dst_concat_resultsumpositive_body_steps_summand + S (fs_a_dst_concat_resultsumpositive_body_steps) = S ((S (fs_i_dst_concat_resultsumpositive_body_steps)) * dst_positive_scale_concat_resultsum)) /\ exists fs_q_dst_concat_resultsumpositive_body_steps_summand. dst_positive_code_concat_resultsum = fs_q_dst_concat_resultsumpositive_body_steps_summand * S ((S (fs_i_dst_concat_resultsumpositive_body_steps)) * dst_positive_scale_concat_resultsum) + (fs_a_dst_concat_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_resultsumpositive_body_steps_partial. fs_h_dst_concat_resultsumpositive_body_steps_partial + S (fs_r_dst_concat_resultsumpositive_body_steps) = S ((S (fs_i_dst_concat_resultsumpositive_body_steps)) * fs_v_dst_concat_resultsumpositive)) /\ exists fs_q_dst_concat_resultsumpositive_body_steps_partial. fs_u_dst_concat_resultsumpositive = fs_q_dst_concat_resultsumpositive_body_steps_partial * S ((S (fs_i_dst_concat_resultsumpositive_body_steps)) * fs_v_dst_concat_resultsumpositive) + (fs_r_dst_concat_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_concat_resultsumpositive_body_steps_successor. fs_h_dst_concat_resultsumpositive_body_steps_successor + S (fs_s_dst_concat_resultsumpositive_body_steps) = S ((S (S fs_i_dst_concat_resultsumpositive_body_steps)) * fs_v_dst_concat_resultsumpositive)) /\ exists fs_q_dst_concat_resultsumpositive_body_steps_successor. fs_u_dst_concat_resultsumpositive = fs_q_dst_concat_resultsumpositive_body_steps_successor * S ((S (S fs_i_dst_concat_resultsumpositive_body_steps)) * fs_v_dst_concat_resultsumpositive) + (fs_s_dst_concat_resultsumpositive_body_steps))) /\ fs_s_dst_concat_resultsumpositive_body_steps = fs_r_dst_concat_resultsumpositive_body_steps + fs_a_dst_concat_resultsumpositive_body_steps)))))) /\ (((exists fs_u_dst_concat_resultsumnegative fs_v_dst_concat_resultsumnegative. ((((exists fs_h_dst_concat_resultsumnegative_body_start. fs_h_dst_concat_resultsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_concat_resultsumnegative)) /\ exists fs_q_dst_concat_resultsumnegative_body_start. fs_u_dst_concat_resultsumnegative = fs_q_dst_concat_resultsumnegative_body_start * S ((S (0)) * fs_v_dst_concat_resultsumnegative) + (0))) /\ ((((exists fs_h_dst_concat_resultsumnegative_body_terminal. fs_h_dst_concat_resultsumnegative_body_terminal + S (dst_negative_sum_concat_resultsum) = S ((S (p+q)) * fs_v_dst_concat_resultsumnegative)) /\ exists fs_q_dst_concat_resultsumnegative_body_terminal. fs_u_dst_concat_resultsumnegative = fs_q_dst_concat_resultsumnegative_body_terminal * S ((S (p+q)) * fs_v_dst_concat_resultsumnegative) + (dst_negative_sum_concat_resultsum))) /\ forall fs_i_dst_concat_resultsumnegative_body_steps. (exists fs_lt_dst_concat_resultsumnegative_body_steps_bound. fs_lt_dst_concat_resultsumnegative_body_steps_bound + S fs_i_dst_concat_resultsumnegative_body_steps = p+q) -> exists fs_a_dst_concat_resultsumnegative_body_steps fs_r_dst_concat_resultsumnegative_body_steps fs_s_dst_concat_resultsumnegative_body_steps. ((((exists fs_h_dst_concat_resultsumnegative_body_steps_summand. fs_h_dst_concat_resultsumnegative_body_steps_summand + S (fs_a_dst_concat_resultsumnegative_body_steps) = S ((S (fs_i_dst_concat_resultsumnegative_body_steps)) * dst_negative_scale_concat_resultsum)) /\ exists fs_q_dst_concat_resultsumnegative_body_steps_summand. dst_negative_code_concat_resultsum = fs_q_dst_concat_resultsumnegative_body_steps_summand * S ((S (fs_i_dst_concat_resultsumnegative_body_steps)) * dst_negative_scale_concat_resultsum) + (fs_a_dst_concat_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_resultsumnegative_body_steps_partial. fs_h_dst_concat_resultsumnegative_body_steps_partial + S (fs_r_dst_concat_resultsumnegative_body_steps) = S ((S (fs_i_dst_concat_resultsumnegative_body_steps)) * fs_v_dst_concat_resultsumnegative)) /\ exists fs_q_dst_concat_resultsumnegative_body_steps_partial. fs_u_dst_concat_resultsumnegative = fs_q_dst_concat_resultsumnegative_body_steps_partial * S ((S (fs_i_dst_concat_resultsumnegative_body_steps)) * fs_v_dst_concat_resultsumnegative) + (fs_r_dst_concat_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_concat_resultsumnegative_body_steps_successor. fs_h_dst_concat_resultsumnegative_body_steps_successor + S (fs_s_dst_concat_resultsumnegative_body_steps) = S ((S (S fs_i_dst_concat_resultsumnegative_body_steps)) * fs_v_dst_concat_resultsumnegative)) /\ exists fs_q_dst_concat_resultsumnegative_body_steps_successor. fs_u_dst_concat_resultsumnegative = fs_q_dst_concat_resultsumnegative_body_steps_successor * S ((S (S fs_i_dst_concat_resultsumnegative_body_steps)) * fs_v_dst_concat_resultsumnegative) + (fs_s_dst_concat_resultsumnegative_body_steps))) /\ fs_s_dst_concat_resultsumnegative_body_steps = fs_r_dst_concat_resultsumnegative_body_steps + fs_a_dst_concat_resultsumnegative_body_steps)))))) /\ (exists ge_balance_positive_concat_resultsumresult ge_balance_negative_concat_resultsumresult. (((((c) = 2 * (ge_balance_positive_concat_resultsumresult) /\ (ge_balance_negative_concat_resultsumresult) = 0) \/ exists ge_signed_half_concat_resultsumresultdecode. (((c) = 2 * ge_signed_half_concat_resultsumresultdecode + 1 /\ (ge_balance_positive_concat_resultsumresult) = 0) /\ (ge_balance_negative_concat_resultsumresult) = S ge_signed_half_concat_resultsumresultdecode))) /\ ((dst_positive_sum_concat_resultsum) + ge_balance_negative_concat_resultsumresult = (dst_negative_sum_concat_resultsum) + ge_balance_positive_concat_resultsumresult)))))))))))