signed_rectangular_slice_sum_functional

Exact expanded first-order arithmetic statement

forall F o s l a b. (exists srs_slice_sum_functional_first. ((((exists dst_positive_code_sum_functional_firstslicesource_table dst_positive_scale_sum_functional_firstslicesource_table dst_negative_code_sum_functional_firstslicesource_table dst_negative_scale_sum_functional_firstslicesource_table. (((F) = (((((dst_positive_code_sum_functional_firstslicesource_table) + (dst_positive_scale_sum_functional_firstslicesource_table)) * S ((dst_positive_code_sum_functional_firstslicesource_table) + (dst_positive_scale_sum_functional_firstslicesource_table)) + ((dst_positive_scale_sum_functional_firstslicesource_table) + (dst_positive_scale_sum_functional_firstslicesource_table))) + (((dst_negative_code_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)) * S ((dst_negative_code_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)) + ((dst_negative_scale_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)))) * S ((((dst_positive_code_sum_functional_firstslicesource_table) + (dst_positive_scale_sum_functional_firstslicesource_table)) * S ((dst_positive_code_sum_functional_firstslicesource_table) + (dst_positive_scale_sum_functional_firstslicesource_table)) + ((dst_positive_scale_sum_functional_firstslicesource_table) + (dst_positive_scale_sum_functional_firstslicesource_table))) + (((dst_negative_code_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)) * S ((dst_negative_code_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)) + ((dst_negative_scale_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)))) + ((((dst_negative_code_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)) * S ((dst_negative_code_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)) + ((dst_negative_scale_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table))) + (((dst_negative_code_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)) * S ((dst_negative_code_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)) + ((dst_negative_scale_sum_functional_firstslicesource_table) + (dst_negative_scale_sum_functional_firstslicesource_table)))))) /\ (forall dst_index_sum_functional_firstslicesource_table. (exists pvs_le_gap_sum_functional_firstslicesource_tabledomain. pvs_le_gap_sum_functional_firstslicesource_tabledomain + (dst_index_sum_functional_firstslicesource_table) = (0)) -> exists dst_positive_sum_functional_firstslicesource_table dst_negative_sum_functional_firstslicesource_table dst_value_sum_functional_firstslicesource_table. ((((exists ff_h_pvs_sum_functional_firstslicesource_tableentrypositive. ff_h_pvs_sum_functional_firstslicesource_tableentrypositive + S (dst_positive_sum_functional_firstslicesource_table) = S ((S (dst_index_sum_functional_firstslicesource_table)) * dst_positive_scale_sum_functional_firstslicesource_table)) /\ exists ff_q_pvs_sum_functional_firstslicesource_tableentrypositive. dst_positive_code_sum_functional_firstslicesource_table = ff_q_pvs_sum_functional_firstslicesource_tableentrypositive * S ((S (dst_index_sum_functional_firstslicesource_table)) * dst_positive_scale_sum_functional_firstslicesource_table) + (dst_positive_sum_functional_firstslicesource_table))) /\ (((((exists ff_h_pvs_sum_functional_firstslicesource_tableentrynegative. ff_h_pvs_sum_functional_firstslicesource_tableentrynegative + S (dst_negative_sum_functional_firstslicesource_table) = S ((S (dst_index_sum_functional_firstslicesource_table)) * dst_negative_scale_sum_functional_firstslicesource_table)) /\ exists ff_q_pvs_sum_functional_firstslicesource_tableentrynegative. dst_negative_code_sum_functional_firstslicesource_table = ff_q_pvs_sum_functional_firstslicesource_tableentrynegative * S ((S (dst_index_sum_functional_firstslicesource_table)) * dst_negative_scale_sum_functional_firstslicesource_table) + (dst_negative_sum_functional_firstslicesource_table))) /\ (exists ge_balance_positive_sum_functional_firstslicesource_tableentryvalue ge_balance_negative_sum_functional_firstslicesource_tableentryvalue. (((((dst_value_sum_functional_firstslicesource_table) = 2 * (ge_balance_positive_sum_functional_firstslicesource_tableentryvalue) /\ (ge_balance_negative_sum_functional_firstslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_firstslicesource_tableentryvaluedecode. (((dst_value_sum_functional_firstslicesource_table) = 2 * ge_signed_half_sum_functional_firstslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_firstslicesource_tableentryvalue) = S ge_signed_half_sum_functional_firstslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_firstslicesource_table) + ge_balance_negative_sum_functional_firstslicesource_tableentryvalue = (dst_negative_sum_functional_firstslicesource_table) + ge_balance_positive_sum_functional_firstslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_functional_firstsliceoutput_table dst_positive_scale_sum_functional_firstsliceoutput_table dst_negative_code_sum_functional_firstsliceoutput_table dst_negative_scale_sum_functional_firstsliceoutput_table. (((srs_slice_sum_functional_first) = (((((dst_positive_code_sum_functional_firstsliceoutput_table) + (dst_positive_scale_sum_functional_firstsliceoutput_table)) * S ((dst_positive_code_sum_functional_firstsliceoutput_table) + (dst_positive_scale_sum_functional_firstsliceoutput_table)) + ((dst_positive_scale_sum_functional_firstsliceoutput_table) + (dst_positive_scale_sum_functional_firstsliceoutput_table))) + (((dst_negative_code_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)) * S ((dst_negative_code_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)) + ((dst_negative_scale_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)))) * S ((((dst_positive_code_sum_functional_firstsliceoutput_table) + (dst_positive_scale_sum_functional_firstsliceoutput_table)) * S ((dst_positive_code_sum_functional_firstsliceoutput_table) + (dst_positive_scale_sum_functional_firstsliceoutput_table)) + ((dst_positive_scale_sum_functional_firstsliceoutput_table) + (dst_positive_scale_sum_functional_firstsliceoutput_table))) + (((dst_negative_code_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)) * S ((dst_negative_code_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)) + ((dst_negative_scale_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)))) + ((((dst_negative_code_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)) * S ((dst_negative_code_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)) + ((dst_negative_scale_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table))) + (((dst_negative_code_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)) * S ((dst_negative_code_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)) + ((dst_negative_scale_sum_functional_firstsliceoutput_table) + (dst_negative_scale_sum_functional_firstsliceoutput_table)))))) /\ (forall dst_index_sum_functional_firstsliceoutput_table. (exists pvs_le_gap_sum_functional_firstsliceoutput_tabledomain. pvs_le_gap_sum_functional_firstsliceoutput_tabledomain + (dst_index_sum_functional_firstsliceoutput_table) = (l)) -> exists dst_positive_sum_functional_firstsliceoutput_table dst_negative_sum_functional_firstsliceoutput_table dst_value_sum_functional_firstsliceoutput_table. ((((exists ff_h_pvs_sum_functional_firstsliceoutput_tableentrypositive. ff_h_pvs_sum_functional_firstsliceoutput_tableentrypositive + S (dst_positive_sum_functional_firstsliceoutput_table) = S ((S (dst_index_sum_functional_firstsliceoutput_table)) * dst_positive_scale_sum_functional_firstsliceoutput_table)) /\ exists ff_q_pvs_sum_functional_firstsliceoutput_tableentrypositive. dst_positive_code_sum_functional_firstsliceoutput_table = ff_q_pvs_sum_functional_firstsliceoutput_tableentrypositive * S ((S (dst_index_sum_functional_firstsliceoutput_table)) * dst_positive_scale_sum_functional_firstsliceoutput_table) + (dst_positive_sum_functional_firstsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_functional_firstsliceoutput_tableentrynegative. ff_h_pvs_sum_functional_firstsliceoutput_tableentrynegative + S (dst_negative_sum_functional_firstsliceoutput_table) = S ((S (dst_index_sum_functional_firstsliceoutput_table)) * dst_negative_scale_sum_functional_firstsliceoutput_table)) /\ exists ff_q_pvs_sum_functional_firstsliceoutput_tableentrynegative. dst_negative_code_sum_functional_firstsliceoutput_table = ff_q_pvs_sum_functional_firstsliceoutput_tableentrynegative * S ((S (dst_index_sum_functional_firstsliceoutput_table)) * dst_negative_scale_sum_functional_firstsliceoutput_table) + (dst_negative_sum_functional_firstsliceoutput_table))) /\ (exists ge_balance_positive_sum_functional_firstsliceoutput_tableentryvalue ge_balance_negative_sum_functional_firstsliceoutput_tableentryvalue. (((((dst_value_sum_functional_firstsliceoutput_table) = 2 * (ge_balance_positive_sum_functional_firstsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_functional_firstsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_firstsliceoutput_tableentryvaluedecode. (((dst_value_sum_functional_firstsliceoutput_table) = 2 * ge_signed_half_sum_functional_firstsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_firstsliceoutput_tableentryvalue) = S ge_signed_half_sum_functional_firstsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_firstsliceoutput_table) + ge_balance_negative_sum_functional_firstsliceoutput_tableentryvalue = (dst_negative_sum_functional_firstsliceoutput_table) + ge_balance_positive_sum_functional_firstsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_functional_firstslice. (exists pvs_gap_sum_functional_firstslicebound. pvs_gap_sum_functional_firstslicebound + S (srs_index_sum_functional_firstslice) = (l)) -> exists srs_value_sum_functional_firstslice. (((exists dst_positive_code_sum_functional_firstsliceentrysource dst_positive_scale_sum_functional_firstsliceentrysource dst_negative_code_sum_functional_firstsliceentrysource dst_negative_scale_sum_functional_firstsliceentrysource dst_positive_sum_functional_firstsliceentrysource dst_negative_sum_functional_firstsliceentrysource. (((F) = (((((dst_positive_code_sum_functional_firstsliceentrysource) + (dst_positive_scale_sum_functional_firstsliceentrysource)) * S ((dst_positive_code_sum_functional_firstsliceentrysource) + (dst_positive_scale_sum_functional_firstsliceentrysource)) + ((dst_positive_scale_sum_functional_firstsliceentrysource) + (dst_positive_scale_sum_functional_firstsliceentrysource))) + (((dst_negative_code_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)) * S ((dst_negative_code_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)) + ((dst_negative_scale_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)))) * S ((((dst_positive_code_sum_functional_firstsliceentrysource) + (dst_positive_scale_sum_functional_firstsliceentrysource)) * S ((dst_positive_code_sum_functional_firstsliceentrysource) + (dst_positive_scale_sum_functional_firstsliceentrysource)) + ((dst_positive_scale_sum_functional_firstsliceentrysource) + (dst_positive_scale_sum_functional_firstsliceentrysource))) + (((dst_negative_code_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)) * S ((dst_negative_code_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)) + ((dst_negative_scale_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)))) + ((((dst_negative_code_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)) * S ((dst_negative_code_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)) + ((dst_negative_scale_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource))) + (((dst_negative_code_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)) * S ((dst_negative_code_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)) + ((dst_negative_scale_sum_functional_firstsliceentrysource) + (dst_negative_scale_sum_functional_firstsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_functional_firstsliceentrysourcepositive. ff_h_pvs_sum_functional_firstsliceentrysourcepositive + S (dst_positive_sum_functional_firstsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_functional_firstslice))))) * dst_positive_scale_sum_functional_firstsliceentrysource)) /\ exists ff_q_pvs_sum_functional_firstsliceentrysourcepositive. dst_positive_code_sum_functional_firstsliceentrysource = ff_q_pvs_sum_functional_firstsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_functional_firstslice))))) * dst_positive_scale_sum_functional_firstsliceentrysource) + (dst_positive_sum_functional_firstsliceentrysource))) /\ (((((exists ff_h_pvs_sum_functional_firstsliceentrysourcenegative. ff_h_pvs_sum_functional_firstsliceentrysourcenegative + S (dst_negative_sum_functional_firstsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_functional_firstslice))))) * dst_negative_scale_sum_functional_firstsliceentrysource)) /\ exists ff_q_pvs_sum_functional_firstsliceentrysourcenegative. dst_negative_code_sum_functional_firstsliceentrysource = ff_q_pvs_sum_functional_firstsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_functional_firstslice))))) * dst_negative_scale_sum_functional_firstsliceentrysource) + (dst_negative_sum_functional_firstsliceentrysource))) /\ (exists ge_balance_positive_sum_functional_firstsliceentrysourcevalue ge_balance_negative_sum_functional_firstsliceentrysourcevalue. (((((srs_value_sum_functional_firstslice) = 2 * (ge_balance_positive_sum_functional_firstsliceentrysourcevalue) /\ (ge_balance_negative_sum_functional_firstsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_functional_firstsliceentrysourcevaluedecode. (((srs_value_sum_functional_firstslice) = 2 * ge_signed_half_sum_functional_firstsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_functional_firstsliceentrysourcevalue) = S ge_signed_half_sum_functional_firstsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_functional_firstsliceentrysource) + ge_balance_negative_sum_functional_firstsliceentrysourcevalue = (dst_negative_sum_functional_firstsliceentrysource) + ge_balance_positive_sum_functional_firstsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_functional_firstsliceentryoutput dst_positive_scale_sum_functional_firstsliceentryoutput dst_negative_code_sum_functional_firstsliceentryoutput dst_negative_scale_sum_functional_firstsliceentryoutput dst_positive_sum_functional_firstsliceentryoutput dst_negative_sum_functional_firstsliceentryoutput. (((srs_slice_sum_functional_first) = (((((dst_positive_code_sum_functional_firstsliceentryoutput) + (dst_positive_scale_sum_functional_firstsliceentryoutput)) * S ((dst_positive_code_sum_functional_firstsliceentryoutput) + (dst_positive_scale_sum_functional_firstsliceentryoutput)) + ((dst_positive_scale_sum_functional_firstsliceentryoutput) + (dst_positive_scale_sum_functional_firstsliceentryoutput))) + (((dst_negative_code_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)) * S ((dst_negative_code_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)) + ((dst_negative_scale_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)))) * S ((((dst_positive_code_sum_functional_firstsliceentryoutput) + (dst_positive_scale_sum_functional_firstsliceentryoutput)) * S ((dst_positive_code_sum_functional_firstsliceentryoutput) + (dst_positive_scale_sum_functional_firstsliceentryoutput)) + ((dst_positive_scale_sum_functional_firstsliceentryoutput) + (dst_positive_scale_sum_functional_firstsliceentryoutput))) + (((dst_negative_code_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)) * S ((dst_negative_code_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)) + ((dst_negative_scale_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)))) + ((((dst_negative_code_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)) * S ((dst_negative_code_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)) + ((dst_negative_scale_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput))) + (((dst_negative_code_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)) * S ((dst_negative_code_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)) + ((dst_negative_scale_sum_functional_firstsliceentryoutput) + (dst_negative_scale_sum_functional_firstsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_functional_firstsliceentryoutputpositive. ff_h_pvs_sum_functional_firstsliceentryoutputpositive + S (dst_positive_sum_functional_firstsliceentryoutput) = S ((S (srs_index_sum_functional_firstslice)) * dst_positive_scale_sum_functional_firstsliceentryoutput)) /\ exists ff_q_pvs_sum_functional_firstsliceentryoutputpositive. dst_positive_code_sum_functional_firstsliceentryoutput = ff_q_pvs_sum_functional_firstsliceentryoutputpositive * S ((S (srs_index_sum_functional_firstslice)) * dst_positive_scale_sum_functional_firstsliceentryoutput) + (dst_positive_sum_functional_firstsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_functional_firstsliceentryoutputnegative. ff_h_pvs_sum_functional_firstsliceentryoutputnegative + S (dst_negative_sum_functional_firstsliceentryoutput) = S ((S (srs_index_sum_functional_firstslice)) * dst_negative_scale_sum_functional_firstsliceentryoutput)) /\ exists ff_q_pvs_sum_functional_firstsliceentryoutputnegative. dst_negative_code_sum_functional_firstsliceentryoutput = ff_q_pvs_sum_functional_firstsliceentryoutputnegative * S ((S (srs_index_sum_functional_firstslice)) * dst_negative_scale_sum_functional_firstsliceentryoutput) + (dst_negative_sum_functional_firstsliceentryoutput))) /\ (exists ge_balance_positive_sum_functional_firstsliceentryoutputvalue ge_balance_negative_sum_functional_firstsliceentryoutputvalue. (((((srs_value_sum_functional_firstslice) = 2 * (ge_balance_positive_sum_functional_firstsliceentryoutputvalue) /\ (ge_balance_negative_sum_functional_firstsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_functional_firstsliceentryoutputvaluedecode. (((srs_value_sum_functional_firstslice) = 2 * ge_signed_half_sum_functional_firstsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_functional_firstsliceentryoutputvalue) = S ge_signed_half_sum_functional_firstsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_functional_firstsliceentryoutput) + ge_balance_negative_sum_functional_firstsliceentryoutputvalue = (dst_negative_sum_functional_firstsliceentryoutput) + ge_balance_positive_sum_functional_firstsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_functional_firstsum dst_positive_scale_sum_functional_firstsum dst_negative_code_sum_functional_firstsum dst_negative_scale_sum_functional_firstsum dst_positive_sum_sum_functional_firstsum dst_negative_sum_sum_functional_firstsum. (((srs_slice_sum_functional_first) = (((((dst_positive_code_sum_functional_firstsum) + (dst_positive_scale_sum_functional_firstsum)) * S ((dst_positive_code_sum_functional_firstsum) + (dst_positive_scale_sum_functional_firstsum)) + ((dst_positive_scale_sum_functional_firstsum) + (dst_positive_scale_sum_functional_firstsum))) + (((dst_negative_code_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)) * S ((dst_negative_code_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)) + ((dst_negative_scale_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)))) * S ((((dst_positive_code_sum_functional_firstsum) + (dst_positive_scale_sum_functional_firstsum)) * S ((dst_positive_code_sum_functional_firstsum) + (dst_positive_scale_sum_functional_firstsum)) + ((dst_positive_scale_sum_functional_firstsum) + (dst_positive_scale_sum_functional_firstsum))) + (((dst_negative_code_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)) * S ((dst_negative_code_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)) + ((dst_negative_scale_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)))) + ((((dst_negative_code_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)) * S ((dst_negative_code_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)) + ((dst_negative_scale_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum))) + (((dst_negative_code_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)) * S ((dst_negative_code_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)) + ((dst_negative_scale_sum_functional_firstsum) + (dst_negative_scale_sum_functional_firstsum)))))) /\ (((exists fs_u_dst_sum_functional_firstsumpositive fs_v_dst_sum_functional_firstsumpositive. ((((exists fs_h_dst_sum_functional_firstsumpositive_body_start. fs_h_dst_sum_functional_firstsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_firstsumpositive)) /\ exists fs_q_dst_sum_functional_firstsumpositive_body_start. fs_u_dst_sum_functional_firstsumpositive = fs_q_dst_sum_functional_firstsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_functional_firstsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_functional_firstsumpositive_body_terminal. fs_h_dst_sum_functional_firstsumpositive_body_terminal + S (dst_positive_sum_sum_functional_firstsum) = S ((S (l)) * fs_v_dst_sum_functional_firstsumpositive)) /\ exists fs_q_dst_sum_functional_firstsumpositive_body_terminal. fs_u_dst_sum_functional_firstsumpositive = fs_q_dst_sum_functional_firstsumpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_functional_firstsumpositive) + (dst_positive_sum_sum_functional_firstsum))) /\ forall fs_i_dst_sum_functional_firstsumpositive_body_steps. (exists fs_lt_dst_sum_functional_firstsumpositive_body_steps_bound. fs_lt_dst_sum_functional_firstsumpositive_body_steps_bound + S fs_i_dst_sum_functional_firstsumpositive_body_steps = l) -> exists fs_a_dst_sum_functional_firstsumpositive_body_steps fs_r_dst_sum_functional_firstsumpositive_body_steps fs_s_dst_sum_functional_firstsumpositive_body_steps. ((((exists fs_h_dst_sum_functional_firstsumpositive_body_steps_summand. fs_h_dst_sum_functional_firstsumpositive_body_steps_summand + S (fs_a_dst_sum_functional_firstsumpositive_body_steps) = S ((S (fs_i_dst_sum_functional_firstsumpositive_body_steps)) * dst_positive_scale_sum_functional_firstsum)) /\ exists fs_q_dst_sum_functional_firstsumpositive_body_steps_summand. dst_positive_code_sum_functional_firstsum = fs_q_dst_sum_functional_firstsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_functional_firstsumpositive_body_steps)) * dst_positive_scale_sum_functional_firstsum) + (fs_a_dst_sum_functional_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firstsumpositive_body_steps_partial. fs_h_dst_sum_functional_firstsumpositive_body_steps_partial + S (fs_r_dst_sum_functional_firstsumpositive_body_steps) = S ((S (fs_i_dst_sum_functional_firstsumpositive_body_steps)) * fs_v_dst_sum_functional_firstsumpositive)) /\ exists fs_q_dst_sum_functional_firstsumpositive_body_steps_partial. fs_u_dst_sum_functional_firstsumpositive = fs_q_dst_sum_functional_firstsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_functional_firstsumpositive_body_steps)) * fs_v_dst_sum_functional_firstsumpositive) + (fs_r_dst_sum_functional_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firstsumpositive_body_steps_successor. fs_h_dst_sum_functional_firstsumpositive_body_steps_successor + S (fs_s_dst_sum_functional_firstsumpositive_body_steps) = S ((S (S fs_i_dst_sum_functional_firstsumpositive_body_steps)) * fs_v_dst_sum_functional_firstsumpositive)) /\ exists fs_q_dst_sum_functional_firstsumpositive_body_steps_successor. fs_u_dst_sum_functional_firstsumpositive = fs_q_dst_sum_functional_firstsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_functional_firstsumpositive_body_steps)) * fs_v_dst_sum_functional_firstsumpositive) + (fs_s_dst_sum_functional_firstsumpositive_body_steps))) /\ fs_s_dst_sum_functional_firstsumpositive_body_steps = fs_r_dst_sum_functional_firstsumpositive_body_steps + fs_a_dst_sum_functional_firstsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_functional_firstsumnegative fs_v_dst_sum_functional_firstsumnegative. ((((exists fs_h_dst_sum_functional_firstsumnegative_body_start. fs_h_dst_sum_functional_firstsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_firstsumnegative)) /\ exists fs_q_dst_sum_functional_firstsumnegative_body_start. fs_u_dst_sum_functional_firstsumnegative = fs_q_dst_sum_functional_firstsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_functional_firstsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_functional_firstsumnegative_body_terminal. fs_h_dst_sum_functional_firstsumnegative_body_terminal + S (dst_negative_sum_sum_functional_firstsum) = S ((S (l)) * fs_v_dst_sum_functional_firstsumnegative)) /\ exists fs_q_dst_sum_functional_firstsumnegative_body_terminal. fs_u_dst_sum_functional_firstsumnegative = fs_q_dst_sum_functional_firstsumnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_functional_firstsumnegative) + (dst_negative_sum_sum_functional_firstsum))) /\ forall fs_i_dst_sum_functional_firstsumnegative_body_steps. (exists fs_lt_dst_sum_functional_firstsumnegative_body_steps_bound. fs_lt_dst_sum_functional_firstsumnegative_body_steps_bound + S fs_i_dst_sum_functional_firstsumnegative_body_steps = l) -> exists fs_a_dst_sum_functional_firstsumnegative_body_steps fs_r_dst_sum_functional_firstsumnegative_body_steps fs_s_dst_sum_functional_firstsumnegative_body_steps. ((((exists fs_h_dst_sum_functional_firstsumnegative_body_steps_summand. fs_h_dst_sum_functional_firstsumnegative_body_steps_summand + S (fs_a_dst_sum_functional_firstsumnegative_body_steps) = S ((S (fs_i_dst_sum_functional_firstsumnegative_body_steps)) * dst_negative_scale_sum_functional_firstsum)) /\ exists fs_q_dst_sum_functional_firstsumnegative_body_steps_summand. dst_negative_code_sum_functional_firstsum = fs_q_dst_sum_functional_firstsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_functional_firstsumnegative_body_steps)) * dst_negative_scale_sum_functional_firstsum) + (fs_a_dst_sum_functional_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firstsumnegative_body_steps_partial. fs_h_dst_sum_functional_firstsumnegative_body_steps_partial + S (fs_r_dst_sum_functional_firstsumnegative_body_steps) = S ((S (fs_i_dst_sum_functional_firstsumnegative_body_steps)) * fs_v_dst_sum_functional_firstsumnegative)) /\ exists fs_q_dst_sum_functional_firstsumnegative_body_steps_partial. fs_u_dst_sum_functional_firstsumnegative = fs_q_dst_sum_functional_firstsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_functional_firstsumnegative_body_steps)) * fs_v_dst_sum_functional_firstsumnegative) + (fs_r_dst_sum_functional_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firstsumnegative_body_steps_successor. fs_h_dst_sum_functional_firstsumnegative_body_steps_successor + S (fs_s_dst_sum_functional_firstsumnegative_body_steps) = S ((S (S fs_i_dst_sum_functional_firstsumnegative_body_steps)) * fs_v_dst_sum_functional_firstsumnegative)) /\ exists fs_q_dst_sum_functional_firstsumnegative_body_steps_successor. fs_u_dst_sum_functional_firstsumnegative = fs_q_dst_sum_functional_firstsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_functional_firstsumnegative_body_steps)) * fs_v_dst_sum_functional_firstsumnegative) + (fs_s_dst_sum_functional_firstsumnegative_body_steps))) /\ fs_s_dst_sum_functional_firstsumnegative_body_steps = fs_r_dst_sum_functional_firstsumnegative_body_steps + fs_a_dst_sum_functional_firstsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_functional_firstsumresult ge_balance_negative_sum_functional_firstsumresult. (((((a) = 2 * (ge_balance_positive_sum_functional_firstsumresult) /\ (ge_balance_negative_sum_functional_firstsumresult) = 0) \/ exists ge_signed_half_sum_functional_firstsumresultdecode. (((a) = 2 * ge_signed_half_sum_functional_firstsumresultdecode + 1 /\ (ge_balance_positive_sum_functional_firstsumresult) = 0) /\ (ge_balance_negative_sum_functional_firstsumresult) = S ge_signed_half_sum_functional_firstsumresultdecode))) /\ ((dst_positive_sum_sum_functional_firstsum) + ge_balance_negative_sum_functional_firstsumresult = (dst_negative_sum_sum_functional_firstsum) + ge_balance_positive_sum_functional_firstsumresult))))))))))) -> (exists srs_slice_sum_functional_second. ((((exists dst_positive_code_sum_functional_secondslicesource_table dst_positive_scale_sum_functional_secondslicesource_table dst_negative_code_sum_functional_secondslicesource_table dst_negative_scale_sum_functional_secondslicesource_table. (((F) = (((((dst_positive_code_sum_functional_secondslicesource_table) + (dst_positive_scale_sum_functional_secondslicesource_table)) * S ((dst_positive_code_sum_functional_secondslicesource_table) + (dst_positive_scale_sum_functional_secondslicesource_table)) + ((dst_positive_scale_sum_functional_secondslicesource_table) + (dst_positive_scale_sum_functional_secondslicesource_table))) + (((dst_negative_code_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)) * S ((dst_negative_code_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)) + ((dst_negative_scale_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)))) * S ((((dst_positive_code_sum_functional_secondslicesource_table) + (dst_positive_scale_sum_functional_secondslicesource_table)) * S ((dst_positive_code_sum_functional_secondslicesource_table) + (dst_positive_scale_sum_functional_secondslicesource_table)) + ((dst_positive_scale_sum_functional_secondslicesource_table) + (dst_positive_scale_sum_functional_secondslicesource_table))) + (((dst_negative_code_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)) * S ((dst_negative_code_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)) + ((dst_negative_scale_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)))) + ((((dst_negative_code_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)) * S ((dst_negative_code_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)) + ((dst_negative_scale_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table))) + (((dst_negative_code_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)) * S ((dst_negative_code_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)) + ((dst_negative_scale_sum_functional_secondslicesource_table) + (dst_negative_scale_sum_functional_secondslicesource_table)))))) /\ (forall dst_index_sum_functional_secondslicesource_table. (exists pvs_le_gap_sum_functional_secondslicesource_tabledomain. pvs_le_gap_sum_functional_secondslicesource_tabledomain + (dst_index_sum_functional_secondslicesource_table) = (0)) -> exists dst_positive_sum_functional_secondslicesource_table dst_negative_sum_functional_secondslicesource_table dst_value_sum_functional_secondslicesource_table. ((((exists ff_h_pvs_sum_functional_secondslicesource_tableentrypositive. ff_h_pvs_sum_functional_secondslicesource_tableentrypositive + S (dst_positive_sum_functional_secondslicesource_table) = S ((S (dst_index_sum_functional_secondslicesource_table)) * dst_positive_scale_sum_functional_secondslicesource_table)) /\ exists ff_q_pvs_sum_functional_secondslicesource_tableentrypositive. dst_positive_code_sum_functional_secondslicesource_table = ff_q_pvs_sum_functional_secondslicesource_tableentrypositive * S ((S (dst_index_sum_functional_secondslicesource_table)) * dst_positive_scale_sum_functional_secondslicesource_table) + (dst_positive_sum_functional_secondslicesource_table))) /\ (((((exists ff_h_pvs_sum_functional_secondslicesource_tableentrynegative. ff_h_pvs_sum_functional_secondslicesource_tableentrynegative + S (dst_negative_sum_functional_secondslicesource_table) = S ((S (dst_index_sum_functional_secondslicesource_table)) * dst_negative_scale_sum_functional_secondslicesource_table)) /\ exists ff_q_pvs_sum_functional_secondslicesource_tableentrynegative. dst_negative_code_sum_functional_secondslicesource_table = ff_q_pvs_sum_functional_secondslicesource_tableentrynegative * S ((S (dst_index_sum_functional_secondslicesource_table)) * dst_negative_scale_sum_functional_secondslicesource_table) + (dst_negative_sum_functional_secondslicesource_table))) /\ (exists ge_balance_positive_sum_functional_secondslicesource_tableentryvalue ge_balance_negative_sum_functional_secondslicesource_tableentryvalue. (((((dst_value_sum_functional_secondslicesource_table) = 2 * (ge_balance_positive_sum_functional_secondslicesource_tableentryvalue) /\ (ge_balance_negative_sum_functional_secondslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_secondslicesource_tableentryvaluedecode. (((dst_value_sum_functional_secondslicesource_table) = 2 * ge_signed_half_sum_functional_secondslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_secondslicesource_tableentryvalue) = S ge_signed_half_sum_functional_secondslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_secondslicesource_table) + ge_balance_negative_sum_functional_secondslicesource_tableentryvalue = (dst_negative_sum_functional_secondslicesource_table) + ge_balance_positive_sum_functional_secondslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_functional_secondsliceoutput_table dst_positive_scale_sum_functional_secondsliceoutput_table dst_negative_code_sum_functional_secondsliceoutput_table dst_negative_scale_sum_functional_secondsliceoutput_table. (((srs_slice_sum_functional_second) = (((((dst_positive_code_sum_functional_secondsliceoutput_table) + (dst_positive_scale_sum_functional_secondsliceoutput_table)) * S ((dst_positive_code_sum_functional_secondsliceoutput_table) + (dst_positive_scale_sum_functional_secondsliceoutput_table)) + ((dst_positive_scale_sum_functional_secondsliceoutput_table) + (dst_positive_scale_sum_functional_secondsliceoutput_table))) + (((dst_negative_code_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)) * S ((dst_negative_code_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)) + ((dst_negative_scale_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)))) * S ((((dst_positive_code_sum_functional_secondsliceoutput_table) + (dst_positive_scale_sum_functional_secondsliceoutput_table)) * S ((dst_positive_code_sum_functional_secondsliceoutput_table) + (dst_positive_scale_sum_functional_secondsliceoutput_table)) + ((dst_positive_scale_sum_functional_secondsliceoutput_table) + (dst_positive_scale_sum_functional_secondsliceoutput_table))) + (((dst_negative_code_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)) * S ((dst_negative_code_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)) + ((dst_negative_scale_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)))) + ((((dst_negative_code_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)) * S ((dst_negative_code_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)) + ((dst_negative_scale_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table))) + (((dst_negative_code_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)) * S ((dst_negative_code_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)) + ((dst_negative_scale_sum_functional_secondsliceoutput_table) + (dst_negative_scale_sum_functional_secondsliceoutput_table)))))) /\ (forall dst_index_sum_functional_secondsliceoutput_table. (exists pvs_le_gap_sum_functional_secondsliceoutput_tabledomain. pvs_le_gap_sum_functional_secondsliceoutput_tabledomain + (dst_index_sum_functional_secondsliceoutput_table) = (l)) -> exists dst_positive_sum_functional_secondsliceoutput_table dst_negative_sum_functional_secondsliceoutput_table dst_value_sum_functional_secondsliceoutput_table. ((((exists ff_h_pvs_sum_functional_secondsliceoutput_tableentrypositive. ff_h_pvs_sum_functional_secondsliceoutput_tableentrypositive + S (dst_positive_sum_functional_secondsliceoutput_table) = S ((S (dst_index_sum_functional_secondsliceoutput_table)) * dst_positive_scale_sum_functional_secondsliceoutput_table)) /\ exists ff_q_pvs_sum_functional_secondsliceoutput_tableentrypositive. dst_positive_code_sum_functional_secondsliceoutput_table = ff_q_pvs_sum_functional_secondsliceoutput_tableentrypositive * S ((S (dst_index_sum_functional_secondsliceoutput_table)) * dst_positive_scale_sum_functional_secondsliceoutput_table) + (dst_positive_sum_functional_secondsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_functional_secondsliceoutput_tableentrynegative. ff_h_pvs_sum_functional_secondsliceoutput_tableentrynegative + S (dst_negative_sum_functional_secondsliceoutput_table) = S ((S (dst_index_sum_functional_secondsliceoutput_table)) * dst_negative_scale_sum_functional_secondsliceoutput_table)) /\ exists ff_q_pvs_sum_functional_secondsliceoutput_tableentrynegative. dst_negative_code_sum_functional_secondsliceoutput_table = ff_q_pvs_sum_functional_secondsliceoutput_tableentrynegative * S ((S (dst_index_sum_functional_secondsliceoutput_table)) * dst_negative_scale_sum_functional_secondsliceoutput_table) + (dst_negative_sum_functional_secondsliceoutput_table))) /\ (exists ge_balance_positive_sum_functional_secondsliceoutput_tableentryvalue ge_balance_negative_sum_functional_secondsliceoutput_tableentryvalue. (((((dst_value_sum_functional_secondsliceoutput_table) = 2 * (ge_balance_positive_sum_functional_secondsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_functional_secondsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_secondsliceoutput_tableentryvaluedecode. (((dst_value_sum_functional_secondsliceoutput_table) = 2 * ge_signed_half_sum_functional_secondsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_secondsliceoutput_tableentryvalue) = S ge_signed_half_sum_functional_secondsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_secondsliceoutput_table) + ge_balance_negative_sum_functional_secondsliceoutput_tableentryvalue = (dst_negative_sum_functional_secondsliceoutput_table) + ge_balance_positive_sum_functional_secondsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_functional_secondslice. (exists pvs_gap_sum_functional_secondslicebound. pvs_gap_sum_functional_secondslicebound + S (srs_index_sum_functional_secondslice) = (l)) -> exists srs_value_sum_functional_secondslice. (((exists dst_positive_code_sum_functional_secondsliceentrysource dst_positive_scale_sum_functional_secondsliceentrysource dst_negative_code_sum_functional_secondsliceentrysource dst_negative_scale_sum_functional_secondsliceentrysource dst_positive_sum_functional_secondsliceentrysource dst_negative_sum_functional_secondsliceentrysource. (((F) = (((((dst_positive_code_sum_functional_secondsliceentrysource) + (dst_positive_scale_sum_functional_secondsliceentrysource)) * S ((dst_positive_code_sum_functional_secondsliceentrysource) + (dst_positive_scale_sum_functional_secondsliceentrysource)) + ((dst_positive_scale_sum_functional_secondsliceentrysource) + (dst_positive_scale_sum_functional_secondsliceentrysource))) + (((dst_negative_code_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)) * S ((dst_negative_code_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)) + ((dst_negative_scale_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)))) * S ((((dst_positive_code_sum_functional_secondsliceentrysource) + (dst_positive_scale_sum_functional_secondsliceentrysource)) * S ((dst_positive_code_sum_functional_secondsliceentrysource) + (dst_positive_scale_sum_functional_secondsliceentrysource)) + ((dst_positive_scale_sum_functional_secondsliceentrysource) + (dst_positive_scale_sum_functional_secondsliceentrysource))) + (((dst_negative_code_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)) * S ((dst_negative_code_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)) + ((dst_negative_scale_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)))) + ((((dst_negative_code_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)) * S ((dst_negative_code_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)) + ((dst_negative_scale_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource))) + (((dst_negative_code_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)) * S ((dst_negative_code_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)) + ((dst_negative_scale_sum_functional_secondsliceentrysource) + (dst_negative_scale_sum_functional_secondsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_functional_secondsliceentrysourcepositive. ff_h_pvs_sum_functional_secondsliceentrysourcepositive + S (dst_positive_sum_functional_secondsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_functional_secondslice))))) * dst_positive_scale_sum_functional_secondsliceentrysource)) /\ exists ff_q_pvs_sum_functional_secondsliceentrysourcepositive. dst_positive_code_sum_functional_secondsliceentrysource = ff_q_pvs_sum_functional_secondsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_functional_secondslice))))) * dst_positive_scale_sum_functional_secondsliceentrysource) + (dst_positive_sum_functional_secondsliceentrysource))) /\ (((((exists ff_h_pvs_sum_functional_secondsliceentrysourcenegative. ff_h_pvs_sum_functional_secondsliceentrysourcenegative + S (dst_negative_sum_functional_secondsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_functional_secondslice))))) * dst_negative_scale_sum_functional_secondsliceentrysource)) /\ exists ff_q_pvs_sum_functional_secondsliceentrysourcenegative. dst_negative_code_sum_functional_secondsliceentrysource = ff_q_pvs_sum_functional_secondsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_functional_secondslice))))) * dst_negative_scale_sum_functional_secondsliceentrysource) + (dst_negative_sum_functional_secondsliceentrysource))) /\ (exists ge_balance_positive_sum_functional_secondsliceentrysourcevalue ge_balance_negative_sum_functional_secondsliceentrysourcevalue. (((((srs_value_sum_functional_secondslice) = 2 * (ge_balance_positive_sum_functional_secondsliceentrysourcevalue) /\ (ge_balance_negative_sum_functional_secondsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_functional_secondsliceentrysourcevaluedecode. (((srs_value_sum_functional_secondslice) = 2 * ge_signed_half_sum_functional_secondsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_functional_secondsliceentrysourcevalue) = S ge_signed_half_sum_functional_secondsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_functional_secondsliceentrysource) + ge_balance_negative_sum_functional_secondsliceentrysourcevalue = (dst_negative_sum_functional_secondsliceentrysource) + ge_balance_positive_sum_functional_secondsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_functional_secondsliceentryoutput dst_positive_scale_sum_functional_secondsliceentryoutput dst_negative_code_sum_functional_secondsliceentryoutput dst_negative_scale_sum_functional_secondsliceentryoutput dst_positive_sum_functional_secondsliceentryoutput dst_negative_sum_functional_secondsliceentryoutput. (((srs_slice_sum_functional_second) = (((((dst_positive_code_sum_functional_secondsliceentryoutput) + (dst_positive_scale_sum_functional_secondsliceentryoutput)) * S ((dst_positive_code_sum_functional_secondsliceentryoutput) + (dst_positive_scale_sum_functional_secondsliceentryoutput)) + ((dst_positive_scale_sum_functional_secondsliceentryoutput) + (dst_positive_scale_sum_functional_secondsliceentryoutput))) + (((dst_negative_code_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)) * S ((dst_negative_code_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)) + ((dst_negative_scale_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)))) * S ((((dst_positive_code_sum_functional_secondsliceentryoutput) + (dst_positive_scale_sum_functional_secondsliceentryoutput)) * S ((dst_positive_code_sum_functional_secondsliceentryoutput) + (dst_positive_scale_sum_functional_secondsliceentryoutput)) + ((dst_positive_scale_sum_functional_secondsliceentryoutput) + (dst_positive_scale_sum_functional_secondsliceentryoutput))) + (((dst_negative_code_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)) * S ((dst_negative_code_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)) + ((dst_negative_scale_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)))) + ((((dst_negative_code_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)) * S ((dst_negative_code_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)) + ((dst_negative_scale_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput))) + (((dst_negative_code_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)) * S ((dst_negative_code_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)) + ((dst_negative_scale_sum_functional_secondsliceentryoutput) + (dst_negative_scale_sum_functional_secondsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_functional_secondsliceentryoutputpositive. ff_h_pvs_sum_functional_secondsliceentryoutputpositive + S (dst_positive_sum_functional_secondsliceentryoutput) = S ((S (srs_index_sum_functional_secondslice)) * dst_positive_scale_sum_functional_secondsliceentryoutput)) /\ exists ff_q_pvs_sum_functional_secondsliceentryoutputpositive. dst_positive_code_sum_functional_secondsliceentryoutput = ff_q_pvs_sum_functional_secondsliceentryoutputpositive * S ((S (srs_index_sum_functional_secondslice)) * dst_positive_scale_sum_functional_secondsliceentryoutput) + (dst_positive_sum_functional_secondsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_functional_secondsliceentryoutputnegative. ff_h_pvs_sum_functional_secondsliceentryoutputnegative + S (dst_negative_sum_functional_secondsliceentryoutput) = S ((S (srs_index_sum_functional_secondslice)) * dst_negative_scale_sum_functional_secondsliceentryoutput)) /\ exists ff_q_pvs_sum_functional_secondsliceentryoutputnegative. dst_negative_code_sum_functional_secondsliceentryoutput = ff_q_pvs_sum_functional_secondsliceentryoutputnegative * S ((S (srs_index_sum_functional_secondslice)) * dst_negative_scale_sum_functional_secondsliceentryoutput) + (dst_negative_sum_functional_secondsliceentryoutput))) /\ (exists ge_balance_positive_sum_functional_secondsliceentryoutputvalue ge_balance_negative_sum_functional_secondsliceentryoutputvalue. (((((srs_value_sum_functional_secondslice) = 2 * (ge_balance_positive_sum_functional_secondsliceentryoutputvalue) /\ (ge_balance_negative_sum_functional_secondsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_functional_secondsliceentryoutputvaluedecode. (((srs_value_sum_functional_secondslice) = 2 * ge_signed_half_sum_functional_secondsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_functional_secondsliceentryoutputvalue) = S ge_signed_half_sum_functional_secondsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_functional_secondsliceentryoutput) + ge_balance_negative_sum_functional_secondsliceentryoutputvalue = (dst_negative_sum_functional_secondsliceentryoutput) + ge_balance_positive_sum_functional_secondsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_functional_secondsum dst_positive_scale_sum_functional_secondsum dst_negative_code_sum_functional_secondsum dst_negative_scale_sum_functional_secondsum dst_positive_sum_sum_functional_secondsum dst_negative_sum_sum_functional_secondsum. (((srs_slice_sum_functional_second) = (((((dst_positive_code_sum_functional_secondsum) + (dst_positive_scale_sum_functional_secondsum)) * S ((dst_positive_code_sum_functional_secondsum) + (dst_positive_scale_sum_functional_secondsum)) + ((dst_positive_scale_sum_functional_secondsum) + (dst_positive_scale_sum_functional_secondsum))) + (((dst_negative_code_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)) * S ((dst_negative_code_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)) + ((dst_negative_scale_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)))) * S ((((dst_positive_code_sum_functional_secondsum) + (dst_positive_scale_sum_functional_secondsum)) * S ((dst_positive_code_sum_functional_secondsum) + (dst_positive_scale_sum_functional_secondsum)) + ((dst_positive_scale_sum_functional_secondsum) + (dst_positive_scale_sum_functional_secondsum))) + (((dst_negative_code_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)) * S ((dst_negative_code_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)) + ((dst_negative_scale_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)))) + ((((dst_negative_code_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)) * S ((dst_negative_code_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)) + ((dst_negative_scale_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum))) + (((dst_negative_code_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)) * S ((dst_negative_code_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)) + ((dst_negative_scale_sum_functional_secondsum) + (dst_negative_scale_sum_functional_secondsum)))))) /\ (((exists fs_u_dst_sum_functional_secondsumpositive fs_v_dst_sum_functional_secondsumpositive. ((((exists fs_h_dst_sum_functional_secondsumpositive_body_start. fs_h_dst_sum_functional_secondsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_secondsumpositive)) /\ exists fs_q_dst_sum_functional_secondsumpositive_body_start. fs_u_dst_sum_functional_secondsumpositive = fs_q_dst_sum_functional_secondsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_functional_secondsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_functional_secondsumpositive_body_terminal. fs_h_dst_sum_functional_secondsumpositive_body_terminal + S (dst_positive_sum_sum_functional_secondsum) = S ((S (l)) * fs_v_dst_sum_functional_secondsumpositive)) /\ exists fs_q_dst_sum_functional_secondsumpositive_body_terminal. fs_u_dst_sum_functional_secondsumpositive = fs_q_dst_sum_functional_secondsumpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_functional_secondsumpositive) + (dst_positive_sum_sum_functional_secondsum))) /\ forall fs_i_dst_sum_functional_secondsumpositive_body_steps. (exists fs_lt_dst_sum_functional_secondsumpositive_body_steps_bound. fs_lt_dst_sum_functional_secondsumpositive_body_steps_bound + S fs_i_dst_sum_functional_secondsumpositive_body_steps = l) -> exists fs_a_dst_sum_functional_secondsumpositive_body_steps fs_r_dst_sum_functional_secondsumpositive_body_steps fs_s_dst_sum_functional_secondsumpositive_body_steps. ((((exists fs_h_dst_sum_functional_secondsumpositive_body_steps_summand. fs_h_dst_sum_functional_secondsumpositive_body_steps_summand + S (fs_a_dst_sum_functional_secondsumpositive_body_steps) = S ((S (fs_i_dst_sum_functional_secondsumpositive_body_steps)) * dst_positive_scale_sum_functional_secondsum)) /\ exists fs_q_dst_sum_functional_secondsumpositive_body_steps_summand. dst_positive_code_sum_functional_secondsum = fs_q_dst_sum_functional_secondsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_functional_secondsumpositive_body_steps)) * dst_positive_scale_sum_functional_secondsum) + (fs_a_dst_sum_functional_secondsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondsumpositive_body_steps_partial. fs_h_dst_sum_functional_secondsumpositive_body_steps_partial + S (fs_r_dst_sum_functional_secondsumpositive_body_steps) = S ((S (fs_i_dst_sum_functional_secondsumpositive_body_steps)) * fs_v_dst_sum_functional_secondsumpositive)) /\ exists fs_q_dst_sum_functional_secondsumpositive_body_steps_partial. fs_u_dst_sum_functional_secondsumpositive = fs_q_dst_sum_functional_secondsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_functional_secondsumpositive_body_steps)) * fs_v_dst_sum_functional_secondsumpositive) + (fs_r_dst_sum_functional_secondsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondsumpositive_body_steps_successor. fs_h_dst_sum_functional_secondsumpositive_body_steps_successor + S (fs_s_dst_sum_functional_secondsumpositive_body_steps) = S ((S (S fs_i_dst_sum_functional_secondsumpositive_body_steps)) * fs_v_dst_sum_functional_secondsumpositive)) /\ exists fs_q_dst_sum_functional_secondsumpositive_body_steps_successor. fs_u_dst_sum_functional_secondsumpositive = fs_q_dst_sum_functional_secondsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_functional_secondsumpositive_body_steps)) * fs_v_dst_sum_functional_secondsumpositive) + (fs_s_dst_sum_functional_secondsumpositive_body_steps))) /\ fs_s_dst_sum_functional_secondsumpositive_body_steps = fs_r_dst_sum_functional_secondsumpositive_body_steps + fs_a_dst_sum_functional_secondsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_functional_secondsumnegative fs_v_dst_sum_functional_secondsumnegative. ((((exists fs_h_dst_sum_functional_secondsumnegative_body_start. fs_h_dst_sum_functional_secondsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_secondsumnegative)) /\ exists fs_q_dst_sum_functional_secondsumnegative_body_start. fs_u_dst_sum_functional_secondsumnegative = fs_q_dst_sum_functional_secondsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_functional_secondsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_functional_secondsumnegative_body_terminal. fs_h_dst_sum_functional_secondsumnegative_body_terminal + S (dst_negative_sum_sum_functional_secondsum) = S ((S (l)) * fs_v_dst_sum_functional_secondsumnegative)) /\ exists fs_q_dst_sum_functional_secondsumnegative_body_terminal. fs_u_dst_sum_functional_secondsumnegative = fs_q_dst_sum_functional_secondsumnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_functional_secondsumnegative) + (dst_negative_sum_sum_functional_secondsum))) /\ forall fs_i_dst_sum_functional_secondsumnegative_body_steps. (exists fs_lt_dst_sum_functional_secondsumnegative_body_steps_bound. fs_lt_dst_sum_functional_secondsumnegative_body_steps_bound + S fs_i_dst_sum_functional_secondsumnegative_body_steps = l) -> exists fs_a_dst_sum_functional_secondsumnegative_body_steps fs_r_dst_sum_functional_secondsumnegative_body_steps fs_s_dst_sum_functional_secondsumnegative_body_steps. ((((exists fs_h_dst_sum_functional_secondsumnegative_body_steps_summand. fs_h_dst_sum_functional_secondsumnegative_body_steps_summand + S (fs_a_dst_sum_functional_secondsumnegative_body_steps) = S ((S (fs_i_dst_sum_functional_secondsumnegative_body_steps)) * dst_negative_scale_sum_functional_secondsum)) /\ exists fs_q_dst_sum_functional_secondsumnegative_body_steps_summand. dst_negative_code_sum_functional_secondsum = fs_q_dst_sum_functional_secondsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_functional_secondsumnegative_body_steps)) * dst_negative_scale_sum_functional_secondsum) + (fs_a_dst_sum_functional_secondsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondsumnegative_body_steps_partial. fs_h_dst_sum_functional_secondsumnegative_body_steps_partial + S (fs_r_dst_sum_functional_secondsumnegative_body_steps) = S ((S (fs_i_dst_sum_functional_secondsumnegative_body_steps)) * fs_v_dst_sum_functional_secondsumnegative)) /\ exists fs_q_dst_sum_functional_secondsumnegative_body_steps_partial. fs_u_dst_sum_functional_secondsumnegative = fs_q_dst_sum_functional_secondsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_functional_secondsumnegative_body_steps)) * fs_v_dst_sum_functional_secondsumnegative) + (fs_r_dst_sum_functional_secondsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondsumnegative_body_steps_successor. fs_h_dst_sum_functional_secondsumnegative_body_steps_successor + S (fs_s_dst_sum_functional_secondsumnegative_body_steps) = S ((S (S fs_i_dst_sum_functional_secondsumnegative_body_steps)) * fs_v_dst_sum_functional_secondsumnegative)) /\ exists fs_q_dst_sum_functional_secondsumnegative_body_steps_successor. fs_u_dst_sum_functional_secondsumnegative = fs_q_dst_sum_functional_secondsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_functional_secondsumnegative_body_steps)) * fs_v_dst_sum_functional_secondsumnegative) + (fs_s_dst_sum_functional_secondsumnegative_body_steps))) /\ fs_s_dst_sum_functional_secondsumnegative_body_steps = fs_r_dst_sum_functional_secondsumnegative_body_steps + fs_a_dst_sum_functional_secondsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_functional_secondsumresult ge_balance_negative_sum_functional_secondsumresult. (((((b) = 2 * (ge_balance_positive_sum_functional_secondsumresult) /\ (ge_balance_negative_sum_functional_secondsumresult) = 0) \/ exists ge_signed_half_sum_functional_secondsumresultdecode. (((b) = 2 * ge_signed_half_sum_functional_secondsumresultdecode + 1 /\ (ge_balance_positive_sum_functional_secondsumresult) = 0) /\ (ge_balance_negative_sum_functional_secondsumresult) = S ge_signed_half_sum_functional_secondsumresultdecode))) /\ ((dst_positive_sum_sum_functional_secondsum) + ge_balance_negative_sum_functional_secondsumresult = (dst_negative_sum_sum_functional_secondsum) + ge_balance_positive_sum_functional_secondsumresult))))))))))) -> a=b