signed_rectangular_slice_sum_empty_value

Exact expanded first-order arithmetic statement

forall F o s z. (exists srs_slice_sum_empty_input. ((((exists dst_positive_code_sum_empty_inputslicesource_table dst_positive_scale_sum_empty_inputslicesource_table dst_negative_code_sum_empty_inputslicesource_table dst_negative_scale_sum_empty_inputslicesource_table. (((F) = (((((dst_positive_code_sum_empty_inputslicesource_table) + (dst_positive_scale_sum_empty_inputslicesource_table)) * S ((dst_positive_code_sum_empty_inputslicesource_table) + (dst_positive_scale_sum_empty_inputslicesource_table)) + ((dst_positive_scale_sum_empty_inputslicesource_table) + (dst_positive_scale_sum_empty_inputslicesource_table))) + (((dst_negative_code_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)) * S ((dst_negative_code_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)) + ((dst_negative_scale_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)))) * S ((((dst_positive_code_sum_empty_inputslicesource_table) + (dst_positive_scale_sum_empty_inputslicesource_table)) * S ((dst_positive_code_sum_empty_inputslicesource_table) + (dst_positive_scale_sum_empty_inputslicesource_table)) + ((dst_positive_scale_sum_empty_inputslicesource_table) + (dst_positive_scale_sum_empty_inputslicesource_table))) + (((dst_negative_code_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)) * S ((dst_negative_code_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)) + ((dst_negative_scale_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)))) + ((((dst_negative_code_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)) * S ((dst_negative_code_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)) + ((dst_negative_scale_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table))) + (((dst_negative_code_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)) * S ((dst_negative_code_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)) + ((dst_negative_scale_sum_empty_inputslicesource_table) + (dst_negative_scale_sum_empty_inputslicesource_table)))))) /\ (forall dst_index_sum_empty_inputslicesource_table. (exists pvs_le_gap_sum_empty_inputslicesource_tabledomain. pvs_le_gap_sum_empty_inputslicesource_tabledomain + (dst_index_sum_empty_inputslicesource_table) = (0)) -> exists dst_positive_sum_empty_inputslicesource_table dst_negative_sum_empty_inputslicesource_table dst_value_sum_empty_inputslicesource_table. ((((exists ff_h_pvs_sum_empty_inputslicesource_tableentrypositive. ff_h_pvs_sum_empty_inputslicesource_tableentrypositive + S (dst_positive_sum_empty_inputslicesource_table) = S ((S (dst_index_sum_empty_inputslicesource_table)) * dst_positive_scale_sum_empty_inputslicesource_table)) /\ exists ff_q_pvs_sum_empty_inputslicesource_tableentrypositive. dst_positive_code_sum_empty_inputslicesource_table = ff_q_pvs_sum_empty_inputslicesource_tableentrypositive * S ((S (dst_index_sum_empty_inputslicesource_table)) * dst_positive_scale_sum_empty_inputslicesource_table) + (dst_positive_sum_empty_inputslicesource_table))) /\ (((((exists ff_h_pvs_sum_empty_inputslicesource_tableentrynegative. ff_h_pvs_sum_empty_inputslicesource_tableentrynegative + S (dst_negative_sum_empty_inputslicesource_table) = S ((S (dst_index_sum_empty_inputslicesource_table)) * dst_negative_scale_sum_empty_inputslicesource_table)) /\ exists ff_q_pvs_sum_empty_inputslicesource_tableentrynegative. dst_negative_code_sum_empty_inputslicesource_table = ff_q_pvs_sum_empty_inputslicesource_tableentrynegative * S ((S (dst_index_sum_empty_inputslicesource_table)) * dst_negative_scale_sum_empty_inputslicesource_table) + (dst_negative_sum_empty_inputslicesource_table))) /\ (exists ge_balance_positive_sum_empty_inputslicesource_tableentryvalue ge_balance_negative_sum_empty_inputslicesource_tableentryvalue. (((((dst_value_sum_empty_inputslicesource_table) = 2 * (ge_balance_positive_sum_empty_inputslicesource_tableentryvalue) /\ (ge_balance_negative_sum_empty_inputslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_empty_inputslicesource_tableentryvaluedecode. (((dst_value_sum_empty_inputslicesource_table) = 2 * ge_signed_half_sum_empty_inputslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_empty_inputslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_empty_inputslicesource_tableentryvalue) = S ge_signed_half_sum_empty_inputslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_empty_inputslicesource_table) + ge_balance_negative_sum_empty_inputslicesource_tableentryvalue = (dst_negative_sum_empty_inputslicesource_table) + ge_balance_positive_sum_empty_inputslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_empty_inputsliceoutput_table dst_positive_scale_sum_empty_inputsliceoutput_table dst_negative_code_sum_empty_inputsliceoutput_table dst_negative_scale_sum_empty_inputsliceoutput_table. (((srs_slice_sum_empty_input) = (((((dst_positive_code_sum_empty_inputsliceoutput_table) + (dst_positive_scale_sum_empty_inputsliceoutput_table)) * S ((dst_positive_code_sum_empty_inputsliceoutput_table) + (dst_positive_scale_sum_empty_inputsliceoutput_table)) + ((dst_positive_scale_sum_empty_inputsliceoutput_table) + (dst_positive_scale_sum_empty_inputsliceoutput_table))) + (((dst_negative_code_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)) * S ((dst_negative_code_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)) + ((dst_negative_scale_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)))) * S ((((dst_positive_code_sum_empty_inputsliceoutput_table) + (dst_positive_scale_sum_empty_inputsliceoutput_table)) * S ((dst_positive_code_sum_empty_inputsliceoutput_table) + (dst_positive_scale_sum_empty_inputsliceoutput_table)) + ((dst_positive_scale_sum_empty_inputsliceoutput_table) + (dst_positive_scale_sum_empty_inputsliceoutput_table))) + (((dst_negative_code_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)) * S ((dst_negative_code_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)) + ((dst_negative_scale_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)))) + ((((dst_negative_code_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)) * S ((dst_negative_code_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)) + ((dst_negative_scale_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table))) + (((dst_negative_code_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)) * S ((dst_negative_code_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)) + ((dst_negative_scale_sum_empty_inputsliceoutput_table) + (dst_negative_scale_sum_empty_inputsliceoutput_table)))))) /\ (forall dst_index_sum_empty_inputsliceoutput_table. (exists pvs_le_gap_sum_empty_inputsliceoutput_tabledomain. pvs_le_gap_sum_empty_inputsliceoutput_tabledomain + (dst_index_sum_empty_inputsliceoutput_table) = (0)) -> exists dst_positive_sum_empty_inputsliceoutput_table dst_negative_sum_empty_inputsliceoutput_table dst_value_sum_empty_inputsliceoutput_table. ((((exists ff_h_pvs_sum_empty_inputsliceoutput_tableentrypositive. ff_h_pvs_sum_empty_inputsliceoutput_tableentrypositive + S (dst_positive_sum_empty_inputsliceoutput_table) = S ((S (dst_index_sum_empty_inputsliceoutput_table)) * dst_positive_scale_sum_empty_inputsliceoutput_table)) /\ exists ff_q_pvs_sum_empty_inputsliceoutput_tableentrypositive. dst_positive_code_sum_empty_inputsliceoutput_table = ff_q_pvs_sum_empty_inputsliceoutput_tableentrypositive * S ((S (dst_index_sum_empty_inputsliceoutput_table)) * dst_positive_scale_sum_empty_inputsliceoutput_table) + (dst_positive_sum_empty_inputsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_empty_inputsliceoutput_tableentrynegative. ff_h_pvs_sum_empty_inputsliceoutput_tableentrynegative + S (dst_negative_sum_empty_inputsliceoutput_table) = S ((S (dst_index_sum_empty_inputsliceoutput_table)) * dst_negative_scale_sum_empty_inputsliceoutput_table)) /\ exists ff_q_pvs_sum_empty_inputsliceoutput_tableentrynegative. dst_negative_code_sum_empty_inputsliceoutput_table = ff_q_pvs_sum_empty_inputsliceoutput_tableentrynegative * S ((S (dst_index_sum_empty_inputsliceoutput_table)) * dst_negative_scale_sum_empty_inputsliceoutput_table) + (dst_negative_sum_empty_inputsliceoutput_table))) /\ (exists ge_balance_positive_sum_empty_inputsliceoutput_tableentryvalue ge_balance_negative_sum_empty_inputsliceoutput_tableentryvalue. (((((dst_value_sum_empty_inputsliceoutput_table) = 2 * (ge_balance_positive_sum_empty_inputsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_empty_inputsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_empty_inputsliceoutput_tableentryvaluedecode. (((dst_value_sum_empty_inputsliceoutput_table) = 2 * ge_signed_half_sum_empty_inputsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_empty_inputsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_empty_inputsliceoutput_tableentryvalue) = S ge_signed_half_sum_empty_inputsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_empty_inputsliceoutput_table) + ge_balance_negative_sum_empty_inputsliceoutput_tableentryvalue = (dst_negative_sum_empty_inputsliceoutput_table) + ge_balance_positive_sum_empty_inputsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_empty_inputslice. (exists pvs_gap_sum_empty_inputslicebound. pvs_gap_sum_empty_inputslicebound + S (srs_index_sum_empty_inputslice) = (0)) -> exists srs_value_sum_empty_inputslice. (((exists dst_positive_code_sum_empty_inputsliceentrysource dst_positive_scale_sum_empty_inputsliceentrysource dst_negative_code_sum_empty_inputsliceentrysource dst_negative_scale_sum_empty_inputsliceentrysource dst_positive_sum_empty_inputsliceentrysource dst_negative_sum_empty_inputsliceentrysource. (((F) = (((((dst_positive_code_sum_empty_inputsliceentrysource) + (dst_positive_scale_sum_empty_inputsliceentrysource)) * S ((dst_positive_code_sum_empty_inputsliceentrysource) + (dst_positive_scale_sum_empty_inputsliceentrysource)) + ((dst_positive_scale_sum_empty_inputsliceentrysource) + (dst_positive_scale_sum_empty_inputsliceentrysource))) + (((dst_negative_code_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)) * S ((dst_negative_code_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)) + ((dst_negative_scale_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)))) * S ((((dst_positive_code_sum_empty_inputsliceentrysource) + (dst_positive_scale_sum_empty_inputsliceentrysource)) * S ((dst_positive_code_sum_empty_inputsliceentrysource) + (dst_positive_scale_sum_empty_inputsliceentrysource)) + ((dst_positive_scale_sum_empty_inputsliceentrysource) + (dst_positive_scale_sum_empty_inputsliceentrysource))) + (((dst_negative_code_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)) * S ((dst_negative_code_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)) + ((dst_negative_scale_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)))) + ((((dst_negative_code_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)) * S ((dst_negative_code_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)) + ((dst_negative_scale_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource))) + (((dst_negative_code_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)) * S ((dst_negative_code_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)) + ((dst_negative_scale_sum_empty_inputsliceentrysource) + (dst_negative_scale_sum_empty_inputsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_empty_inputsliceentrysourcepositive. ff_h_pvs_sum_empty_inputsliceentrysourcepositive + S (dst_positive_sum_empty_inputsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_empty_inputslice))))) * dst_positive_scale_sum_empty_inputsliceentrysource)) /\ exists ff_q_pvs_sum_empty_inputsliceentrysourcepositive. dst_positive_code_sum_empty_inputsliceentrysource = ff_q_pvs_sum_empty_inputsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_empty_inputslice))))) * dst_positive_scale_sum_empty_inputsliceentrysource) + (dst_positive_sum_empty_inputsliceentrysource))) /\ (((((exists ff_h_pvs_sum_empty_inputsliceentrysourcenegative. ff_h_pvs_sum_empty_inputsliceentrysourcenegative + S (dst_negative_sum_empty_inputsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_empty_inputslice))))) * dst_negative_scale_sum_empty_inputsliceentrysource)) /\ exists ff_q_pvs_sum_empty_inputsliceentrysourcenegative. dst_negative_code_sum_empty_inputsliceentrysource = ff_q_pvs_sum_empty_inputsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_empty_inputslice))))) * dst_negative_scale_sum_empty_inputsliceentrysource) + (dst_negative_sum_empty_inputsliceentrysource))) /\ (exists ge_balance_positive_sum_empty_inputsliceentrysourcevalue ge_balance_negative_sum_empty_inputsliceentrysourcevalue. (((((srs_value_sum_empty_inputslice) = 2 * (ge_balance_positive_sum_empty_inputsliceentrysourcevalue) /\ (ge_balance_negative_sum_empty_inputsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_empty_inputsliceentrysourcevaluedecode. (((srs_value_sum_empty_inputslice) = 2 * ge_signed_half_sum_empty_inputsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_empty_inputsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_empty_inputsliceentrysourcevalue) = S ge_signed_half_sum_empty_inputsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_empty_inputsliceentrysource) + ge_balance_negative_sum_empty_inputsliceentrysourcevalue = (dst_negative_sum_empty_inputsliceentrysource) + ge_balance_positive_sum_empty_inputsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_empty_inputsliceentryoutput dst_positive_scale_sum_empty_inputsliceentryoutput dst_negative_code_sum_empty_inputsliceentryoutput dst_negative_scale_sum_empty_inputsliceentryoutput dst_positive_sum_empty_inputsliceentryoutput dst_negative_sum_empty_inputsliceentryoutput. (((srs_slice_sum_empty_input) = (((((dst_positive_code_sum_empty_inputsliceentryoutput) + (dst_positive_scale_sum_empty_inputsliceentryoutput)) * S ((dst_positive_code_sum_empty_inputsliceentryoutput) + (dst_positive_scale_sum_empty_inputsliceentryoutput)) + ((dst_positive_scale_sum_empty_inputsliceentryoutput) + (dst_positive_scale_sum_empty_inputsliceentryoutput))) + (((dst_negative_code_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)) * S ((dst_negative_code_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)) + ((dst_negative_scale_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)))) * S ((((dst_positive_code_sum_empty_inputsliceentryoutput) + (dst_positive_scale_sum_empty_inputsliceentryoutput)) * S ((dst_positive_code_sum_empty_inputsliceentryoutput) + (dst_positive_scale_sum_empty_inputsliceentryoutput)) + ((dst_positive_scale_sum_empty_inputsliceentryoutput) + (dst_positive_scale_sum_empty_inputsliceentryoutput))) + (((dst_negative_code_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)) * S ((dst_negative_code_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)) + ((dst_negative_scale_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)))) + ((((dst_negative_code_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)) * S ((dst_negative_code_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)) + ((dst_negative_scale_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput))) + (((dst_negative_code_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)) * S ((dst_negative_code_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)) + ((dst_negative_scale_sum_empty_inputsliceentryoutput) + (dst_negative_scale_sum_empty_inputsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_empty_inputsliceentryoutputpositive. ff_h_pvs_sum_empty_inputsliceentryoutputpositive + S (dst_positive_sum_empty_inputsliceentryoutput) = S ((S (srs_index_sum_empty_inputslice)) * dst_positive_scale_sum_empty_inputsliceentryoutput)) /\ exists ff_q_pvs_sum_empty_inputsliceentryoutputpositive. dst_positive_code_sum_empty_inputsliceentryoutput = ff_q_pvs_sum_empty_inputsliceentryoutputpositive * S ((S (srs_index_sum_empty_inputslice)) * dst_positive_scale_sum_empty_inputsliceentryoutput) + (dst_positive_sum_empty_inputsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_empty_inputsliceentryoutputnegative. ff_h_pvs_sum_empty_inputsliceentryoutputnegative + S (dst_negative_sum_empty_inputsliceentryoutput) = S ((S (srs_index_sum_empty_inputslice)) * dst_negative_scale_sum_empty_inputsliceentryoutput)) /\ exists ff_q_pvs_sum_empty_inputsliceentryoutputnegative. dst_negative_code_sum_empty_inputsliceentryoutput = ff_q_pvs_sum_empty_inputsliceentryoutputnegative * S ((S (srs_index_sum_empty_inputslice)) * dst_negative_scale_sum_empty_inputsliceentryoutput) + (dst_negative_sum_empty_inputsliceentryoutput))) /\ (exists ge_balance_positive_sum_empty_inputsliceentryoutputvalue ge_balance_negative_sum_empty_inputsliceentryoutputvalue. (((((srs_value_sum_empty_inputslice) = 2 * (ge_balance_positive_sum_empty_inputsliceentryoutputvalue) /\ (ge_balance_negative_sum_empty_inputsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_empty_inputsliceentryoutputvaluedecode. (((srs_value_sum_empty_inputslice) = 2 * ge_signed_half_sum_empty_inputsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_empty_inputsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_empty_inputsliceentryoutputvalue) = S ge_signed_half_sum_empty_inputsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_empty_inputsliceentryoutput) + ge_balance_negative_sum_empty_inputsliceentryoutputvalue = (dst_negative_sum_empty_inputsliceentryoutput) + ge_balance_positive_sum_empty_inputsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_empty_inputsum dst_positive_scale_sum_empty_inputsum dst_negative_code_sum_empty_inputsum dst_negative_scale_sum_empty_inputsum dst_positive_sum_sum_empty_inputsum dst_negative_sum_sum_empty_inputsum. (((srs_slice_sum_empty_input) = (((((dst_positive_code_sum_empty_inputsum) + (dst_positive_scale_sum_empty_inputsum)) * S ((dst_positive_code_sum_empty_inputsum) + (dst_positive_scale_sum_empty_inputsum)) + ((dst_positive_scale_sum_empty_inputsum) + (dst_positive_scale_sum_empty_inputsum))) + (((dst_negative_code_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)) * S ((dst_negative_code_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)) + ((dst_negative_scale_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)))) * S ((((dst_positive_code_sum_empty_inputsum) + (dst_positive_scale_sum_empty_inputsum)) * S ((dst_positive_code_sum_empty_inputsum) + (dst_positive_scale_sum_empty_inputsum)) + ((dst_positive_scale_sum_empty_inputsum) + (dst_positive_scale_sum_empty_inputsum))) + (((dst_negative_code_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)) * S ((dst_negative_code_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)) + ((dst_negative_scale_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)))) + ((((dst_negative_code_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)) * S ((dst_negative_code_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)) + ((dst_negative_scale_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum))) + (((dst_negative_code_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)) * S ((dst_negative_code_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)) + ((dst_negative_scale_sum_empty_inputsum) + (dst_negative_scale_sum_empty_inputsum)))))) /\ (((exists fs_u_dst_sum_empty_inputsumpositive fs_v_dst_sum_empty_inputsumpositive. ((((exists fs_h_dst_sum_empty_inputsumpositive_body_start. fs_h_dst_sum_empty_inputsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_empty_inputsumpositive)) /\ exists fs_q_dst_sum_empty_inputsumpositive_body_start. fs_u_dst_sum_empty_inputsumpositive = fs_q_dst_sum_empty_inputsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_empty_inputsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_empty_inputsumpositive_body_terminal. fs_h_dst_sum_empty_inputsumpositive_body_terminal + S (dst_positive_sum_sum_empty_inputsum) = S ((S (0)) * fs_v_dst_sum_empty_inputsumpositive)) /\ exists fs_q_dst_sum_empty_inputsumpositive_body_terminal. fs_u_dst_sum_empty_inputsumpositive = fs_q_dst_sum_empty_inputsumpositive_body_terminal * S ((S (0)) * fs_v_dst_sum_empty_inputsumpositive) + (dst_positive_sum_sum_empty_inputsum))) /\ forall fs_i_dst_sum_empty_inputsumpositive_body_steps. (exists fs_lt_dst_sum_empty_inputsumpositive_body_steps_bound. fs_lt_dst_sum_empty_inputsumpositive_body_steps_bound + S fs_i_dst_sum_empty_inputsumpositive_body_steps = 0) -> exists fs_a_dst_sum_empty_inputsumpositive_body_steps fs_r_dst_sum_empty_inputsumpositive_body_steps fs_s_dst_sum_empty_inputsumpositive_body_steps. ((((exists fs_h_dst_sum_empty_inputsumpositive_body_steps_summand. fs_h_dst_sum_empty_inputsumpositive_body_steps_summand + S (fs_a_dst_sum_empty_inputsumpositive_body_steps) = S ((S (fs_i_dst_sum_empty_inputsumpositive_body_steps)) * dst_positive_scale_sum_empty_inputsum)) /\ exists fs_q_dst_sum_empty_inputsumpositive_body_steps_summand. dst_positive_code_sum_empty_inputsum = fs_q_dst_sum_empty_inputsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_empty_inputsumpositive_body_steps)) * dst_positive_scale_sum_empty_inputsum) + (fs_a_dst_sum_empty_inputsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_empty_inputsumpositive_body_steps_partial. fs_h_dst_sum_empty_inputsumpositive_body_steps_partial + S (fs_r_dst_sum_empty_inputsumpositive_body_steps) = S ((S (fs_i_dst_sum_empty_inputsumpositive_body_steps)) * fs_v_dst_sum_empty_inputsumpositive)) /\ exists fs_q_dst_sum_empty_inputsumpositive_body_steps_partial. fs_u_dst_sum_empty_inputsumpositive = fs_q_dst_sum_empty_inputsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_empty_inputsumpositive_body_steps)) * fs_v_dst_sum_empty_inputsumpositive) + (fs_r_dst_sum_empty_inputsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_empty_inputsumpositive_body_steps_successor. fs_h_dst_sum_empty_inputsumpositive_body_steps_successor + S (fs_s_dst_sum_empty_inputsumpositive_body_steps) = S ((S (S fs_i_dst_sum_empty_inputsumpositive_body_steps)) * fs_v_dst_sum_empty_inputsumpositive)) /\ exists fs_q_dst_sum_empty_inputsumpositive_body_steps_successor. fs_u_dst_sum_empty_inputsumpositive = fs_q_dst_sum_empty_inputsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_empty_inputsumpositive_body_steps)) * fs_v_dst_sum_empty_inputsumpositive) + (fs_s_dst_sum_empty_inputsumpositive_body_steps))) /\ fs_s_dst_sum_empty_inputsumpositive_body_steps = fs_r_dst_sum_empty_inputsumpositive_body_steps + fs_a_dst_sum_empty_inputsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_empty_inputsumnegative fs_v_dst_sum_empty_inputsumnegative. ((((exists fs_h_dst_sum_empty_inputsumnegative_body_start. fs_h_dst_sum_empty_inputsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_empty_inputsumnegative)) /\ exists fs_q_dst_sum_empty_inputsumnegative_body_start. fs_u_dst_sum_empty_inputsumnegative = fs_q_dst_sum_empty_inputsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_empty_inputsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_empty_inputsumnegative_body_terminal. fs_h_dst_sum_empty_inputsumnegative_body_terminal + S (dst_negative_sum_sum_empty_inputsum) = S ((S (0)) * fs_v_dst_sum_empty_inputsumnegative)) /\ exists fs_q_dst_sum_empty_inputsumnegative_body_terminal. fs_u_dst_sum_empty_inputsumnegative = fs_q_dst_sum_empty_inputsumnegative_body_terminal * S ((S (0)) * fs_v_dst_sum_empty_inputsumnegative) + (dst_negative_sum_sum_empty_inputsum))) /\ forall fs_i_dst_sum_empty_inputsumnegative_body_steps. (exists fs_lt_dst_sum_empty_inputsumnegative_body_steps_bound. fs_lt_dst_sum_empty_inputsumnegative_body_steps_bound + S fs_i_dst_sum_empty_inputsumnegative_body_steps = 0) -> exists fs_a_dst_sum_empty_inputsumnegative_body_steps fs_r_dst_sum_empty_inputsumnegative_body_steps fs_s_dst_sum_empty_inputsumnegative_body_steps. ((((exists fs_h_dst_sum_empty_inputsumnegative_body_steps_summand. fs_h_dst_sum_empty_inputsumnegative_body_steps_summand + S (fs_a_dst_sum_empty_inputsumnegative_body_steps) = S ((S (fs_i_dst_sum_empty_inputsumnegative_body_steps)) * dst_negative_scale_sum_empty_inputsum)) /\ exists fs_q_dst_sum_empty_inputsumnegative_body_steps_summand. dst_negative_code_sum_empty_inputsum = fs_q_dst_sum_empty_inputsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_empty_inputsumnegative_body_steps)) * dst_negative_scale_sum_empty_inputsum) + (fs_a_dst_sum_empty_inputsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_empty_inputsumnegative_body_steps_partial. fs_h_dst_sum_empty_inputsumnegative_body_steps_partial + S (fs_r_dst_sum_empty_inputsumnegative_body_steps) = S ((S (fs_i_dst_sum_empty_inputsumnegative_body_steps)) * fs_v_dst_sum_empty_inputsumnegative)) /\ exists fs_q_dst_sum_empty_inputsumnegative_body_steps_partial. fs_u_dst_sum_empty_inputsumnegative = fs_q_dst_sum_empty_inputsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_empty_inputsumnegative_body_steps)) * fs_v_dst_sum_empty_inputsumnegative) + (fs_r_dst_sum_empty_inputsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_empty_inputsumnegative_body_steps_successor. fs_h_dst_sum_empty_inputsumnegative_body_steps_successor + S (fs_s_dst_sum_empty_inputsumnegative_body_steps) = S ((S (S fs_i_dst_sum_empty_inputsumnegative_body_steps)) * fs_v_dst_sum_empty_inputsumnegative)) /\ exists fs_q_dst_sum_empty_inputsumnegative_body_steps_successor. fs_u_dst_sum_empty_inputsumnegative = fs_q_dst_sum_empty_inputsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_empty_inputsumnegative_body_steps)) * fs_v_dst_sum_empty_inputsumnegative) + (fs_s_dst_sum_empty_inputsumnegative_body_steps))) /\ fs_s_dst_sum_empty_inputsumnegative_body_steps = fs_r_dst_sum_empty_inputsumnegative_body_steps + fs_a_dst_sum_empty_inputsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_empty_inputsumresult ge_balance_negative_sum_empty_inputsumresult. (((((z) = 2 * (ge_balance_positive_sum_empty_inputsumresult) /\ (ge_balance_negative_sum_empty_inputsumresult) = 0) \/ exists ge_signed_half_sum_empty_inputsumresultdecode. (((z) = 2 * ge_signed_half_sum_empty_inputsumresultdecode + 1 /\ (ge_balance_positive_sum_empty_inputsumresult) = 0) /\ (ge_balance_negative_sum_empty_inputsumresult) = S ge_signed_half_sum_empty_inputsumresultdecode))) /\ ((dst_positive_sum_sum_empty_inputsum) + ge_balance_negative_sum_empty_inputsumresult = (dst_negative_sum_sum_empty_inputsum) + ge_balance_positive_sum_empty_inputsumresult))))))))))) -> z=0