signed_row_sums_flatten

Exact expanded first-order arithmetic statement

forall m F R n z. (((exists dst_positive_code_flatten_rowssource_table dst_positive_scale_flatten_rowssource_table dst_negative_code_flatten_rowssource_table dst_negative_scale_flatten_rowssource_table. (((F) = (((((dst_positive_code_flatten_rowssource_table) + (dst_positive_scale_flatten_rowssource_table)) * S ((dst_positive_code_flatten_rowssource_table) + (dst_positive_scale_flatten_rowssource_table)) + ((dst_positive_scale_flatten_rowssource_table) + (dst_positive_scale_flatten_rowssource_table))) + (((dst_negative_code_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)) * S ((dst_negative_code_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)) + ((dst_negative_scale_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)))) * S ((((dst_positive_code_flatten_rowssource_table) + (dst_positive_scale_flatten_rowssource_table)) * S ((dst_positive_code_flatten_rowssource_table) + (dst_positive_scale_flatten_rowssource_table)) + ((dst_positive_scale_flatten_rowssource_table) + (dst_positive_scale_flatten_rowssource_table))) + (((dst_negative_code_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)) * S ((dst_negative_code_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)) + ((dst_negative_scale_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)))) + ((((dst_negative_code_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)) * S ((dst_negative_code_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)) + ((dst_negative_scale_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table))) + (((dst_negative_code_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)) * S ((dst_negative_code_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)) + ((dst_negative_scale_flatten_rowssource_table) + (dst_negative_scale_flatten_rowssource_table)))))) /\ (forall dst_index_flatten_rowssource_table. (exists pvs_le_gap_flatten_rowssource_tabledomain. pvs_le_gap_flatten_rowssource_tabledomain + (dst_index_flatten_rowssource_table) = (0)) -> exists dst_positive_flatten_rowssource_table dst_negative_flatten_rowssource_table dst_value_flatten_rowssource_table. ((((exists ff_h_pvs_flatten_rowssource_tableentrypositive. ff_h_pvs_flatten_rowssource_tableentrypositive + S (dst_positive_flatten_rowssource_table) = S ((S (dst_index_flatten_rowssource_table)) * dst_positive_scale_flatten_rowssource_table)) /\ exists ff_q_pvs_flatten_rowssource_tableentrypositive. dst_positive_code_flatten_rowssource_table = ff_q_pvs_flatten_rowssource_tableentrypositive * S ((S (dst_index_flatten_rowssource_table)) * dst_positive_scale_flatten_rowssource_table) + (dst_positive_flatten_rowssource_table))) /\ (((((exists ff_h_pvs_flatten_rowssource_tableentrynegative. ff_h_pvs_flatten_rowssource_tableentrynegative + S (dst_negative_flatten_rowssource_table) = S ((S (dst_index_flatten_rowssource_table)) * dst_negative_scale_flatten_rowssource_table)) /\ exists ff_q_pvs_flatten_rowssource_tableentrynegative. dst_negative_code_flatten_rowssource_table = ff_q_pvs_flatten_rowssource_tableentrynegative * S ((S (dst_index_flatten_rowssource_table)) * dst_negative_scale_flatten_rowssource_table) + (dst_negative_flatten_rowssource_table))) /\ (exists ge_balance_positive_flatten_rowssource_tableentryvalue ge_balance_negative_flatten_rowssource_tableentryvalue. (((((dst_value_flatten_rowssource_table) = 2 * (ge_balance_positive_flatten_rowssource_tableentryvalue) /\ (ge_balance_negative_flatten_rowssource_tableentryvalue) = 0) \/ exists ge_signed_half_flatten_rowssource_tableentryvaluedecode. (((dst_value_flatten_rowssource_table) = 2 * ge_signed_half_flatten_rowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_flatten_rowssource_tableentryvalue) = 0) /\ (ge_balance_negative_flatten_rowssource_tableentryvalue) = S ge_signed_half_flatten_rowssource_tableentryvaluedecode))) /\ ((dst_positive_flatten_rowssource_table) + ge_balance_negative_flatten_rowssource_tableentryvalue = (dst_negative_flatten_rowssource_table) + ge_balance_positive_flatten_rowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_flatten_rowsrow_table dst_positive_scale_flatten_rowsrow_table dst_negative_code_flatten_rowsrow_table dst_negative_scale_flatten_rowsrow_table. (((R) = (((((dst_positive_code_flatten_rowsrow_table) + (dst_positive_scale_flatten_rowsrow_table)) * S ((dst_positive_code_flatten_rowsrow_table) + (dst_positive_scale_flatten_rowsrow_table)) + ((dst_positive_scale_flatten_rowsrow_table) + (dst_positive_scale_flatten_rowsrow_table))) + (((dst_negative_code_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)) * S ((dst_negative_code_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)) + ((dst_negative_scale_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)))) * S ((((dst_positive_code_flatten_rowsrow_table) + (dst_positive_scale_flatten_rowsrow_table)) * S ((dst_positive_code_flatten_rowsrow_table) + (dst_positive_scale_flatten_rowsrow_table)) + ((dst_positive_scale_flatten_rowsrow_table) + (dst_positive_scale_flatten_rowsrow_table))) + (((dst_negative_code_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)) * S ((dst_negative_code_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)) + ((dst_negative_scale_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)))) + ((((dst_negative_code_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)) * S ((dst_negative_code_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)) + ((dst_negative_scale_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table))) + (((dst_negative_code_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)) * S ((dst_negative_code_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)) + ((dst_negative_scale_flatten_rowsrow_table) + (dst_negative_scale_flatten_rowsrow_table)))))) /\ (forall dst_index_flatten_rowsrow_table. (exists pvs_le_gap_flatten_rowsrow_tabledomain. pvs_le_gap_flatten_rowsrow_tabledomain + (dst_index_flatten_rowsrow_table) = (m)) -> exists dst_positive_flatten_rowsrow_table dst_negative_flatten_rowsrow_table dst_value_flatten_rowsrow_table. ((((exists ff_h_pvs_flatten_rowsrow_tableentrypositive. ff_h_pvs_flatten_rowsrow_tableentrypositive + S (dst_positive_flatten_rowsrow_table) = S ((S (dst_index_flatten_rowsrow_table)) * dst_positive_scale_flatten_rowsrow_table)) /\ exists ff_q_pvs_flatten_rowsrow_tableentrypositive. dst_positive_code_flatten_rowsrow_table = ff_q_pvs_flatten_rowsrow_tableentrypositive * S ((S (dst_index_flatten_rowsrow_table)) * dst_positive_scale_flatten_rowsrow_table) + (dst_positive_flatten_rowsrow_table))) /\ (((((exists ff_h_pvs_flatten_rowsrow_tableentrynegative. ff_h_pvs_flatten_rowsrow_tableentrynegative + S (dst_negative_flatten_rowsrow_table) = S ((S (dst_index_flatten_rowsrow_table)) * dst_negative_scale_flatten_rowsrow_table)) /\ exists ff_q_pvs_flatten_rowsrow_tableentrynegative. dst_negative_code_flatten_rowsrow_table = ff_q_pvs_flatten_rowsrow_tableentrynegative * S ((S (dst_index_flatten_rowsrow_table)) * dst_negative_scale_flatten_rowsrow_table) + (dst_negative_flatten_rowsrow_table))) /\ (exists ge_balance_positive_flatten_rowsrow_tableentryvalue ge_balance_negative_flatten_rowsrow_tableentryvalue. (((((dst_value_flatten_rowsrow_table) = 2 * (ge_balance_positive_flatten_rowsrow_tableentryvalue) /\ (ge_balance_negative_flatten_rowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_flatten_rowsrow_tableentryvaluedecode. (((dst_value_flatten_rowsrow_table) = 2 * ge_signed_half_flatten_rowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_flatten_rowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_flatten_rowsrow_tableentryvalue) = S ge_signed_half_flatten_rowsrow_tableentryvaluedecode))) /\ ((dst_positive_flatten_rowsrow_table) + ge_balance_negative_flatten_rowsrow_tableentryvalue = (dst_negative_flatten_rowsrow_table) + ge_balance_positive_flatten_rowsrow_tableentryvalue))))))))) /\ (forall srt_index_flatten_rows. (exists pvs_gap_flatten_rowsbound. pvs_gap_flatten_rowsbound + S (srt_index_flatten_rows) = (m)) -> exists srt_value_flatten_rows. (((exists dst_positive_code_flatten_rowsrowentry dst_positive_scale_flatten_rowsrowentry dst_negative_code_flatten_rowsrowentry dst_negative_scale_flatten_rowsrowentry dst_positive_flatten_rowsrowentry dst_negative_flatten_rowsrowentry. (((R) = (((((dst_positive_code_flatten_rowsrowentry) + (dst_positive_scale_flatten_rowsrowentry)) * S ((dst_positive_code_flatten_rowsrowentry) + (dst_positive_scale_flatten_rowsrowentry)) + ((dst_positive_scale_flatten_rowsrowentry) + (dst_positive_scale_flatten_rowsrowentry))) + (((dst_negative_code_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)) * S ((dst_negative_code_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)) + ((dst_negative_scale_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)))) * S ((((dst_positive_code_flatten_rowsrowentry) + (dst_positive_scale_flatten_rowsrowentry)) * S ((dst_positive_code_flatten_rowsrowentry) + (dst_positive_scale_flatten_rowsrowentry)) + ((dst_positive_scale_flatten_rowsrowentry) + (dst_positive_scale_flatten_rowsrowentry))) + (((dst_negative_code_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)) * S ((dst_negative_code_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)) + ((dst_negative_scale_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)))) + ((((dst_negative_code_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)) * S ((dst_negative_code_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)) + ((dst_negative_scale_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry))) + (((dst_negative_code_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)) * S ((dst_negative_code_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)) + ((dst_negative_scale_flatten_rowsrowentry) + (dst_negative_scale_flatten_rowsrowentry)))))) /\ (((((exists ff_h_pvs_flatten_rowsrowentrypositive. ff_h_pvs_flatten_rowsrowentrypositive + S (dst_positive_flatten_rowsrowentry) = S ((S (srt_index_flatten_rows)) * dst_positive_scale_flatten_rowsrowentry)) /\ exists ff_q_pvs_flatten_rowsrowentrypositive. dst_positive_code_flatten_rowsrowentry = ff_q_pvs_flatten_rowsrowentrypositive * S ((S (srt_index_flatten_rows)) * dst_positive_scale_flatten_rowsrowentry) + (dst_positive_flatten_rowsrowentry))) /\ (((((exists ff_h_pvs_flatten_rowsrowentrynegative. ff_h_pvs_flatten_rowsrowentrynegative + S (dst_negative_flatten_rowsrowentry) = S ((S (srt_index_flatten_rows)) * dst_negative_scale_flatten_rowsrowentry)) /\ exists ff_q_pvs_flatten_rowsrowentrynegative. dst_negative_code_flatten_rowsrowentry = ff_q_pvs_flatten_rowsrowentrynegative * S ((S (srt_index_flatten_rows)) * dst_negative_scale_flatten_rowsrowentry) + (dst_negative_flatten_rowsrowentry))) /\ (exists ge_balance_positive_flatten_rowsrowentryvalue ge_balance_negative_flatten_rowsrowentryvalue. (((((srt_value_flatten_rows) = 2 * (ge_balance_positive_flatten_rowsrowentryvalue) /\ (ge_balance_negative_flatten_rowsrowentryvalue) = 0) \/ exists ge_signed_half_flatten_rowsrowentryvaluedecode. (((srt_value_flatten_rows) = 2 * ge_signed_half_flatten_rowsrowentryvaluedecode + 1 /\ (ge_balance_positive_flatten_rowsrowentryvalue) = 0) /\ (ge_balance_negative_flatten_rowsrowentryvalue) = S ge_signed_half_flatten_rowsrowentryvaluedecode))) /\ ((dst_positive_flatten_rowsrowentry) + ge_balance_negative_flatten_rowsrowentryvalue = (dst_negative_flatten_rowsrowentry) + ge_balance_positive_flatten_rowsrowentryvalue))))))))) /\ (exists srs_slice_flatten_rowsrowrow_sum. ((((exists dst_positive_code_flatten_rowsrowrow_sumslicesource_table dst_positive_scale_flatten_rowsrowrow_sumslicesource_table dst_negative_code_flatten_rowsrowrow_sumslicesource_table dst_negative_scale_flatten_rowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_flatten_rowsrowrow_sumslicesource_table) + (dst_positive_scale_flatten_rowsrowrow_sumslicesource_table)) * S ((dst_positive_code_flatten_rowsrowrow_sumslicesource_table) + (dst_positive_scale_flatten_rowsrowrow_sumslicesource_table)) + ((dst_positive_scale_flatten_rowsrowrow_sumslicesource_table) + (dst_positive_scale_flatten_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_flatten_rowsrowrow_sumslicesource_table) + (dst_positive_scale_flatten_rowsrowrow_sumslicesource_table)) * S ((dst_positive_code_flatten_rowsrowrow_sumslicesource_table) + (dst_positive_scale_flatten_rowsrowrow_sumslicesource_table)) + ((dst_positive_scale_flatten_rowsrowrow_sumslicesource_table) + (dst_positive_scale_flatten_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_flatten_rowsrowrow_sumslicesource_table. (exists pvs_le_gap_flatten_rowsrowrow_sumslicesource_tabledomain. pvs_le_gap_flatten_rowsrowrow_sumslicesource_tabledomain + (dst_index_flatten_rowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_flatten_rowsrowrow_sumslicesource_table dst_negative_flatten_rowsrowrow_sumslicesource_table dst_value_flatten_rowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_flatten_rowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_flatten_rowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_flatten_rowsrowrow_sumslicesource_table) = S ((S (dst_index_flatten_rowsrowrow_sumslicesource_table)) * dst_positive_scale_flatten_rowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_flatten_rowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_flatten_rowsrowrow_sumslicesource_table = ff_q_pvs_flatten_rowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_flatten_rowsrowrow_sumslicesource_table)) * dst_positive_scale_flatten_rowsrowrow_sumslicesource_table) + (dst_positive_flatten_rowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_flatten_rowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_flatten_rowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_flatten_rowsrowrow_sumslicesource_table) = S ((S (dst_index_flatten_rowsrowrow_sumslicesource_table)) * dst_negative_scale_flatten_rowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_flatten_rowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_flatten_rowsrowrow_sumslicesource_table = ff_q_pvs_flatten_rowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_flatten_rowsrowrow_sumslicesource_table)) * dst_negative_scale_flatten_rowsrowrow_sumslicesource_table) + (dst_negative_flatten_rowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_flatten_rowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_flatten_rowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_flatten_rowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_flatten_rowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_flatten_rowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_flatten_rowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_flatten_rowsrowrow_sumslicesource_table) = 2 * ge_signed_half_flatten_rowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_flatten_rowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_flatten_rowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_flatten_rowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_flatten_rowsrowrow_sumslicesource_table) + ge_balance_negative_flatten_rowsrowrow_sumslicesource_tableentryvalue = (dst_negative_flatten_rowsrowrow_sumslicesource_table) + ge_balance_positive_flatten_rowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_flatten_rowsrowrow_sumsliceoutput_table dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table. (((srs_slice_flatten_rowsrowrow_sum) = (((((dst_positive_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_flatten_rowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_flatten_rowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_flatten_rowsrowrow_sumsliceoutput_tabledomain + (dst_index_flatten_rowsrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_flatten_rowsrowrow_sumsliceoutput_table dst_negative_flatten_rowsrowrow_sumsliceoutput_table dst_value_flatten_rowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_flatten_rowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_flatten_rowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_flatten_rowsrowrow_sumsliceoutput_table) = S ((S (dst_index_flatten_rowsrowrow_sumsliceoutput_table)) * dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_flatten_rowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_flatten_rowsrowrow_sumsliceoutput_table = ff_q_pvs_flatten_rowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_flatten_rowsrowrow_sumsliceoutput_table)) * dst_positive_scale_flatten_rowsrowrow_sumsliceoutput_table) + (dst_positive_flatten_rowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_flatten_rowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_flatten_rowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_flatten_rowsrowrow_sumsliceoutput_table) = S ((S (dst_index_flatten_rowsrowrow_sumsliceoutput_table)) * dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_flatten_rowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_flatten_rowsrowrow_sumsliceoutput_table = ff_q_pvs_flatten_rowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_flatten_rowsrowrow_sumsliceoutput_table)) * dst_negative_scale_flatten_rowsrowrow_sumsliceoutput_table) + (dst_negative_flatten_rowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_flatten_rowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_flatten_rowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_flatten_rowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_flatten_rowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_flatten_rowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_flatten_rowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_flatten_rowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_flatten_rowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_flatten_rowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_flatten_rowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_flatten_rowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_flatten_rowsrowrow_sumsliceoutput_table) + ge_balance_negative_flatten_rowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_flatten_rowsrowrow_sumsliceoutput_table) + ge_balance_positive_flatten_rowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_flatten_rowsrowrow_sumslice. (exists pvs_gap_flatten_rowsrowrow_sumslicebound. pvs_gap_flatten_rowsrowrow_sumslicebound + S (srs_index_flatten_rowsrowrow_sumslice) = (n)) -> exists srs_value_flatten_rowsrowrow_sumslice. (((exists dst_positive_code_flatten_rowsrowrow_sumsliceentrysource dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource dst_negative_code_flatten_rowsrowrow_sumsliceentrysource dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource dst_positive_flatten_rowsrowrow_sumsliceentrysource dst_negative_flatten_rowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_flatten_rowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_flatten_rowsrowrow_sumsliceentrysourcepositive + S (dst_positive_flatten_rowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_flatten_rows)))) + ((1) * (srs_index_flatten_rowsrowrow_sumslice))))) * dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_flatten_rowsrowrow_sumsliceentrysourcepositive. dst_positive_code_flatten_rowsrowrow_sumsliceentrysource = ff_q_pvs_flatten_rowsrowrow_sumsliceentrysourcepositive * S ((S (((((0) + ((n) * (srt_index_flatten_rows)))) + ((1) * (srs_index_flatten_rowsrowrow_sumslice))))) * dst_positive_scale_flatten_rowsrowrow_sumsliceentrysource) + (dst_positive_flatten_rowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_flatten_rowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_flatten_rowsrowrow_sumsliceentrysourcenegative + S (dst_negative_flatten_rowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_flatten_rows)))) + ((1) * (srs_index_flatten_rowsrowrow_sumslice))))) * dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_flatten_rowsrowrow_sumsliceentrysourcenegative. dst_negative_code_flatten_rowsrowrow_sumsliceentrysource = ff_q_pvs_flatten_rowsrowrow_sumsliceentrysourcenegative * S ((S (((((0) + ((n) * (srt_index_flatten_rows)))) + ((1) * (srs_index_flatten_rowsrowrow_sumslice))))) * dst_negative_scale_flatten_rowsrowrow_sumsliceentrysource) + (dst_negative_flatten_rowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_flatten_rowsrowrow_sumsliceentrysourcevalue ge_balance_negative_flatten_rowsrowrow_sumsliceentrysourcevalue. (((((srs_value_flatten_rowsrowrow_sumslice) = 2 * (ge_balance_positive_flatten_rowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_flatten_rowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_flatten_rowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_flatten_rowsrowrow_sumslice) = 2 * ge_signed_half_flatten_rowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_flatten_rowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_flatten_rowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_flatten_rowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_flatten_rowsrowrow_sumsliceentrysource) + ge_balance_negative_flatten_rowsrowrow_sumsliceentrysourcevalue = (dst_negative_flatten_rowsrowrow_sumsliceentrysource) + ge_balance_positive_flatten_rowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_flatten_rowsrowrow_sumsliceentryoutput dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput dst_positive_flatten_rowsrowrow_sumsliceentryoutput dst_negative_flatten_rowsrowrow_sumsliceentryoutput. (((srs_slice_flatten_rowsrowrow_sum) = (((((dst_positive_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_flatten_rowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_flatten_rowsrowrow_sumsliceentryoutputpositive + S (dst_positive_flatten_rowsrowrow_sumsliceentryoutput) = S ((S (srs_index_flatten_rowsrowrow_sumslice)) * dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_flatten_rowsrowrow_sumsliceentryoutputpositive. dst_positive_code_flatten_rowsrowrow_sumsliceentryoutput = ff_q_pvs_flatten_rowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_flatten_rowsrowrow_sumslice)) * dst_positive_scale_flatten_rowsrowrow_sumsliceentryoutput) + (dst_positive_flatten_rowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_flatten_rowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_flatten_rowsrowrow_sumsliceentryoutputnegative + S (dst_negative_flatten_rowsrowrow_sumsliceentryoutput) = S ((S (srs_index_flatten_rowsrowrow_sumslice)) * dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_flatten_rowsrowrow_sumsliceentryoutputnegative. dst_negative_code_flatten_rowsrowrow_sumsliceentryoutput = ff_q_pvs_flatten_rowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_flatten_rowsrowrow_sumslice)) * dst_negative_scale_flatten_rowsrowrow_sumsliceentryoutput) + (dst_negative_flatten_rowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_flatten_rowsrowrow_sumsliceentryoutputvalue ge_balance_negative_flatten_rowsrowrow_sumsliceentryoutputvalue. (((((srs_value_flatten_rowsrowrow_sumslice) = 2 * (ge_balance_positive_flatten_rowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_flatten_rowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_flatten_rowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_flatten_rowsrowrow_sumslice) = 2 * ge_signed_half_flatten_rowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_flatten_rowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_flatten_rowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_flatten_rowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_flatten_rowsrowrow_sumsliceentryoutput) + ge_balance_negative_flatten_rowsrowrow_sumsliceentryoutputvalue = (dst_negative_flatten_rowsrowrow_sumsliceentryoutput) + ge_balance_positive_flatten_rowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_flatten_rowsrowrow_sumsum dst_positive_scale_flatten_rowsrowrow_sumsum dst_negative_code_flatten_rowsrowrow_sumsum dst_negative_scale_flatten_rowsrowrow_sumsum dst_positive_sum_flatten_rowsrowrow_sumsum dst_negative_sum_flatten_rowsrowrow_sumsum. (((srs_slice_flatten_rowsrowrow_sum) = (((((dst_positive_code_flatten_rowsrowrow_sumsum) + (dst_positive_scale_flatten_rowsrowrow_sumsum)) * S ((dst_positive_code_flatten_rowsrowrow_sumsum) + (dst_positive_scale_flatten_rowsrowrow_sumsum)) + ((dst_positive_scale_flatten_rowsrowrow_sumsum) + (dst_positive_scale_flatten_rowsrowrow_sumsum))) + (((dst_negative_code_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)) * S ((dst_negative_code_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)) + ((dst_negative_scale_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)))) * S ((((dst_positive_code_flatten_rowsrowrow_sumsum) + (dst_positive_scale_flatten_rowsrowrow_sumsum)) * S ((dst_positive_code_flatten_rowsrowrow_sumsum) + (dst_positive_scale_flatten_rowsrowrow_sumsum)) + ((dst_positive_scale_flatten_rowsrowrow_sumsum) + (dst_positive_scale_flatten_rowsrowrow_sumsum))) + (((dst_negative_code_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)) * S ((dst_negative_code_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)) + ((dst_negative_scale_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)))) + ((((dst_negative_code_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)) * S ((dst_negative_code_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)) + ((dst_negative_scale_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum))) + (((dst_negative_code_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)) * S ((dst_negative_code_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)) + ((dst_negative_scale_flatten_rowsrowrow_sumsum) + (dst_negative_scale_flatten_rowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_flatten_rowsrowrow_sumsumpositive fs_v_dst_flatten_rowsrowrow_sumsumpositive. ((((exists fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_start. fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_flatten_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_start. fs_u_dst_flatten_rowsrowrow_sumsumpositive = fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_flatten_rowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_terminal. fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_flatten_rowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_flatten_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_terminal. fs_u_dst_flatten_rowsrowrow_sumsumpositive = fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_flatten_rowsrowrow_sumsumpositive) + (dst_positive_sum_flatten_rowsrowrow_sumsum))) /\ forall fs_i_dst_flatten_rowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_flatten_rowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_flatten_rowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_flatten_rowsrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_flatten_rowsrowrow_sumsumpositive_body_steps fs_r_dst_flatten_rowsrowrow_sumsumpositive_body_steps fs_s_dst_flatten_rowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_flatten_rowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_flatten_rowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_flatten_rowsrowrow_sumsum)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_flatten_rowsrowrow_sumsum = fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_flatten_rowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_flatten_rowsrowrow_sumsum) + (fs_a_dst_flatten_rowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_flatten_rowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_flatten_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flatten_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_flatten_rowsrowrow_sumsumpositive = fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_flatten_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flatten_rowsrowrow_sumsumpositive) + (fs_r_dst_flatten_rowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_flatten_rowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_flatten_rowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_flatten_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flatten_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_flatten_rowsrowrow_sumsumpositive = fs_q_dst_flatten_rowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_flatten_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flatten_rowsrowrow_sumsumpositive) + (fs_s_dst_flatten_rowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_flatten_rowsrowrow_sumsumpositive_body_steps = fs_r_dst_flatten_rowsrowrow_sumsumpositive_body_steps + fs_a_dst_flatten_rowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_flatten_rowsrowrow_sumsumnegative fs_v_dst_flatten_rowsrowrow_sumsumnegative. ((((exists fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_start. fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_flatten_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_start. fs_u_dst_flatten_rowsrowrow_sumsumnegative = fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_flatten_rowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_terminal. fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_flatten_rowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_flatten_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_terminal. fs_u_dst_flatten_rowsrowrow_sumsumnegative = fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_flatten_rowsrowrow_sumsumnegative) + (dst_negative_sum_flatten_rowsrowrow_sumsum))) /\ forall fs_i_dst_flatten_rowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_flatten_rowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_flatten_rowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_flatten_rowsrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_flatten_rowsrowrow_sumsumnegative_body_steps fs_r_dst_flatten_rowsrowrow_sumsumnegative_body_steps fs_s_dst_flatten_rowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_flatten_rowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_flatten_rowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_flatten_rowsrowrow_sumsum)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_flatten_rowsrowrow_sumsum = fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_flatten_rowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_flatten_rowsrowrow_sumsum) + (fs_a_dst_flatten_rowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_flatten_rowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_flatten_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flatten_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_flatten_rowsrowrow_sumsumnegative = fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_flatten_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flatten_rowsrowrow_sumsumnegative) + (fs_r_dst_flatten_rowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_flatten_rowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_flatten_rowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_flatten_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flatten_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_flatten_rowsrowrow_sumsumnegative = fs_q_dst_flatten_rowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_flatten_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flatten_rowsrowrow_sumsumnegative) + (fs_s_dst_flatten_rowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_flatten_rowsrowrow_sumsumnegative_body_steps = fs_r_dst_flatten_rowsrowrow_sumsumnegative_body_steps + fs_a_dst_flatten_rowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_flatten_rowsrowrow_sumsumresult ge_balance_negative_flatten_rowsrowrow_sumsumresult. (((((srt_value_flatten_rows) = 2 * (ge_balance_positive_flatten_rowsrowrow_sumsumresult) /\ (ge_balance_negative_flatten_rowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_flatten_rowsrowrow_sumsumresultdecode. (((srt_value_flatten_rows) = 2 * ge_signed_half_flatten_rowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_flatten_rowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_flatten_rowsrowrow_sumsumresult) = S ge_signed_half_flatten_rowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_flatten_rowsrowrow_sumsum) + ge_balance_negative_flatten_rowsrowrow_sumsumresult = (dst_negative_sum_flatten_rowsrowrow_sumsum) + ge_balance_positive_flatten_rowsrowrow_sumsumresult)))))))))))))))))) -> (exists dst_positive_code_flatten_sum dst_positive_scale_flatten_sum dst_negative_code_flatten_sum dst_negative_scale_flatten_sum dst_positive_sum_flatten_sum dst_negative_sum_flatten_sum. (((R) = (((((dst_positive_code_flatten_sum) + (dst_positive_scale_flatten_sum)) * S ((dst_positive_code_flatten_sum) + (dst_positive_scale_flatten_sum)) + ((dst_positive_scale_flatten_sum) + (dst_positive_scale_flatten_sum))) + (((dst_negative_code_flatten_sum) + (dst_negative_scale_flatten_sum)) * S ((dst_negative_code_flatten_sum) + (dst_negative_scale_flatten_sum)) + ((dst_negative_scale_flatten_sum) + (dst_negative_scale_flatten_sum)))) * S ((((dst_positive_code_flatten_sum) + (dst_positive_scale_flatten_sum)) * S ((dst_positive_code_flatten_sum) + (dst_positive_scale_flatten_sum)) + ((dst_positive_scale_flatten_sum) + (dst_positive_scale_flatten_sum))) + (((dst_negative_code_flatten_sum) + (dst_negative_scale_flatten_sum)) * S ((dst_negative_code_flatten_sum) + (dst_negative_scale_flatten_sum)) + ((dst_negative_scale_flatten_sum) + (dst_negative_scale_flatten_sum)))) + ((((dst_negative_code_flatten_sum) + (dst_negative_scale_flatten_sum)) * S ((dst_negative_code_flatten_sum) + (dst_negative_scale_flatten_sum)) + ((dst_negative_scale_flatten_sum) + (dst_negative_scale_flatten_sum))) + (((dst_negative_code_flatten_sum) + (dst_negative_scale_flatten_sum)) * S ((dst_negative_code_flatten_sum) + (dst_negative_scale_flatten_sum)) + ((dst_negative_scale_flatten_sum) + (dst_negative_scale_flatten_sum)))))) /\ (((exists fs_u_dst_flatten_sumpositive fs_v_dst_flatten_sumpositive. ((((exists fs_h_dst_flatten_sumpositive_body_start. fs_h_dst_flatten_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_flatten_sumpositive)) /\ exists fs_q_dst_flatten_sumpositive_body_start. fs_u_dst_flatten_sumpositive = fs_q_dst_flatten_sumpositive_body_start * S ((S (0)) * fs_v_dst_flatten_sumpositive) + (0))) /\ ((((exists fs_h_dst_flatten_sumpositive_body_terminal. fs_h_dst_flatten_sumpositive_body_terminal + S (dst_positive_sum_flatten_sum) = S ((S (m)) * fs_v_dst_flatten_sumpositive)) /\ exists fs_q_dst_flatten_sumpositive_body_terminal. fs_u_dst_flatten_sumpositive = fs_q_dst_flatten_sumpositive_body_terminal * S ((S (m)) * fs_v_dst_flatten_sumpositive) + (dst_positive_sum_flatten_sum))) /\ forall fs_i_dst_flatten_sumpositive_body_steps. (exists fs_lt_dst_flatten_sumpositive_body_steps_bound. fs_lt_dst_flatten_sumpositive_body_steps_bound + S fs_i_dst_flatten_sumpositive_body_steps = m) -> exists fs_a_dst_flatten_sumpositive_body_steps fs_r_dst_flatten_sumpositive_body_steps fs_s_dst_flatten_sumpositive_body_steps. ((((exists fs_h_dst_flatten_sumpositive_body_steps_summand. fs_h_dst_flatten_sumpositive_body_steps_summand + S (fs_a_dst_flatten_sumpositive_body_steps) = S ((S (fs_i_dst_flatten_sumpositive_body_steps)) * dst_positive_scale_flatten_sum)) /\ exists fs_q_dst_flatten_sumpositive_body_steps_summand. dst_positive_code_flatten_sum = fs_q_dst_flatten_sumpositive_body_steps_summand * S ((S (fs_i_dst_flatten_sumpositive_body_steps)) * dst_positive_scale_flatten_sum) + (fs_a_dst_flatten_sumpositive_body_steps))) /\ ((((exists fs_h_dst_flatten_sumpositive_body_steps_partial. fs_h_dst_flatten_sumpositive_body_steps_partial + S (fs_r_dst_flatten_sumpositive_body_steps) = S ((S (fs_i_dst_flatten_sumpositive_body_steps)) * fs_v_dst_flatten_sumpositive)) /\ exists fs_q_dst_flatten_sumpositive_body_steps_partial. fs_u_dst_flatten_sumpositive = fs_q_dst_flatten_sumpositive_body_steps_partial * S ((S (fs_i_dst_flatten_sumpositive_body_steps)) * fs_v_dst_flatten_sumpositive) + (fs_r_dst_flatten_sumpositive_body_steps))) /\ ((((exists fs_h_dst_flatten_sumpositive_body_steps_successor. fs_h_dst_flatten_sumpositive_body_steps_successor + S (fs_s_dst_flatten_sumpositive_body_steps) = S ((S (S fs_i_dst_flatten_sumpositive_body_steps)) * fs_v_dst_flatten_sumpositive)) /\ exists fs_q_dst_flatten_sumpositive_body_steps_successor. fs_u_dst_flatten_sumpositive = fs_q_dst_flatten_sumpositive_body_steps_successor * S ((S (S fs_i_dst_flatten_sumpositive_body_steps)) * fs_v_dst_flatten_sumpositive) + (fs_s_dst_flatten_sumpositive_body_steps))) /\ fs_s_dst_flatten_sumpositive_body_steps = fs_r_dst_flatten_sumpositive_body_steps + fs_a_dst_flatten_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_flatten_sumnegative fs_v_dst_flatten_sumnegative. ((((exists fs_h_dst_flatten_sumnegative_body_start. fs_h_dst_flatten_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_flatten_sumnegative)) /\ exists fs_q_dst_flatten_sumnegative_body_start. fs_u_dst_flatten_sumnegative = fs_q_dst_flatten_sumnegative_body_start * S ((S (0)) * fs_v_dst_flatten_sumnegative) + (0))) /\ ((((exists fs_h_dst_flatten_sumnegative_body_terminal. fs_h_dst_flatten_sumnegative_body_terminal + S (dst_negative_sum_flatten_sum) = S ((S (m)) * fs_v_dst_flatten_sumnegative)) /\ exists fs_q_dst_flatten_sumnegative_body_terminal. fs_u_dst_flatten_sumnegative = fs_q_dst_flatten_sumnegative_body_terminal * S ((S (m)) * fs_v_dst_flatten_sumnegative) + (dst_negative_sum_flatten_sum))) /\ forall fs_i_dst_flatten_sumnegative_body_steps. (exists fs_lt_dst_flatten_sumnegative_body_steps_bound. fs_lt_dst_flatten_sumnegative_body_steps_bound + S fs_i_dst_flatten_sumnegative_body_steps = m) -> exists fs_a_dst_flatten_sumnegative_body_steps fs_r_dst_flatten_sumnegative_body_steps fs_s_dst_flatten_sumnegative_body_steps. ((((exists fs_h_dst_flatten_sumnegative_body_steps_summand. fs_h_dst_flatten_sumnegative_body_steps_summand + S (fs_a_dst_flatten_sumnegative_body_steps) = S ((S (fs_i_dst_flatten_sumnegative_body_steps)) * dst_negative_scale_flatten_sum)) /\ exists fs_q_dst_flatten_sumnegative_body_steps_summand. dst_negative_code_flatten_sum = fs_q_dst_flatten_sumnegative_body_steps_summand * S ((S (fs_i_dst_flatten_sumnegative_body_steps)) * dst_negative_scale_flatten_sum) + (fs_a_dst_flatten_sumnegative_body_steps))) /\ ((((exists fs_h_dst_flatten_sumnegative_body_steps_partial. fs_h_dst_flatten_sumnegative_body_steps_partial + S (fs_r_dst_flatten_sumnegative_body_steps) = S ((S (fs_i_dst_flatten_sumnegative_body_steps)) * fs_v_dst_flatten_sumnegative)) /\ exists fs_q_dst_flatten_sumnegative_body_steps_partial. fs_u_dst_flatten_sumnegative = fs_q_dst_flatten_sumnegative_body_steps_partial * S ((S (fs_i_dst_flatten_sumnegative_body_steps)) * fs_v_dst_flatten_sumnegative) + (fs_r_dst_flatten_sumnegative_body_steps))) /\ ((((exists fs_h_dst_flatten_sumnegative_body_steps_successor. fs_h_dst_flatten_sumnegative_body_steps_successor + S (fs_s_dst_flatten_sumnegative_body_steps) = S ((S (S fs_i_dst_flatten_sumnegative_body_steps)) * fs_v_dst_flatten_sumnegative)) /\ exists fs_q_dst_flatten_sumnegative_body_steps_successor. fs_u_dst_flatten_sumnegative = fs_q_dst_flatten_sumnegative_body_steps_successor * S ((S (S fs_i_dst_flatten_sumnegative_body_steps)) * fs_v_dst_flatten_sumnegative) + (fs_s_dst_flatten_sumnegative_body_steps))) /\ fs_s_dst_flatten_sumnegative_body_steps = fs_r_dst_flatten_sumnegative_body_steps + fs_a_dst_flatten_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_flatten_sumresult ge_balance_negative_flatten_sumresult. (((((z) = 2 * (ge_balance_positive_flatten_sumresult) /\ (ge_balance_negative_flatten_sumresult) = 0) \/ exists ge_signed_half_flatten_sumresultdecode. (((z) = 2 * ge_signed_half_flatten_sumresultdecode + 1 /\ (ge_balance_positive_flatten_sumresult) = 0) /\ (ge_balance_negative_flatten_sumresult) = S ge_signed_half_flatten_sumresultdecode))) /\ ((dst_positive_sum_flatten_sum) + ge_balance_negative_flatten_sumresult = (dst_negative_sum_flatten_sum) + ge_balance_positive_flatten_sumresult))))))))) -> (exists srs_slice_flatten_result. ((((exists dst_positive_code_flatten_resultslicesource_table dst_positive_scale_flatten_resultslicesource_table dst_negative_code_flatten_resultslicesource_table dst_negative_scale_flatten_resultslicesource_table. (((F) = (((((dst_positive_code_flatten_resultslicesource_table) + (dst_positive_scale_flatten_resultslicesource_table)) * S ((dst_positive_code_flatten_resultslicesource_table) + (dst_positive_scale_flatten_resultslicesource_table)) + ((dst_positive_scale_flatten_resultslicesource_table) + (dst_positive_scale_flatten_resultslicesource_table))) + (((dst_negative_code_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)) * S ((dst_negative_code_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)) + ((dst_negative_scale_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)))) * S ((((dst_positive_code_flatten_resultslicesource_table) + (dst_positive_scale_flatten_resultslicesource_table)) * S ((dst_positive_code_flatten_resultslicesource_table) + (dst_positive_scale_flatten_resultslicesource_table)) + ((dst_positive_scale_flatten_resultslicesource_table) + (dst_positive_scale_flatten_resultslicesource_table))) + (((dst_negative_code_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)) * S ((dst_negative_code_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)) + ((dst_negative_scale_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)))) + ((((dst_negative_code_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)) * S ((dst_negative_code_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)) + ((dst_negative_scale_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table))) + (((dst_negative_code_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)) * S ((dst_negative_code_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)) + ((dst_negative_scale_flatten_resultslicesource_table) + (dst_negative_scale_flatten_resultslicesource_table)))))) /\ (forall dst_index_flatten_resultslicesource_table. (exists pvs_le_gap_flatten_resultslicesource_tabledomain. pvs_le_gap_flatten_resultslicesource_tabledomain + (dst_index_flatten_resultslicesource_table) = (0)) -> exists dst_positive_flatten_resultslicesource_table dst_negative_flatten_resultslicesource_table dst_value_flatten_resultslicesource_table. ((((exists ff_h_pvs_flatten_resultslicesource_tableentrypositive. ff_h_pvs_flatten_resultslicesource_tableentrypositive + S (dst_positive_flatten_resultslicesource_table) = S ((S (dst_index_flatten_resultslicesource_table)) * dst_positive_scale_flatten_resultslicesource_table)) /\ exists ff_q_pvs_flatten_resultslicesource_tableentrypositive. dst_positive_code_flatten_resultslicesource_table = ff_q_pvs_flatten_resultslicesource_tableentrypositive * S ((S (dst_index_flatten_resultslicesource_table)) * dst_positive_scale_flatten_resultslicesource_table) + (dst_positive_flatten_resultslicesource_table))) /\ (((((exists ff_h_pvs_flatten_resultslicesource_tableentrynegative. ff_h_pvs_flatten_resultslicesource_tableentrynegative + S (dst_negative_flatten_resultslicesource_table) = S ((S (dst_index_flatten_resultslicesource_table)) * dst_negative_scale_flatten_resultslicesource_table)) /\ exists ff_q_pvs_flatten_resultslicesource_tableentrynegative. dst_negative_code_flatten_resultslicesource_table = ff_q_pvs_flatten_resultslicesource_tableentrynegative * S ((S (dst_index_flatten_resultslicesource_table)) * dst_negative_scale_flatten_resultslicesource_table) + (dst_negative_flatten_resultslicesource_table))) /\ (exists ge_balance_positive_flatten_resultslicesource_tableentryvalue ge_balance_negative_flatten_resultslicesource_tableentryvalue. (((((dst_value_flatten_resultslicesource_table) = 2 * (ge_balance_positive_flatten_resultslicesource_tableentryvalue) /\ (ge_balance_negative_flatten_resultslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_flatten_resultslicesource_tableentryvaluedecode. (((dst_value_flatten_resultslicesource_table) = 2 * ge_signed_half_flatten_resultslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_flatten_resultslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_flatten_resultslicesource_tableentryvalue) = S ge_signed_half_flatten_resultslicesource_tableentryvaluedecode))) /\ ((dst_positive_flatten_resultslicesource_table) + ge_balance_negative_flatten_resultslicesource_tableentryvalue = (dst_negative_flatten_resultslicesource_table) + ge_balance_positive_flatten_resultslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_flatten_resultsliceoutput_table dst_positive_scale_flatten_resultsliceoutput_table dst_negative_code_flatten_resultsliceoutput_table dst_negative_scale_flatten_resultsliceoutput_table. (((srs_slice_flatten_result) = (((((dst_positive_code_flatten_resultsliceoutput_table) + (dst_positive_scale_flatten_resultsliceoutput_table)) * S ((dst_positive_code_flatten_resultsliceoutput_table) + (dst_positive_scale_flatten_resultsliceoutput_table)) + ((dst_positive_scale_flatten_resultsliceoutput_table) + (dst_positive_scale_flatten_resultsliceoutput_table))) + (((dst_negative_code_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)) * S ((dst_negative_code_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)) + ((dst_negative_scale_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)))) * S ((((dst_positive_code_flatten_resultsliceoutput_table) + (dst_positive_scale_flatten_resultsliceoutput_table)) * S ((dst_positive_code_flatten_resultsliceoutput_table) + (dst_positive_scale_flatten_resultsliceoutput_table)) + ((dst_positive_scale_flatten_resultsliceoutput_table) + (dst_positive_scale_flatten_resultsliceoutput_table))) + (((dst_negative_code_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)) * S ((dst_negative_code_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)) + ((dst_negative_scale_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)))) + ((((dst_negative_code_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)) * S ((dst_negative_code_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)) + ((dst_negative_scale_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table))) + (((dst_negative_code_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)) * S ((dst_negative_code_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)) + ((dst_negative_scale_flatten_resultsliceoutput_table) + (dst_negative_scale_flatten_resultsliceoutput_table)))))) /\ (forall dst_index_flatten_resultsliceoutput_table. (exists pvs_le_gap_flatten_resultsliceoutput_tabledomain. pvs_le_gap_flatten_resultsliceoutput_tabledomain + (dst_index_flatten_resultsliceoutput_table) = (m*n)) -> exists dst_positive_flatten_resultsliceoutput_table dst_negative_flatten_resultsliceoutput_table dst_value_flatten_resultsliceoutput_table. ((((exists ff_h_pvs_flatten_resultsliceoutput_tableentrypositive. ff_h_pvs_flatten_resultsliceoutput_tableentrypositive + S (dst_positive_flatten_resultsliceoutput_table) = S ((S (dst_index_flatten_resultsliceoutput_table)) * dst_positive_scale_flatten_resultsliceoutput_table)) /\ exists ff_q_pvs_flatten_resultsliceoutput_tableentrypositive. dst_positive_code_flatten_resultsliceoutput_table = ff_q_pvs_flatten_resultsliceoutput_tableentrypositive * S ((S (dst_index_flatten_resultsliceoutput_table)) * dst_positive_scale_flatten_resultsliceoutput_table) + (dst_positive_flatten_resultsliceoutput_table))) /\ (((((exists ff_h_pvs_flatten_resultsliceoutput_tableentrynegative. ff_h_pvs_flatten_resultsliceoutput_tableentrynegative + S (dst_negative_flatten_resultsliceoutput_table) = S ((S (dst_index_flatten_resultsliceoutput_table)) * dst_negative_scale_flatten_resultsliceoutput_table)) /\ exists ff_q_pvs_flatten_resultsliceoutput_tableentrynegative. dst_negative_code_flatten_resultsliceoutput_table = ff_q_pvs_flatten_resultsliceoutput_tableentrynegative * S ((S (dst_index_flatten_resultsliceoutput_table)) * dst_negative_scale_flatten_resultsliceoutput_table) + (dst_negative_flatten_resultsliceoutput_table))) /\ (exists ge_balance_positive_flatten_resultsliceoutput_tableentryvalue ge_balance_negative_flatten_resultsliceoutput_tableentryvalue. (((((dst_value_flatten_resultsliceoutput_table) = 2 * (ge_balance_positive_flatten_resultsliceoutput_tableentryvalue) /\ (ge_balance_negative_flatten_resultsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_flatten_resultsliceoutput_tableentryvaluedecode. (((dst_value_flatten_resultsliceoutput_table) = 2 * ge_signed_half_flatten_resultsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_flatten_resultsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_flatten_resultsliceoutput_tableentryvalue) = S ge_signed_half_flatten_resultsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_flatten_resultsliceoutput_table) + ge_balance_negative_flatten_resultsliceoutput_tableentryvalue = (dst_negative_flatten_resultsliceoutput_table) + ge_balance_positive_flatten_resultsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_flatten_resultslice. (exists pvs_gap_flatten_resultslicebound. pvs_gap_flatten_resultslicebound + S (srs_index_flatten_resultslice) = (m*n)) -> exists srs_value_flatten_resultslice. (((exists dst_positive_code_flatten_resultsliceentrysource dst_positive_scale_flatten_resultsliceentrysource dst_negative_code_flatten_resultsliceentrysource dst_negative_scale_flatten_resultsliceentrysource dst_positive_flatten_resultsliceentrysource dst_negative_flatten_resultsliceentrysource. (((F) = (((((dst_positive_code_flatten_resultsliceentrysource) + (dst_positive_scale_flatten_resultsliceentrysource)) * S ((dst_positive_code_flatten_resultsliceentrysource) + (dst_positive_scale_flatten_resultsliceentrysource)) + ((dst_positive_scale_flatten_resultsliceentrysource) + (dst_positive_scale_flatten_resultsliceentrysource))) + (((dst_negative_code_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)) * S ((dst_negative_code_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)) + ((dst_negative_scale_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)))) * S ((((dst_positive_code_flatten_resultsliceentrysource) + (dst_positive_scale_flatten_resultsliceentrysource)) * S ((dst_positive_code_flatten_resultsliceentrysource) + (dst_positive_scale_flatten_resultsliceentrysource)) + ((dst_positive_scale_flatten_resultsliceentrysource) + (dst_positive_scale_flatten_resultsliceentrysource))) + (((dst_negative_code_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)) * S ((dst_negative_code_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)) + ((dst_negative_scale_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)))) + ((((dst_negative_code_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)) * S ((dst_negative_code_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)) + ((dst_negative_scale_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource))) + (((dst_negative_code_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)) * S ((dst_negative_code_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)) + ((dst_negative_scale_flatten_resultsliceentrysource) + (dst_negative_scale_flatten_resultsliceentrysource)))))) /\ (((((exists ff_h_pvs_flatten_resultsliceentrysourcepositive. ff_h_pvs_flatten_resultsliceentrysourcepositive + S (dst_positive_flatten_resultsliceentrysource) = S ((S (((0) + ((1) * (srs_index_flatten_resultslice))))) * dst_positive_scale_flatten_resultsliceentrysource)) /\ exists ff_q_pvs_flatten_resultsliceentrysourcepositive. dst_positive_code_flatten_resultsliceentrysource = ff_q_pvs_flatten_resultsliceentrysourcepositive * S ((S (((0) + ((1) * (srs_index_flatten_resultslice))))) * dst_positive_scale_flatten_resultsliceentrysource) + (dst_positive_flatten_resultsliceentrysource))) /\ (((((exists ff_h_pvs_flatten_resultsliceentrysourcenegative. ff_h_pvs_flatten_resultsliceentrysourcenegative + S (dst_negative_flatten_resultsliceentrysource) = S ((S (((0) + ((1) * (srs_index_flatten_resultslice))))) * dst_negative_scale_flatten_resultsliceentrysource)) /\ exists ff_q_pvs_flatten_resultsliceentrysourcenegative. dst_negative_code_flatten_resultsliceentrysource = ff_q_pvs_flatten_resultsliceentrysourcenegative * S ((S (((0) + ((1) * (srs_index_flatten_resultslice))))) * dst_negative_scale_flatten_resultsliceentrysource) + (dst_negative_flatten_resultsliceentrysource))) /\ (exists ge_balance_positive_flatten_resultsliceentrysourcevalue ge_balance_negative_flatten_resultsliceentrysourcevalue. (((((srs_value_flatten_resultslice) = 2 * (ge_balance_positive_flatten_resultsliceentrysourcevalue) /\ (ge_balance_negative_flatten_resultsliceentrysourcevalue) = 0) \/ exists ge_signed_half_flatten_resultsliceentrysourcevaluedecode. (((srs_value_flatten_resultslice) = 2 * ge_signed_half_flatten_resultsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_flatten_resultsliceentrysourcevalue) = 0) /\ (ge_balance_negative_flatten_resultsliceentrysourcevalue) = S ge_signed_half_flatten_resultsliceentrysourcevaluedecode))) /\ ((dst_positive_flatten_resultsliceentrysource) + ge_balance_negative_flatten_resultsliceentrysourcevalue = (dst_negative_flatten_resultsliceentrysource) + ge_balance_positive_flatten_resultsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_flatten_resultsliceentryoutput dst_positive_scale_flatten_resultsliceentryoutput dst_negative_code_flatten_resultsliceentryoutput dst_negative_scale_flatten_resultsliceentryoutput dst_positive_flatten_resultsliceentryoutput dst_negative_flatten_resultsliceentryoutput. (((srs_slice_flatten_result) = (((((dst_positive_code_flatten_resultsliceentryoutput) + (dst_positive_scale_flatten_resultsliceentryoutput)) * S ((dst_positive_code_flatten_resultsliceentryoutput) + (dst_positive_scale_flatten_resultsliceentryoutput)) + ((dst_positive_scale_flatten_resultsliceentryoutput) + (dst_positive_scale_flatten_resultsliceentryoutput))) + (((dst_negative_code_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)) * S ((dst_negative_code_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)) + ((dst_negative_scale_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)))) * S ((((dst_positive_code_flatten_resultsliceentryoutput) + (dst_positive_scale_flatten_resultsliceentryoutput)) * S ((dst_positive_code_flatten_resultsliceentryoutput) + (dst_positive_scale_flatten_resultsliceentryoutput)) + ((dst_positive_scale_flatten_resultsliceentryoutput) + (dst_positive_scale_flatten_resultsliceentryoutput))) + (((dst_negative_code_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)) * S ((dst_negative_code_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)) + ((dst_negative_scale_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)))) + ((((dst_negative_code_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)) * S ((dst_negative_code_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)) + ((dst_negative_scale_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput))) + (((dst_negative_code_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)) * S ((dst_negative_code_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)) + ((dst_negative_scale_flatten_resultsliceentryoutput) + (dst_negative_scale_flatten_resultsliceentryoutput)))))) /\ (((((exists ff_h_pvs_flatten_resultsliceentryoutputpositive. ff_h_pvs_flatten_resultsliceentryoutputpositive + S (dst_positive_flatten_resultsliceentryoutput) = S ((S (srs_index_flatten_resultslice)) * dst_positive_scale_flatten_resultsliceentryoutput)) /\ exists ff_q_pvs_flatten_resultsliceentryoutputpositive. dst_positive_code_flatten_resultsliceentryoutput = ff_q_pvs_flatten_resultsliceentryoutputpositive * S ((S (srs_index_flatten_resultslice)) * dst_positive_scale_flatten_resultsliceentryoutput) + (dst_positive_flatten_resultsliceentryoutput))) /\ (((((exists ff_h_pvs_flatten_resultsliceentryoutputnegative. ff_h_pvs_flatten_resultsliceentryoutputnegative + S (dst_negative_flatten_resultsliceentryoutput) = S ((S (srs_index_flatten_resultslice)) * dst_negative_scale_flatten_resultsliceentryoutput)) /\ exists ff_q_pvs_flatten_resultsliceentryoutputnegative. dst_negative_code_flatten_resultsliceentryoutput = ff_q_pvs_flatten_resultsliceentryoutputnegative * S ((S (srs_index_flatten_resultslice)) * dst_negative_scale_flatten_resultsliceentryoutput) + (dst_negative_flatten_resultsliceentryoutput))) /\ (exists ge_balance_positive_flatten_resultsliceentryoutputvalue ge_balance_negative_flatten_resultsliceentryoutputvalue. (((((srs_value_flatten_resultslice) = 2 * (ge_balance_positive_flatten_resultsliceentryoutputvalue) /\ (ge_balance_negative_flatten_resultsliceentryoutputvalue) = 0) \/ exists ge_signed_half_flatten_resultsliceentryoutputvaluedecode. (((srs_value_flatten_resultslice) = 2 * ge_signed_half_flatten_resultsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_flatten_resultsliceentryoutputvalue) = 0) /\ (ge_balance_negative_flatten_resultsliceentryoutputvalue) = S ge_signed_half_flatten_resultsliceentryoutputvaluedecode))) /\ ((dst_positive_flatten_resultsliceentryoutput) + ge_balance_negative_flatten_resultsliceentryoutputvalue = (dst_negative_flatten_resultsliceentryoutput) + ge_balance_positive_flatten_resultsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_flatten_resultsum dst_positive_scale_flatten_resultsum dst_negative_code_flatten_resultsum dst_negative_scale_flatten_resultsum dst_positive_sum_flatten_resultsum dst_negative_sum_flatten_resultsum. (((srs_slice_flatten_result) = (((((dst_positive_code_flatten_resultsum) + (dst_positive_scale_flatten_resultsum)) * S ((dst_positive_code_flatten_resultsum) + (dst_positive_scale_flatten_resultsum)) + ((dst_positive_scale_flatten_resultsum) + (dst_positive_scale_flatten_resultsum))) + (((dst_negative_code_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)) * S ((dst_negative_code_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)) + ((dst_negative_scale_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)))) * S ((((dst_positive_code_flatten_resultsum) + (dst_positive_scale_flatten_resultsum)) * S ((dst_positive_code_flatten_resultsum) + (dst_positive_scale_flatten_resultsum)) + ((dst_positive_scale_flatten_resultsum) + (dst_positive_scale_flatten_resultsum))) + (((dst_negative_code_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)) * S ((dst_negative_code_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)) + ((dst_negative_scale_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)))) + ((((dst_negative_code_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)) * S ((dst_negative_code_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)) + ((dst_negative_scale_flatten_resultsum) + (dst_negative_scale_flatten_resultsum))) + (((dst_negative_code_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)) * S ((dst_negative_code_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)) + ((dst_negative_scale_flatten_resultsum) + (dst_negative_scale_flatten_resultsum)))))) /\ (((exists fs_u_dst_flatten_resultsumpositive fs_v_dst_flatten_resultsumpositive. ((((exists fs_h_dst_flatten_resultsumpositive_body_start. fs_h_dst_flatten_resultsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_flatten_resultsumpositive)) /\ exists fs_q_dst_flatten_resultsumpositive_body_start. fs_u_dst_flatten_resultsumpositive = fs_q_dst_flatten_resultsumpositive_body_start * S ((S (0)) * fs_v_dst_flatten_resultsumpositive) + (0))) /\ ((((exists fs_h_dst_flatten_resultsumpositive_body_terminal. fs_h_dst_flatten_resultsumpositive_body_terminal + S (dst_positive_sum_flatten_resultsum) = S ((S (m*n)) * fs_v_dst_flatten_resultsumpositive)) /\ exists fs_q_dst_flatten_resultsumpositive_body_terminal. fs_u_dst_flatten_resultsumpositive = fs_q_dst_flatten_resultsumpositive_body_terminal * S ((S (m*n)) * fs_v_dst_flatten_resultsumpositive) + (dst_positive_sum_flatten_resultsum))) /\ forall fs_i_dst_flatten_resultsumpositive_body_steps. (exists fs_lt_dst_flatten_resultsumpositive_body_steps_bound. fs_lt_dst_flatten_resultsumpositive_body_steps_bound + S fs_i_dst_flatten_resultsumpositive_body_steps = m*n) -> exists fs_a_dst_flatten_resultsumpositive_body_steps fs_r_dst_flatten_resultsumpositive_body_steps fs_s_dst_flatten_resultsumpositive_body_steps. ((((exists fs_h_dst_flatten_resultsumpositive_body_steps_summand. fs_h_dst_flatten_resultsumpositive_body_steps_summand + S (fs_a_dst_flatten_resultsumpositive_body_steps) = S ((S (fs_i_dst_flatten_resultsumpositive_body_steps)) * dst_positive_scale_flatten_resultsum)) /\ exists fs_q_dst_flatten_resultsumpositive_body_steps_summand. dst_positive_code_flatten_resultsum = fs_q_dst_flatten_resultsumpositive_body_steps_summand * S ((S (fs_i_dst_flatten_resultsumpositive_body_steps)) * dst_positive_scale_flatten_resultsum) + (fs_a_dst_flatten_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_flatten_resultsumpositive_body_steps_partial. fs_h_dst_flatten_resultsumpositive_body_steps_partial + S (fs_r_dst_flatten_resultsumpositive_body_steps) = S ((S (fs_i_dst_flatten_resultsumpositive_body_steps)) * fs_v_dst_flatten_resultsumpositive)) /\ exists fs_q_dst_flatten_resultsumpositive_body_steps_partial. fs_u_dst_flatten_resultsumpositive = fs_q_dst_flatten_resultsumpositive_body_steps_partial * S ((S (fs_i_dst_flatten_resultsumpositive_body_steps)) * fs_v_dst_flatten_resultsumpositive) + (fs_r_dst_flatten_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_flatten_resultsumpositive_body_steps_successor. fs_h_dst_flatten_resultsumpositive_body_steps_successor + S (fs_s_dst_flatten_resultsumpositive_body_steps) = S ((S (S fs_i_dst_flatten_resultsumpositive_body_steps)) * fs_v_dst_flatten_resultsumpositive)) /\ exists fs_q_dst_flatten_resultsumpositive_body_steps_successor. fs_u_dst_flatten_resultsumpositive = fs_q_dst_flatten_resultsumpositive_body_steps_successor * S ((S (S fs_i_dst_flatten_resultsumpositive_body_steps)) * fs_v_dst_flatten_resultsumpositive) + (fs_s_dst_flatten_resultsumpositive_body_steps))) /\ fs_s_dst_flatten_resultsumpositive_body_steps = fs_r_dst_flatten_resultsumpositive_body_steps + fs_a_dst_flatten_resultsumpositive_body_steps)))))) /\ (((exists fs_u_dst_flatten_resultsumnegative fs_v_dst_flatten_resultsumnegative. ((((exists fs_h_dst_flatten_resultsumnegative_body_start. fs_h_dst_flatten_resultsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_flatten_resultsumnegative)) /\ exists fs_q_dst_flatten_resultsumnegative_body_start. fs_u_dst_flatten_resultsumnegative = fs_q_dst_flatten_resultsumnegative_body_start * S ((S (0)) * fs_v_dst_flatten_resultsumnegative) + (0))) /\ ((((exists fs_h_dst_flatten_resultsumnegative_body_terminal. fs_h_dst_flatten_resultsumnegative_body_terminal + S (dst_negative_sum_flatten_resultsum) = S ((S (m*n)) * fs_v_dst_flatten_resultsumnegative)) /\ exists fs_q_dst_flatten_resultsumnegative_body_terminal. fs_u_dst_flatten_resultsumnegative = fs_q_dst_flatten_resultsumnegative_body_terminal * S ((S (m*n)) * fs_v_dst_flatten_resultsumnegative) + (dst_negative_sum_flatten_resultsum))) /\ forall fs_i_dst_flatten_resultsumnegative_body_steps. (exists fs_lt_dst_flatten_resultsumnegative_body_steps_bound. fs_lt_dst_flatten_resultsumnegative_body_steps_bound + S fs_i_dst_flatten_resultsumnegative_body_steps = m*n) -> exists fs_a_dst_flatten_resultsumnegative_body_steps fs_r_dst_flatten_resultsumnegative_body_steps fs_s_dst_flatten_resultsumnegative_body_steps. ((((exists fs_h_dst_flatten_resultsumnegative_body_steps_summand. fs_h_dst_flatten_resultsumnegative_body_steps_summand + S (fs_a_dst_flatten_resultsumnegative_body_steps) = S ((S (fs_i_dst_flatten_resultsumnegative_body_steps)) * dst_negative_scale_flatten_resultsum)) /\ exists fs_q_dst_flatten_resultsumnegative_body_steps_summand. dst_negative_code_flatten_resultsum = fs_q_dst_flatten_resultsumnegative_body_steps_summand * S ((S (fs_i_dst_flatten_resultsumnegative_body_steps)) * dst_negative_scale_flatten_resultsum) + (fs_a_dst_flatten_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_flatten_resultsumnegative_body_steps_partial. fs_h_dst_flatten_resultsumnegative_body_steps_partial + S (fs_r_dst_flatten_resultsumnegative_body_steps) = S ((S (fs_i_dst_flatten_resultsumnegative_body_steps)) * fs_v_dst_flatten_resultsumnegative)) /\ exists fs_q_dst_flatten_resultsumnegative_body_steps_partial. fs_u_dst_flatten_resultsumnegative = fs_q_dst_flatten_resultsumnegative_body_steps_partial * S ((S (fs_i_dst_flatten_resultsumnegative_body_steps)) * fs_v_dst_flatten_resultsumnegative) + (fs_r_dst_flatten_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_flatten_resultsumnegative_body_steps_successor. fs_h_dst_flatten_resultsumnegative_body_steps_successor + S (fs_s_dst_flatten_resultsumnegative_body_steps) = S ((S (S fs_i_dst_flatten_resultsumnegative_body_steps)) * fs_v_dst_flatten_resultsumnegative)) /\ exists fs_q_dst_flatten_resultsumnegative_body_steps_successor. fs_u_dst_flatten_resultsumnegative = fs_q_dst_flatten_resultsumnegative_body_steps_successor * S ((S (S fs_i_dst_flatten_resultsumnegative_body_steps)) * fs_v_dst_flatten_resultsumnegative) + (fs_s_dst_flatten_resultsumnegative_body_steps))) /\ fs_s_dst_flatten_resultsumnegative_body_steps = fs_r_dst_flatten_resultsumnegative_body_steps + fs_a_dst_flatten_resultsumnegative_body_steps)))))) /\ (exists ge_balance_positive_flatten_resultsumresult ge_balance_negative_flatten_resultsumresult. (((((z) = 2 * (ge_balance_positive_flatten_resultsumresult) /\ (ge_balance_negative_flatten_resultsumresult) = 0) \/ exists ge_signed_half_flatten_resultsumresultdecode. (((z) = 2 * ge_signed_half_flatten_resultsumresultdecode + 1 /\ (ge_balance_positive_flatten_resultsumresult) = 0) /\ (ge_balance_negative_flatten_resultsumresult) = S ge_signed_half_flatten_resultsumresultdecode))) /\ ((dst_positive_sum_flatten_resultsum) + ge_balance_negative_flatten_resultsumresult = (dst_negative_sum_flatten_resultsum) + ge_balance_positive_flatten_resultsumresult)))))))))))