signed_rectangular_sum_zero_outer

Exact expanded first-order arithmetic statement

forall F o s t n z. (exists srt_rows_zero_outer_input. ((((exists dst_positive_code_zero_outer_inputrowssource_table dst_positive_scale_zero_outer_inputrowssource_table dst_negative_code_zero_outer_inputrowssource_table dst_negative_scale_zero_outer_inputrowssource_table. (((F) = (((((dst_positive_code_zero_outer_inputrowssource_table) + (dst_positive_scale_zero_outer_inputrowssource_table)) * S ((dst_positive_code_zero_outer_inputrowssource_table) + (dst_positive_scale_zero_outer_inputrowssource_table)) + ((dst_positive_scale_zero_outer_inputrowssource_table) + (dst_positive_scale_zero_outer_inputrowssource_table))) + (((dst_negative_code_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)) * S ((dst_negative_code_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)) + ((dst_negative_scale_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)))) * S ((((dst_positive_code_zero_outer_inputrowssource_table) + (dst_positive_scale_zero_outer_inputrowssource_table)) * S ((dst_positive_code_zero_outer_inputrowssource_table) + (dst_positive_scale_zero_outer_inputrowssource_table)) + ((dst_positive_scale_zero_outer_inputrowssource_table) + (dst_positive_scale_zero_outer_inputrowssource_table))) + (((dst_negative_code_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)) * S ((dst_negative_code_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)) + ((dst_negative_scale_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)))) + ((((dst_negative_code_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)) * S ((dst_negative_code_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)) + ((dst_negative_scale_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table))) + (((dst_negative_code_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)) * S ((dst_negative_code_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)) + ((dst_negative_scale_zero_outer_inputrowssource_table) + (dst_negative_scale_zero_outer_inputrowssource_table)))))) /\ (forall dst_index_zero_outer_inputrowssource_table. (exists pvs_le_gap_zero_outer_inputrowssource_tabledomain. pvs_le_gap_zero_outer_inputrowssource_tabledomain + (dst_index_zero_outer_inputrowssource_table) = (0)) -> exists dst_positive_zero_outer_inputrowssource_table dst_negative_zero_outer_inputrowssource_table dst_value_zero_outer_inputrowssource_table. ((((exists ff_h_pvs_zero_outer_inputrowssource_tableentrypositive. ff_h_pvs_zero_outer_inputrowssource_tableentrypositive + S (dst_positive_zero_outer_inputrowssource_table) = S ((S (dst_index_zero_outer_inputrowssource_table)) * dst_positive_scale_zero_outer_inputrowssource_table)) /\ exists ff_q_pvs_zero_outer_inputrowssource_tableentrypositive. dst_positive_code_zero_outer_inputrowssource_table = ff_q_pvs_zero_outer_inputrowssource_tableentrypositive * S ((S (dst_index_zero_outer_inputrowssource_table)) * dst_positive_scale_zero_outer_inputrowssource_table) + (dst_positive_zero_outer_inputrowssource_table))) /\ (((((exists ff_h_pvs_zero_outer_inputrowssource_tableentrynegative. ff_h_pvs_zero_outer_inputrowssource_tableentrynegative + S (dst_negative_zero_outer_inputrowssource_table) = S ((S (dst_index_zero_outer_inputrowssource_table)) * dst_negative_scale_zero_outer_inputrowssource_table)) /\ exists ff_q_pvs_zero_outer_inputrowssource_tableentrynegative. dst_negative_code_zero_outer_inputrowssource_table = ff_q_pvs_zero_outer_inputrowssource_tableentrynegative * S ((S (dst_index_zero_outer_inputrowssource_table)) * dst_negative_scale_zero_outer_inputrowssource_table) + (dst_negative_zero_outer_inputrowssource_table))) /\ (exists ge_balance_positive_zero_outer_inputrowssource_tableentryvalue ge_balance_negative_zero_outer_inputrowssource_tableentryvalue. (((((dst_value_zero_outer_inputrowssource_table) = 2 * (ge_balance_positive_zero_outer_inputrowssource_tableentryvalue) /\ (ge_balance_negative_zero_outer_inputrowssource_tableentryvalue) = 0) \/ exists ge_signed_half_zero_outer_inputrowssource_tableentryvaluedecode. (((dst_value_zero_outer_inputrowssource_table) = 2 * ge_signed_half_zero_outer_inputrowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_zero_outer_inputrowssource_tableentryvalue) = 0) /\ (ge_balance_negative_zero_outer_inputrowssource_tableentryvalue) = S ge_signed_half_zero_outer_inputrowssource_tableentryvaluedecode))) /\ ((dst_positive_zero_outer_inputrowssource_table) + ge_balance_negative_zero_outer_inputrowssource_tableentryvalue = (dst_negative_zero_outer_inputrowssource_table) + ge_balance_positive_zero_outer_inputrowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_zero_outer_inputrowsrow_table dst_positive_scale_zero_outer_inputrowsrow_table dst_negative_code_zero_outer_inputrowsrow_table dst_negative_scale_zero_outer_inputrowsrow_table. (((srt_rows_zero_outer_input) = (((((dst_positive_code_zero_outer_inputrowsrow_table) + (dst_positive_scale_zero_outer_inputrowsrow_table)) * S ((dst_positive_code_zero_outer_inputrowsrow_table) + (dst_positive_scale_zero_outer_inputrowsrow_table)) + ((dst_positive_scale_zero_outer_inputrowsrow_table) + (dst_positive_scale_zero_outer_inputrowsrow_table))) + (((dst_negative_code_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)) * S ((dst_negative_code_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)) + ((dst_negative_scale_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)))) * S ((((dst_positive_code_zero_outer_inputrowsrow_table) + (dst_positive_scale_zero_outer_inputrowsrow_table)) * S ((dst_positive_code_zero_outer_inputrowsrow_table) + (dst_positive_scale_zero_outer_inputrowsrow_table)) + ((dst_positive_scale_zero_outer_inputrowsrow_table) + (dst_positive_scale_zero_outer_inputrowsrow_table))) + (((dst_negative_code_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)) * S ((dst_negative_code_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)) + ((dst_negative_scale_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)))) + ((((dst_negative_code_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)) * S ((dst_negative_code_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)) + ((dst_negative_scale_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table))) + (((dst_negative_code_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)) * S ((dst_negative_code_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)) + ((dst_negative_scale_zero_outer_inputrowsrow_table) + (dst_negative_scale_zero_outer_inputrowsrow_table)))))) /\ (forall dst_index_zero_outer_inputrowsrow_table. (exists pvs_le_gap_zero_outer_inputrowsrow_tabledomain. pvs_le_gap_zero_outer_inputrowsrow_tabledomain + (dst_index_zero_outer_inputrowsrow_table) = (0)) -> exists dst_positive_zero_outer_inputrowsrow_table dst_negative_zero_outer_inputrowsrow_table dst_value_zero_outer_inputrowsrow_table. ((((exists ff_h_pvs_zero_outer_inputrowsrow_tableentrypositive. ff_h_pvs_zero_outer_inputrowsrow_tableentrypositive + S (dst_positive_zero_outer_inputrowsrow_table) = S ((S (dst_index_zero_outer_inputrowsrow_table)) * dst_positive_scale_zero_outer_inputrowsrow_table)) /\ exists ff_q_pvs_zero_outer_inputrowsrow_tableentrypositive. dst_positive_code_zero_outer_inputrowsrow_table = ff_q_pvs_zero_outer_inputrowsrow_tableentrypositive * S ((S (dst_index_zero_outer_inputrowsrow_table)) * dst_positive_scale_zero_outer_inputrowsrow_table) + (dst_positive_zero_outer_inputrowsrow_table))) /\ (((((exists ff_h_pvs_zero_outer_inputrowsrow_tableentrynegative. ff_h_pvs_zero_outer_inputrowsrow_tableentrynegative + S (dst_negative_zero_outer_inputrowsrow_table) = S ((S (dst_index_zero_outer_inputrowsrow_table)) * dst_negative_scale_zero_outer_inputrowsrow_table)) /\ exists ff_q_pvs_zero_outer_inputrowsrow_tableentrynegative. dst_negative_code_zero_outer_inputrowsrow_table = ff_q_pvs_zero_outer_inputrowsrow_tableentrynegative * S ((S (dst_index_zero_outer_inputrowsrow_table)) * dst_negative_scale_zero_outer_inputrowsrow_table) + (dst_negative_zero_outer_inputrowsrow_table))) /\ (exists ge_balance_positive_zero_outer_inputrowsrow_tableentryvalue ge_balance_negative_zero_outer_inputrowsrow_tableentryvalue. (((((dst_value_zero_outer_inputrowsrow_table) = 2 * (ge_balance_positive_zero_outer_inputrowsrow_tableentryvalue) /\ (ge_balance_negative_zero_outer_inputrowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_zero_outer_inputrowsrow_tableentryvaluedecode. (((dst_value_zero_outer_inputrowsrow_table) = 2 * ge_signed_half_zero_outer_inputrowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_zero_outer_inputrowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_zero_outer_inputrowsrow_tableentryvalue) = S ge_signed_half_zero_outer_inputrowsrow_tableentryvaluedecode))) /\ ((dst_positive_zero_outer_inputrowsrow_table) + ge_balance_negative_zero_outer_inputrowsrow_tableentryvalue = (dst_negative_zero_outer_inputrowsrow_table) + ge_balance_positive_zero_outer_inputrowsrow_tableentryvalue))))))))) /\ (forall srt_index_zero_outer_inputrows. (exists pvs_gap_zero_outer_inputrowsbound. pvs_gap_zero_outer_inputrowsbound + S (srt_index_zero_outer_inputrows) = (0)) -> exists srt_value_zero_outer_inputrows. (((exists dst_positive_code_zero_outer_inputrowsrowentry dst_positive_scale_zero_outer_inputrowsrowentry dst_negative_code_zero_outer_inputrowsrowentry dst_negative_scale_zero_outer_inputrowsrowentry dst_positive_zero_outer_inputrowsrowentry dst_negative_zero_outer_inputrowsrowentry. (((srt_rows_zero_outer_input) = (((((dst_positive_code_zero_outer_inputrowsrowentry) + (dst_positive_scale_zero_outer_inputrowsrowentry)) * S ((dst_positive_code_zero_outer_inputrowsrowentry) + (dst_positive_scale_zero_outer_inputrowsrowentry)) + ((dst_positive_scale_zero_outer_inputrowsrowentry) + (dst_positive_scale_zero_outer_inputrowsrowentry))) + (((dst_negative_code_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)) * S ((dst_negative_code_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)) + ((dst_negative_scale_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)))) * S ((((dst_positive_code_zero_outer_inputrowsrowentry) + (dst_positive_scale_zero_outer_inputrowsrowentry)) * S ((dst_positive_code_zero_outer_inputrowsrowentry) + (dst_positive_scale_zero_outer_inputrowsrowentry)) + ((dst_positive_scale_zero_outer_inputrowsrowentry) + (dst_positive_scale_zero_outer_inputrowsrowentry))) + (((dst_negative_code_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)) * S ((dst_negative_code_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)) + ((dst_negative_scale_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)))) + ((((dst_negative_code_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)) * S ((dst_negative_code_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)) + ((dst_negative_scale_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry))) + (((dst_negative_code_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)) * S ((dst_negative_code_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)) + ((dst_negative_scale_zero_outer_inputrowsrowentry) + (dst_negative_scale_zero_outer_inputrowsrowentry)))))) /\ (((((exists ff_h_pvs_zero_outer_inputrowsrowentrypositive. ff_h_pvs_zero_outer_inputrowsrowentrypositive + S (dst_positive_zero_outer_inputrowsrowentry) = S ((S (srt_index_zero_outer_inputrows)) * dst_positive_scale_zero_outer_inputrowsrowentry)) /\ exists ff_q_pvs_zero_outer_inputrowsrowentrypositive. dst_positive_code_zero_outer_inputrowsrowentry = ff_q_pvs_zero_outer_inputrowsrowentrypositive * S ((S (srt_index_zero_outer_inputrows)) * dst_positive_scale_zero_outer_inputrowsrowentry) + (dst_positive_zero_outer_inputrowsrowentry))) /\ (((((exists ff_h_pvs_zero_outer_inputrowsrowentrynegative. ff_h_pvs_zero_outer_inputrowsrowentrynegative + S (dst_negative_zero_outer_inputrowsrowentry) = S ((S (srt_index_zero_outer_inputrows)) * dst_negative_scale_zero_outer_inputrowsrowentry)) /\ exists ff_q_pvs_zero_outer_inputrowsrowentrynegative. dst_negative_code_zero_outer_inputrowsrowentry = ff_q_pvs_zero_outer_inputrowsrowentrynegative * S ((S (srt_index_zero_outer_inputrows)) * dst_negative_scale_zero_outer_inputrowsrowentry) + (dst_negative_zero_outer_inputrowsrowentry))) /\ (exists ge_balance_positive_zero_outer_inputrowsrowentryvalue ge_balance_negative_zero_outer_inputrowsrowentryvalue. (((((srt_value_zero_outer_inputrows) = 2 * (ge_balance_positive_zero_outer_inputrowsrowentryvalue) /\ (ge_balance_negative_zero_outer_inputrowsrowentryvalue) = 0) \/ exists ge_signed_half_zero_outer_inputrowsrowentryvaluedecode. (((srt_value_zero_outer_inputrows) = 2 * ge_signed_half_zero_outer_inputrowsrowentryvaluedecode + 1 /\ (ge_balance_positive_zero_outer_inputrowsrowentryvalue) = 0) /\ (ge_balance_negative_zero_outer_inputrowsrowentryvalue) = S ge_signed_half_zero_outer_inputrowsrowentryvaluedecode))) /\ ((dst_positive_zero_outer_inputrowsrowentry) + ge_balance_negative_zero_outer_inputrowsrowentryvalue = (dst_negative_zero_outer_inputrowsrowentry) + ge_balance_positive_zero_outer_inputrowsrowentryvalue))))))))) /\ (exists srs_slice_zero_outer_inputrowsrowrow_sum. ((((exists dst_positive_code_zero_outer_inputrowsrowrow_sumslicesource_table dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_zero_outer_inputrowsrowrow_sumslicesource_table. (exists pvs_le_gap_zero_outer_inputrowsrowrow_sumslicesource_tabledomain. pvs_le_gap_zero_outer_inputrowsrowrow_sumslicesource_tabledomain + (dst_index_zero_outer_inputrowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_zero_outer_inputrowsrowrow_sumslicesource_table dst_negative_zero_outer_inputrowsrowrow_sumslicesource_table dst_value_zero_outer_inputrowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_zero_outer_inputrowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_zero_outer_inputrowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_zero_outer_inputrowsrowrow_sumslicesource_table) = S ((S (dst_index_zero_outer_inputrowsrowrow_sumslicesource_table)) * dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_zero_outer_inputrowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_zero_outer_inputrowsrowrow_sumslicesource_table = ff_q_pvs_zero_outer_inputrowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_zero_outer_inputrowsrowrow_sumslicesource_table)) * dst_positive_scale_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_positive_zero_outer_inputrowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_zero_outer_inputrowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_zero_outer_inputrowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_zero_outer_inputrowsrowrow_sumslicesource_table) = S ((S (dst_index_zero_outer_inputrowsrowrow_sumslicesource_table)) * dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_zero_outer_inputrowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_zero_outer_inputrowsrowrow_sumslicesource_table = ff_q_pvs_zero_outer_inputrowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_zero_outer_inputrowsrowrow_sumslicesource_table)) * dst_negative_scale_zero_outer_inputrowsrowrow_sumslicesource_table) + (dst_negative_zero_outer_inputrowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_zero_outer_inputrowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_zero_outer_inputrowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_zero_outer_inputrowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_zero_outer_inputrowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_zero_outer_inputrowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_zero_outer_inputrowsrowrow_sumslicesource_table) = 2 * ge_signed_half_zero_outer_inputrowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_zero_outer_inputrowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_zero_outer_inputrowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_zero_outer_inputrowsrowrow_sumslicesource_table) + ge_balance_negative_zero_outer_inputrowsrowrow_sumslicesource_tableentryvalue = (dst_negative_zero_outer_inputrowsrowrow_sumslicesource_table) + ge_balance_positive_zero_outer_inputrowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_zero_outer_inputrowsrowrow_sumsliceoutput_table dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table. (((srs_slice_zero_outer_inputrowsrowrow_sum) = (((((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_zero_outer_inputrowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_zero_outer_inputrowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_zero_outer_inputrowsrowrow_sumsliceoutput_tabledomain + (dst_index_zero_outer_inputrowsrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_zero_outer_inputrowsrowrow_sumsliceoutput_table dst_negative_zero_outer_inputrowsrowrow_sumsliceoutput_table dst_value_zero_outer_inputrowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_zero_outer_inputrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_zero_outer_inputrowsrowrow_sumsliceoutput_table = ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_positive_zero_outer_inputrowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_zero_outer_inputrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_zero_outer_inputrowsrowrow_sumsliceoutput_table = ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_zero_outer_inputrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceoutput_table) + (dst_negative_zero_outer_inputrowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_zero_outer_inputrowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_zero_outer_inputrowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_zero_outer_inputrowsrowrow_sumsliceoutput_table) + ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_zero_outer_inputrowsrowrow_sumsliceoutput_table) + ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_zero_outer_inputrowsrowrow_sumslice. (exists pvs_gap_zero_outer_inputrowsrowrow_sumslicebound. pvs_gap_zero_outer_inputrowsrowrow_sumslicebound + S (srs_index_zero_outer_inputrowsrowrow_sumslice) = (n)) -> exists srs_value_zero_outer_inputrowsrowrow_sumslice. (((exists dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentrysource dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource dst_positive_zero_outer_inputrowsrowrow_sumsliceentrysource dst_negative_zero_outer_inputrowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceentrysourcepositive + S (dst_positive_zero_outer_inputrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_zero_outer_inputrows)))) + ((t) * (srs_index_zero_outer_inputrowsrowrow_sumslice))))) * dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceentrysourcepositive. dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentrysource = ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (srt_index_zero_outer_inputrows)))) + ((t) * (srs_index_zero_outer_inputrowsrowrow_sumslice))))) * dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_positive_zero_outer_inputrowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceentrysourcenegative + S (dst_negative_zero_outer_inputrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_zero_outer_inputrows)))) + ((t) * (srs_index_zero_outer_inputrowsrowrow_sumslice))))) * dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceentrysourcenegative. dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentrysource = ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (srt_index_zero_outer_inputrows)))) + ((t) * (srs_index_zero_outer_inputrowsrowrow_sumslice))))) * dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentrysource) + (dst_negative_zero_outer_inputrowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceentrysourcevalue ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceentrysourcevalue. (((((srs_value_zero_outer_inputrowsrowrow_sumslice) = 2 * (ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_zero_outer_inputrowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_zero_outer_inputrowsrowrow_sumslice) = 2 * ge_signed_half_zero_outer_inputrowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_zero_outer_inputrowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_zero_outer_inputrowsrowrow_sumsliceentrysource) + ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceentrysourcevalue = (dst_negative_zero_outer_inputrowsrowrow_sumsliceentrysource) + ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentryoutput dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput dst_positive_zero_outer_inputrowsrowrow_sumsliceentryoutput dst_negative_zero_outer_inputrowsrowrow_sumsliceentryoutput. (((srs_slice_zero_outer_inputrowsrowrow_sum) = (((((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceentryoutputpositive + S (dst_positive_zero_outer_inputrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_zero_outer_inputrowsrowrow_sumslice)) * dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceentryoutputpositive. dst_positive_code_zero_outer_inputrowsrowrow_sumsliceentryoutput = ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_zero_outer_inputrowsrowrow_sumslice)) * dst_positive_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_positive_zero_outer_inputrowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_zero_outer_inputrowsrowrow_sumsliceentryoutputnegative + S (dst_negative_zero_outer_inputrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_zero_outer_inputrowsrowrow_sumslice)) * dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceentryoutputnegative. dst_negative_code_zero_outer_inputrowsrowrow_sumsliceentryoutput = ff_q_pvs_zero_outer_inputrowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_zero_outer_inputrowsrowrow_sumslice)) * dst_negative_scale_zero_outer_inputrowsrowrow_sumsliceentryoutput) + (dst_negative_zero_outer_inputrowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceentryoutputvalue ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceentryoutputvalue. (((((srs_value_zero_outer_inputrowsrowrow_sumslice) = 2 * (ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_zero_outer_inputrowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_zero_outer_inputrowsrowrow_sumslice) = 2 * ge_signed_half_zero_outer_inputrowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_zero_outer_inputrowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_zero_outer_inputrowsrowrow_sumsliceentryoutput) + ge_balance_negative_zero_outer_inputrowsrowrow_sumsliceentryoutputvalue = (dst_negative_zero_outer_inputrowsrowrow_sumsliceentryoutput) + ge_balance_positive_zero_outer_inputrowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_zero_outer_inputrowsrowrow_sumsum dst_positive_scale_zero_outer_inputrowsrowrow_sumsum dst_negative_code_zero_outer_inputrowsrowrow_sumsum dst_negative_scale_zero_outer_inputrowsrowrow_sumsum dst_positive_sum_zero_outer_inputrowsrowrow_sumsum dst_negative_sum_zero_outer_inputrowsrowrow_sumsum. (((srs_slice_zero_outer_inputrowsrowrow_sum) = (((((dst_positive_code_zero_outer_inputrowsrowrow_sumsum) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsum)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumsum) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsum)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumsum) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsum))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)))) * S ((((dst_positive_code_zero_outer_inputrowsrowrow_sumsum) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsum)) * S ((dst_positive_code_zero_outer_inputrowsrowrow_sumsum) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsum)) + ((dst_positive_scale_zero_outer_inputrowsrowrow_sumsum) + (dst_positive_scale_zero_outer_inputrowsrowrow_sumsum))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)))) + ((((dst_negative_code_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum))) + (((dst_negative_code_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)) * S ((dst_negative_code_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)) + ((dst_negative_scale_zero_outer_inputrowsrowrow_sumsum) + (dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_zero_outer_inputrowsrowrow_sumsumpositive fs_v_dst_zero_outer_inputrowsrowrow_sumsumpositive. ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_start. fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_start. fs_u_dst_zero_outer_inputrowsrowrow_sumsumpositive = fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_terminal. fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_zero_outer_inputrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_terminal. fs_u_dst_zero_outer_inputrowsrowrow_sumsumpositive = fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumpositive) + (dst_positive_sum_zero_outer_inputrowsrowrow_sumsum))) /\ forall fs_i_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps fs_r_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps fs_s_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_zero_outer_inputrowsrowrow_sumsum)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_zero_outer_inputrowsrowrow_sumsum = fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_zero_outer_inputrowsrowrow_sumsum) + (fs_a_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_zero_outer_inputrowsrowrow_sumsumpositive = fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumpositive) + (fs_r_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_zero_outer_inputrowsrowrow_sumsumpositive = fs_q_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumpositive) + (fs_s_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps = fs_r_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps + fs_a_dst_zero_outer_inputrowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_zero_outer_inputrowsrowrow_sumsumnegative fs_v_dst_zero_outer_inputrowsrowrow_sumsumnegative. ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_start. fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_start. fs_u_dst_zero_outer_inputrowsrowrow_sumsumnegative = fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_terminal. fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_zero_outer_inputrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_terminal. fs_u_dst_zero_outer_inputrowsrowrow_sumsumnegative = fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumnegative) + (dst_negative_sum_zero_outer_inputrowsrowrow_sumsum))) /\ forall fs_i_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps fs_r_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps fs_s_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_zero_outer_inputrowsrowrow_sumsum)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_zero_outer_inputrowsrowrow_sumsum = fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_zero_outer_inputrowsrowrow_sumsum) + (fs_a_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_zero_outer_inputrowsrowrow_sumsumnegative = fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumnegative) + (fs_r_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_zero_outer_inputrowsrowrow_sumsumnegative = fs_q_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_zero_outer_inputrowsrowrow_sumsumnegative) + (fs_s_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps = fs_r_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps + fs_a_dst_zero_outer_inputrowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_zero_outer_inputrowsrowrow_sumsumresult ge_balance_negative_zero_outer_inputrowsrowrow_sumsumresult. (((((srt_value_zero_outer_inputrows) = 2 * (ge_balance_positive_zero_outer_inputrowsrowrow_sumsumresult) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_zero_outer_inputrowsrowrow_sumsumresultdecode. (((srt_value_zero_outer_inputrows) = 2 * ge_signed_half_zero_outer_inputrowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_zero_outer_inputrowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_zero_outer_inputrowsrowrow_sumsumresult) = S ge_signed_half_zero_outer_inputrowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_zero_outer_inputrowsrowrow_sumsum) + ge_balance_negative_zero_outer_inputrowsrowrow_sumsumresult = (dst_negative_sum_zero_outer_inputrowsrowrow_sumsum) + ge_balance_positive_zero_outer_inputrowsrowrow_sumsumresult)))))))))))))))))) /\ (exists dst_positive_code_zero_outer_inputtotal dst_positive_scale_zero_outer_inputtotal dst_negative_code_zero_outer_inputtotal dst_negative_scale_zero_outer_inputtotal dst_positive_sum_zero_outer_inputtotal dst_negative_sum_zero_outer_inputtotal. (((srt_rows_zero_outer_input) = (((((dst_positive_code_zero_outer_inputtotal) + (dst_positive_scale_zero_outer_inputtotal)) * S ((dst_positive_code_zero_outer_inputtotal) + (dst_positive_scale_zero_outer_inputtotal)) + ((dst_positive_scale_zero_outer_inputtotal) + (dst_positive_scale_zero_outer_inputtotal))) + (((dst_negative_code_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)) * S ((dst_negative_code_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)) + ((dst_negative_scale_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)))) * S ((((dst_positive_code_zero_outer_inputtotal) + (dst_positive_scale_zero_outer_inputtotal)) * S ((dst_positive_code_zero_outer_inputtotal) + (dst_positive_scale_zero_outer_inputtotal)) + ((dst_positive_scale_zero_outer_inputtotal) + (dst_positive_scale_zero_outer_inputtotal))) + (((dst_negative_code_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)) * S ((dst_negative_code_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)) + ((dst_negative_scale_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)))) + ((((dst_negative_code_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)) * S ((dst_negative_code_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)) + ((dst_negative_scale_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal))) + (((dst_negative_code_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)) * S ((dst_negative_code_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)) + ((dst_negative_scale_zero_outer_inputtotal) + (dst_negative_scale_zero_outer_inputtotal)))))) /\ (((exists fs_u_dst_zero_outer_inputtotalpositive fs_v_dst_zero_outer_inputtotalpositive. ((((exists fs_h_dst_zero_outer_inputtotalpositive_body_start. fs_h_dst_zero_outer_inputtotalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_outer_inputtotalpositive)) /\ exists fs_q_dst_zero_outer_inputtotalpositive_body_start. fs_u_dst_zero_outer_inputtotalpositive = fs_q_dst_zero_outer_inputtotalpositive_body_start * S ((S (0)) * fs_v_dst_zero_outer_inputtotalpositive) + (0))) /\ ((((exists fs_h_dst_zero_outer_inputtotalpositive_body_terminal. fs_h_dst_zero_outer_inputtotalpositive_body_terminal + S (dst_positive_sum_zero_outer_inputtotal) = S ((S (0)) * fs_v_dst_zero_outer_inputtotalpositive)) /\ exists fs_q_dst_zero_outer_inputtotalpositive_body_terminal. fs_u_dst_zero_outer_inputtotalpositive = fs_q_dst_zero_outer_inputtotalpositive_body_terminal * S ((S (0)) * fs_v_dst_zero_outer_inputtotalpositive) + (dst_positive_sum_zero_outer_inputtotal))) /\ forall fs_i_dst_zero_outer_inputtotalpositive_body_steps. (exists fs_lt_dst_zero_outer_inputtotalpositive_body_steps_bound. fs_lt_dst_zero_outer_inputtotalpositive_body_steps_bound + S fs_i_dst_zero_outer_inputtotalpositive_body_steps = 0) -> exists fs_a_dst_zero_outer_inputtotalpositive_body_steps fs_r_dst_zero_outer_inputtotalpositive_body_steps fs_s_dst_zero_outer_inputtotalpositive_body_steps. ((((exists fs_h_dst_zero_outer_inputtotalpositive_body_steps_summand. fs_h_dst_zero_outer_inputtotalpositive_body_steps_summand + S (fs_a_dst_zero_outer_inputtotalpositive_body_steps) = S ((S (fs_i_dst_zero_outer_inputtotalpositive_body_steps)) * dst_positive_scale_zero_outer_inputtotal)) /\ exists fs_q_dst_zero_outer_inputtotalpositive_body_steps_summand. dst_positive_code_zero_outer_inputtotal = fs_q_dst_zero_outer_inputtotalpositive_body_steps_summand * S ((S (fs_i_dst_zero_outer_inputtotalpositive_body_steps)) * dst_positive_scale_zero_outer_inputtotal) + (fs_a_dst_zero_outer_inputtotalpositive_body_steps))) /\ ((((exists fs_h_dst_zero_outer_inputtotalpositive_body_steps_partial. fs_h_dst_zero_outer_inputtotalpositive_body_steps_partial + S (fs_r_dst_zero_outer_inputtotalpositive_body_steps) = S ((S (fs_i_dst_zero_outer_inputtotalpositive_body_steps)) * fs_v_dst_zero_outer_inputtotalpositive)) /\ exists fs_q_dst_zero_outer_inputtotalpositive_body_steps_partial. fs_u_dst_zero_outer_inputtotalpositive = fs_q_dst_zero_outer_inputtotalpositive_body_steps_partial * S ((S (fs_i_dst_zero_outer_inputtotalpositive_body_steps)) * fs_v_dst_zero_outer_inputtotalpositive) + (fs_r_dst_zero_outer_inputtotalpositive_body_steps))) /\ ((((exists fs_h_dst_zero_outer_inputtotalpositive_body_steps_successor. fs_h_dst_zero_outer_inputtotalpositive_body_steps_successor + S (fs_s_dst_zero_outer_inputtotalpositive_body_steps) = S ((S (S fs_i_dst_zero_outer_inputtotalpositive_body_steps)) * fs_v_dst_zero_outer_inputtotalpositive)) /\ exists fs_q_dst_zero_outer_inputtotalpositive_body_steps_successor. fs_u_dst_zero_outer_inputtotalpositive = fs_q_dst_zero_outer_inputtotalpositive_body_steps_successor * S ((S (S fs_i_dst_zero_outer_inputtotalpositive_body_steps)) * fs_v_dst_zero_outer_inputtotalpositive) + (fs_s_dst_zero_outer_inputtotalpositive_body_steps))) /\ fs_s_dst_zero_outer_inputtotalpositive_body_steps = fs_r_dst_zero_outer_inputtotalpositive_body_steps + fs_a_dst_zero_outer_inputtotalpositive_body_steps)))))) /\ (((exists fs_u_dst_zero_outer_inputtotalnegative fs_v_dst_zero_outer_inputtotalnegative. ((((exists fs_h_dst_zero_outer_inputtotalnegative_body_start. fs_h_dst_zero_outer_inputtotalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_outer_inputtotalnegative)) /\ exists fs_q_dst_zero_outer_inputtotalnegative_body_start. fs_u_dst_zero_outer_inputtotalnegative = fs_q_dst_zero_outer_inputtotalnegative_body_start * S ((S (0)) * fs_v_dst_zero_outer_inputtotalnegative) + (0))) /\ ((((exists fs_h_dst_zero_outer_inputtotalnegative_body_terminal. fs_h_dst_zero_outer_inputtotalnegative_body_terminal + S (dst_negative_sum_zero_outer_inputtotal) = S ((S (0)) * fs_v_dst_zero_outer_inputtotalnegative)) /\ exists fs_q_dst_zero_outer_inputtotalnegative_body_terminal. fs_u_dst_zero_outer_inputtotalnegative = fs_q_dst_zero_outer_inputtotalnegative_body_terminal * S ((S (0)) * fs_v_dst_zero_outer_inputtotalnegative) + (dst_negative_sum_zero_outer_inputtotal))) /\ forall fs_i_dst_zero_outer_inputtotalnegative_body_steps. (exists fs_lt_dst_zero_outer_inputtotalnegative_body_steps_bound. fs_lt_dst_zero_outer_inputtotalnegative_body_steps_bound + S fs_i_dst_zero_outer_inputtotalnegative_body_steps = 0) -> exists fs_a_dst_zero_outer_inputtotalnegative_body_steps fs_r_dst_zero_outer_inputtotalnegative_body_steps fs_s_dst_zero_outer_inputtotalnegative_body_steps. ((((exists fs_h_dst_zero_outer_inputtotalnegative_body_steps_summand. fs_h_dst_zero_outer_inputtotalnegative_body_steps_summand + S (fs_a_dst_zero_outer_inputtotalnegative_body_steps) = S ((S (fs_i_dst_zero_outer_inputtotalnegative_body_steps)) * dst_negative_scale_zero_outer_inputtotal)) /\ exists fs_q_dst_zero_outer_inputtotalnegative_body_steps_summand. dst_negative_code_zero_outer_inputtotal = fs_q_dst_zero_outer_inputtotalnegative_body_steps_summand * S ((S (fs_i_dst_zero_outer_inputtotalnegative_body_steps)) * dst_negative_scale_zero_outer_inputtotal) + (fs_a_dst_zero_outer_inputtotalnegative_body_steps))) /\ ((((exists fs_h_dst_zero_outer_inputtotalnegative_body_steps_partial. fs_h_dst_zero_outer_inputtotalnegative_body_steps_partial + S (fs_r_dst_zero_outer_inputtotalnegative_body_steps) = S ((S (fs_i_dst_zero_outer_inputtotalnegative_body_steps)) * fs_v_dst_zero_outer_inputtotalnegative)) /\ exists fs_q_dst_zero_outer_inputtotalnegative_body_steps_partial. fs_u_dst_zero_outer_inputtotalnegative = fs_q_dst_zero_outer_inputtotalnegative_body_steps_partial * S ((S (fs_i_dst_zero_outer_inputtotalnegative_body_steps)) * fs_v_dst_zero_outer_inputtotalnegative) + (fs_r_dst_zero_outer_inputtotalnegative_body_steps))) /\ ((((exists fs_h_dst_zero_outer_inputtotalnegative_body_steps_successor. fs_h_dst_zero_outer_inputtotalnegative_body_steps_successor + S (fs_s_dst_zero_outer_inputtotalnegative_body_steps) = S ((S (S fs_i_dst_zero_outer_inputtotalnegative_body_steps)) * fs_v_dst_zero_outer_inputtotalnegative)) /\ exists fs_q_dst_zero_outer_inputtotalnegative_body_steps_successor. fs_u_dst_zero_outer_inputtotalnegative = fs_q_dst_zero_outer_inputtotalnegative_body_steps_successor * S ((S (S fs_i_dst_zero_outer_inputtotalnegative_body_steps)) * fs_v_dst_zero_outer_inputtotalnegative) + (fs_s_dst_zero_outer_inputtotalnegative_body_steps))) /\ fs_s_dst_zero_outer_inputtotalnegative_body_steps = fs_r_dst_zero_outer_inputtotalnegative_body_steps + fs_a_dst_zero_outer_inputtotalnegative_body_steps)))))) /\ (exists ge_balance_positive_zero_outer_inputtotalresult ge_balance_negative_zero_outer_inputtotalresult. (((((z) = 2 * (ge_balance_positive_zero_outer_inputtotalresult) /\ (ge_balance_negative_zero_outer_inputtotalresult) = 0) \/ exists ge_signed_half_zero_outer_inputtotalresultdecode. (((z) = 2 * ge_signed_half_zero_outer_inputtotalresultdecode + 1 /\ (ge_balance_positive_zero_outer_inputtotalresult) = 0) /\ (ge_balance_negative_zero_outer_inputtotalresult) = S ge_signed_half_zero_outer_inputtotalresultdecode))) /\ ((dst_positive_sum_zero_outer_inputtotal) + ge_balance_negative_zero_outer_inputtotalresult = (dst_negative_sum_zero_outer_inputtotal) + ge_balance_positive_zero_outer_inputtotalresult))))))))))) -> z=0