signed_rectangular_fubini

Exact expanded first-order arithmetic statement

forall m F o s t n a b. (exists srt_rows_fubini_rows. ((((exists dst_positive_code_fubini_rowsrowssource_table dst_positive_scale_fubini_rowsrowssource_table dst_negative_code_fubini_rowsrowssource_table dst_negative_scale_fubini_rowsrowssource_table. (((F) = (((((dst_positive_code_fubini_rowsrowssource_table) + (dst_positive_scale_fubini_rowsrowssource_table)) * S ((dst_positive_code_fubini_rowsrowssource_table) + (dst_positive_scale_fubini_rowsrowssource_table)) + ((dst_positive_scale_fubini_rowsrowssource_table) + (dst_positive_scale_fubini_rowsrowssource_table))) + (((dst_negative_code_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)) * S ((dst_negative_code_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)) + ((dst_negative_scale_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)))) * S ((((dst_positive_code_fubini_rowsrowssource_table) + (dst_positive_scale_fubini_rowsrowssource_table)) * S ((dst_positive_code_fubini_rowsrowssource_table) + (dst_positive_scale_fubini_rowsrowssource_table)) + ((dst_positive_scale_fubini_rowsrowssource_table) + (dst_positive_scale_fubini_rowsrowssource_table))) + (((dst_negative_code_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)) * S ((dst_negative_code_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)) + ((dst_negative_scale_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)))) + ((((dst_negative_code_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)) * S ((dst_negative_code_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)) + ((dst_negative_scale_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table))) + (((dst_negative_code_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)) * S ((dst_negative_code_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)) + ((dst_negative_scale_fubini_rowsrowssource_table) + (dst_negative_scale_fubini_rowsrowssource_table)))))) /\ (forall dst_index_fubini_rowsrowssource_table. (exists pvs_le_gap_fubini_rowsrowssource_tabledomain. pvs_le_gap_fubini_rowsrowssource_tabledomain + (dst_index_fubini_rowsrowssource_table) = (0)) -> exists dst_positive_fubini_rowsrowssource_table dst_negative_fubini_rowsrowssource_table dst_value_fubini_rowsrowssource_table. ((((exists ff_h_pvs_fubini_rowsrowssource_tableentrypositive. ff_h_pvs_fubini_rowsrowssource_tableentrypositive + S (dst_positive_fubini_rowsrowssource_table) = S ((S (dst_index_fubini_rowsrowssource_table)) * dst_positive_scale_fubini_rowsrowssource_table)) /\ exists ff_q_pvs_fubini_rowsrowssource_tableentrypositive. dst_positive_code_fubini_rowsrowssource_table = ff_q_pvs_fubini_rowsrowssource_tableentrypositive * S ((S (dst_index_fubini_rowsrowssource_table)) * dst_positive_scale_fubini_rowsrowssource_table) + (dst_positive_fubini_rowsrowssource_table))) /\ (((((exists ff_h_pvs_fubini_rowsrowssource_tableentrynegative. ff_h_pvs_fubini_rowsrowssource_tableentrynegative + S (dst_negative_fubini_rowsrowssource_table) = S ((S (dst_index_fubini_rowsrowssource_table)) * dst_negative_scale_fubini_rowsrowssource_table)) /\ exists ff_q_pvs_fubini_rowsrowssource_tableentrynegative. dst_negative_code_fubini_rowsrowssource_table = ff_q_pvs_fubini_rowsrowssource_tableentrynegative * S ((S (dst_index_fubini_rowsrowssource_table)) * dst_negative_scale_fubini_rowsrowssource_table) + (dst_negative_fubini_rowsrowssource_table))) /\ (exists ge_balance_positive_fubini_rowsrowssource_tableentryvalue ge_balance_negative_fubini_rowsrowssource_tableentryvalue. (((((dst_value_fubini_rowsrowssource_table) = 2 * (ge_balance_positive_fubini_rowsrowssource_tableentryvalue) /\ (ge_balance_negative_fubini_rowsrowssource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_rowsrowssource_tableentryvaluedecode. (((dst_value_fubini_rowsrowssource_table) = 2 * ge_signed_half_fubini_rowsrowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_rowsrowssource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_rowsrowssource_tableentryvalue) = S ge_signed_half_fubini_rowsrowssource_tableentryvaluedecode))) /\ ((dst_positive_fubini_rowsrowssource_table) + ge_balance_negative_fubini_rowsrowssource_tableentryvalue = (dst_negative_fubini_rowsrowssource_table) + ge_balance_positive_fubini_rowsrowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_rowsrowsrow_table dst_positive_scale_fubini_rowsrowsrow_table dst_negative_code_fubini_rowsrowsrow_table dst_negative_scale_fubini_rowsrowsrow_table. (((srt_rows_fubini_rows) = (((((dst_positive_code_fubini_rowsrowsrow_table) + (dst_positive_scale_fubini_rowsrowsrow_table)) * S ((dst_positive_code_fubini_rowsrowsrow_table) + (dst_positive_scale_fubini_rowsrowsrow_table)) + ((dst_positive_scale_fubini_rowsrowsrow_table) + (dst_positive_scale_fubini_rowsrowsrow_table))) + (((dst_negative_code_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)) * S ((dst_negative_code_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)) + ((dst_negative_scale_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)))) * S ((((dst_positive_code_fubini_rowsrowsrow_table) + (dst_positive_scale_fubini_rowsrowsrow_table)) * S ((dst_positive_code_fubini_rowsrowsrow_table) + (dst_positive_scale_fubini_rowsrowsrow_table)) + ((dst_positive_scale_fubini_rowsrowsrow_table) + (dst_positive_scale_fubini_rowsrowsrow_table))) + (((dst_negative_code_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)) * S ((dst_negative_code_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)) + ((dst_negative_scale_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)))) + ((((dst_negative_code_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)) * S ((dst_negative_code_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)) + ((dst_negative_scale_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table))) + (((dst_negative_code_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)) * S ((dst_negative_code_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)) + ((dst_negative_scale_fubini_rowsrowsrow_table) + (dst_negative_scale_fubini_rowsrowsrow_table)))))) /\ (forall dst_index_fubini_rowsrowsrow_table. (exists pvs_le_gap_fubini_rowsrowsrow_tabledomain. pvs_le_gap_fubini_rowsrowsrow_tabledomain + (dst_index_fubini_rowsrowsrow_table) = (m)) -> exists dst_positive_fubini_rowsrowsrow_table dst_negative_fubini_rowsrowsrow_table dst_value_fubini_rowsrowsrow_table. ((((exists ff_h_pvs_fubini_rowsrowsrow_tableentrypositive. ff_h_pvs_fubini_rowsrowsrow_tableentrypositive + S (dst_positive_fubini_rowsrowsrow_table) = S ((S (dst_index_fubini_rowsrowsrow_table)) * dst_positive_scale_fubini_rowsrowsrow_table)) /\ exists ff_q_pvs_fubini_rowsrowsrow_tableentrypositive. dst_positive_code_fubini_rowsrowsrow_table = ff_q_pvs_fubini_rowsrowsrow_tableentrypositive * S ((S (dst_index_fubini_rowsrowsrow_table)) * dst_positive_scale_fubini_rowsrowsrow_table) + (dst_positive_fubini_rowsrowsrow_table))) /\ (((((exists ff_h_pvs_fubini_rowsrowsrow_tableentrynegative. ff_h_pvs_fubini_rowsrowsrow_tableentrynegative + S (dst_negative_fubini_rowsrowsrow_table) = S ((S (dst_index_fubini_rowsrowsrow_table)) * dst_negative_scale_fubini_rowsrowsrow_table)) /\ exists ff_q_pvs_fubini_rowsrowsrow_tableentrynegative. dst_negative_code_fubini_rowsrowsrow_table = ff_q_pvs_fubini_rowsrowsrow_tableentrynegative * S ((S (dst_index_fubini_rowsrowsrow_table)) * dst_negative_scale_fubini_rowsrowsrow_table) + (dst_negative_fubini_rowsrowsrow_table))) /\ (exists ge_balance_positive_fubini_rowsrowsrow_tableentryvalue ge_balance_negative_fubini_rowsrowsrow_tableentryvalue. (((((dst_value_fubini_rowsrowsrow_table) = 2 * (ge_balance_positive_fubini_rowsrowsrow_tableentryvalue) /\ (ge_balance_negative_fubini_rowsrowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_rowsrowsrow_tableentryvaluedecode. (((dst_value_fubini_rowsrowsrow_table) = 2 * ge_signed_half_fubini_rowsrowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_rowsrowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_rowsrowsrow_tableentryvalue) = S ge_signed_half_fubini_rowsrowsrow_tableentryvaluedecode))) /\ ((dst_positive_fubini_rowsrowsrow_table) + ge_balance_negative_fubini_rowsrowsrow_tableentryvalue = (dst_negative_fubini_rowsrowsrow_table) + ge_balance_positive_fubini_rowsrowsrow_tableentryvalue))))))))) /\ (forall srt_index_fubini_rowsrows. (exists pvs_gap_fubini_rowsrowsbound. pvs_gap_fubini_rowsrowsbound + S (srt_index_fubini_rowsrows) = (m)) -> exists srt_value_fubini_rowsrows. (((exists dst_positive_code_fubini_rowsrowsrowentry dst_positive_scale_fubini_rowsrowsrowentry dst_negative_code_fubini_rowsrowsrowentry dst_negative_scale_fubini_rowsrowsrowentry dst_positive_fubini_rowsrowsrowentry dst_negative_fubini_rowsrowsrowentry. (((srt_rows_fubini_rows) = (((((dst_positive_code_fubini_rowsrowsrowentry) + (dst_positive_scale_fubini_rowsrowsrowentry)) * S ((dst_positive_code_fubini_rowsrowsrowentry) + (dst_positive_scale_fubini_rowsrowsrowentry)) + ((dst_positive_scale_fubini_rowsrowsrowentry) + (dst_positive_scale_fubini_rowsrowsrowentry))) + (((dst_negative_code_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)) * S ((dst_negative_code_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)) + ((dst_negative_scale_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)))) * S ((((dst_positive_code_fubini_rowsrowsrowentry) + (dst_positive_scale_fubini_rowsrowsrowentry)) * S ((dst_positive_code_fubini_rowsrowsrowentry) + (dst_positive_scale_fubini_rowsrowsrowentry)) + ((dst_positive_scale_fubini_rowsrowsrowentry) + (dst_positive_scale_fubini_rowsrowsrowentry))) + (((dst_negative_code_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)) * S ((dst_negative_code_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)) + ((dst_negative_scale_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)))) + ((((dst_negative_code_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)) * S ((dst_negative_code_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)) + ((dst_negative_scale_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry))) + (((dst_negative_code_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)) * S ((dst_negative_code_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)) + ((dst_negative_scale_fubini_rowsrowsrowentry) + (dst_negative_scale_fubini_rowsrowsrowentry)))))) /\ (((((exists ff_h_pvs_fubini_rowsrowsrowentrypositive. ff_h_pvs_fubini_rowsrowsrowentrypositive + S (dst_positive_fubini_rowsrowsrowentry) = S ((S (srt_index_fubini_rowsrows)) * dst_positive_scale_fubini_rowsrowsrowentry)) /\ exists ff_q_pvs_fubini_rowsrowsrowentrypositive. dst_positive_code_fubini_rowsrowsrowentry = ff_q_pvs_fubini_rowsrowsrowentrypositive * S ((S (srt_index_fubini_rowsrows)) * dst_positive_scale_fubini_rowsrowsrowentry) + (dst_positive_fubini_rowsrowsrowentry))) /\ (((((exists ff_h_pvs_fubini_rowsrowsrowentrynegative. ff_h_pvs_fubini_rowsrowsrowentrynegative + S (dst_negative_fubini_rowsrowsrowentry) = S ((S (srt_index_fubini_rowsrows)) * dst_negative_scale_fubini_rowsrowsrowentry)) /\ exists ff_q_pvs_fubini_rowsrowsrowentrynegative. dst_negative_code_fubini_rowsrowsrowentry = ff_q_pvs_fubini_rowsrowsrowentrynegative * S ((S (srt_index_fubini_rowsrows)) * dst_negative_scale_fubini_rowsrowsrowentry) + (dst_negative_fubini_rowsrowsrowentry))) /\ (exists ge_balance_positive_fubini_rowsrowsrowentryvalue ge_balance_negative_fubini_rowsrowsrowentryvalue. (((((srt_value_fubini_rowsrows) = 2 * (ge_balance_positive_fubini_rowsrowsrowentryvalue) /\ (ge_balance_negative_fubini_rowsrowsrowentryvalue) = 0) \/ exists ge_signed_half_fubini_rowsrowsrowentryvaluedecode. (((srt_value_fubini_rowsrows) = 2 * ge_signed_half_fubini_rowsrowsrowentryvaluedecode + 1 /\ (ge_balance_positive_fubini_rowsrowsrowentryvalue) = 0) /\ (ge_balance_negative_fubini_rowsrowsrowentryvalue) = S ge_signed_half_fubini_rowsrowsrowentryvaluedecode))) /\ ((dst_positive_fubini_rowsrowsrowentry) + ge_balance_negative_fubini_rowsrowsrowentryvalue = (dst_negative_fubini_rowsrowsrowentry) + ge_balance_positive_fubini_rowsrowsrowentryvalue))))))))) /\ (exists srs_slice_fubini_rowsrowsrowrow_sum. ((((exists dst_positive_code_fubini_rowsrowsrowrow_sumslicesource_table dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_fubini_rowsrowsrowrow_sumslicesource_table. (exists pvs_le_gap_fubini_rowsrowsrowrow_sumslicesource_tabledomain. pvs_le_gap_fubini_rowsrowsrowrow_sumslicesource_tabledomain + (dst_index_fubini_rowsrowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_fubini_rowsrowsrowrow_sumslicesource_table dst_negative_fubini_rowsrowsrowrow_sumslicesource_table dst_value_fubini_rowsrowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_fubini_rowsrowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_fubini_rowsrowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_fubini_rowsrowsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_rowsrowsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_rowsrowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_fubini_rowsrowsrowrow_sumslicesource_table = ff_q_pvs_fubini_rowsrowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_fubini_rowsrowsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_positive_fubini_rowsrowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_fubini_rowsrowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_fubini_rowsrowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_fubini_rowsrowsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_rowsrowsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_rowsrowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_fubini_rowsrowsrowrow_sumslicesource_table = ff_q_pvs_fubini_rowsrowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_fubini_rowsrowsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_rowsrowsrowrow_sumslicesource_table) + (dst_negative_fubini_rowsrowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_fubini_rowsrowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_fubini_rowsrowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_fubini_rowsrowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_fubini_rowsrowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_rowsrowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_fubini_rowsrowsrowrow_sumslicesource_table) = 2 * ge_signed_half_fubini_rowsrowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_rowsrowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_fubini_rowsrowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_fubini_rowsrowsrowrow_sumslicesource_table) + ge_balance_negative_fubini_rowsrowsrowrow_sumslicesource_tableentryvalue = (dst_negative_fubini_rowsrowsrowrow_sumslicesource_table) + ge_balance_positive_fubini_rowsrowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_rowsrowsrowrow_sumsliceoutput_table dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table. (((srs_slice_fubini_rowsrowsrowrow_sum) = (((((dst_positive_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_fubini_rowsrowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_fubini_rowsrowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_fubini_rowsrowsrowrow_sumsliceoutput_tabledomain + (dst_index_fubini_rowsrowsrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_fubini_rowsrowsrowrow_sumsliceoutput_table dst_negative_fubini_rowsrowsrowrow_sumsliceoutput_table dst_value_fubini_rowsrowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_fubini_rowsrowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_fubini_rowsrowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_fubini_rowsrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_rowsrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_rowsrowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_fubini_rowsrowsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_rowsrowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_fubini_rowsrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_positive_fubini_rowsrowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_fubini_rowsrowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_fubini_rowsrowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_fubini_rowsrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_rowsrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_rowsrowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_fubini_rowsrowsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_rowsrowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_fubini_rowsrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_rowsrowsrowrow_sumsliceoutput_table) + (dst_negative_fubini_rowsrowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_fubini_rowsrowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_fubini_rowsrowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_fubini_rowsrowsrowrow_sumsliceoutput_table) + ge_balance_negative_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_fubini_rowsrowsrowrow_sumsliceoutput_table) + ge_balance_positive_fubini_rowsrowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_fubini_rowsrowsrowrow_sumslice. (exists pvs_gap_fubini_rowsrowsrowrow_sumslicebound. pvs_gap_fubini_rowsrowsrowrow_sumslicebound + S (srs_index_fubini_rowsrowsrowrow_sumslice) = (n)) -> exists srs_value_fubini_rowsrowsrowrow_sumslice. (((exists dst_positive_code_fubini_rowsrowsrowrow_sumsliceentrysource dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource dst_positive_fubini_rowsrowsrowrow_sumsliceentrysource dst_negative_fubini_rowsrowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_fubini_rowsrowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_fubini_rowsrowsrowrow_sumsliceentrysourcepositive + S (dst_positive_fubini_rowsrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_fubini_rowsrows)))) + ((t) * (srs_index_fubini_rowsrowsrowrow_sumslice))))) * dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_rowsrowsrowrow_sumsliceentrysourcepositive. dst_positive_code_fubini_rowsrowsrowrow_sumsliceentrysource = ff_q_pvs_fubini_rowsrowsrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (srt_index_fubini_rowsrows)))) + ((t) * (srs_index_fubini_rowsrowsrowrow_sumslice))))) * dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_positive_fubini_rowsrowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_fubini_rowsrowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_fubini_rowsrowsrowrow_sumsliceentrysourcenegative + S (dst_negative_fubini_rowsrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_fubini_rowsrows)))) + ((t) * (srs_index_fubini_rowsrowsrowrow_sumslice))))) * dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_rowsrowsrowrow_sumsliceentrysourcenegative. dst_negative_code_fubini_rowsrowsrowrow_sumsliceentrysource = ff_q_pvs_fubini_rowsrowsrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (srt_index_fubini_rowsrows)))) + ((t) * (srs_index_fubini_rowsrowsrowrow_sumslice))))) * dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentrysource) + (dst_negative_fubini_rowsrowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_fubini_rowsrowsrowrow_sumsliceentrysourcevalue ge_balance_negative_fubini_rowsrowsrowrow_sumsliceentrysourcevalue. (((((srs_value_fubini_rowsrowsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_rowsrowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_fubini_rowsrowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_fubini_rowsrowsrowrow_sumslice) = 2 * ge_signed_half_fubini_rowsrowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_fubini_rowsrowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_fubini_rowsrowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_fubini_rowsrowsrowrow_sumsliceentrysource) + ge_balance_negative_fubini_rowsrowsrowrow_sumsliceentrysourcevalue = (dst_negative_fubini_rowsrowsrowrow_sumsliceentrysource) + ge_balance_positive_fubini_rowsrowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_fubini_rowsrowsrowrow_sumsliceentryoutput dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput dst_positive_fubini_rowsrowsrowrow_sumsliceentryoutput dst_negative_fubini_rowsrowsrowrow_sumsliceentryoutput. (((srs_slice_fubini_rowsrowsrowrow_sum) = (((((dst_positive_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_fubini_rowsrowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_fubini_rowsrowsrowrow_sumsliceentryoutputpositive + S (dst_positive_fubini_rowsrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_rowsrowsrowrow_sumslice)) * dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_rowsrowsrowrow_sumsliceentryoutputpositive. dst_positive_code_fubini_rowsrowsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_rowsrowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_fubini_rowsrowsrowrow_sumslice)) * dst_positive_scale_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_positive_fubini_rowsrowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_fubini_rowsrowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_fubini_rowsrowsrowrow_sumsliceentryoutputnegative + S (dst_negative_fubini_rowsrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_rowsrowsrowrow_sumslice)) * dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_rowsrowsrowrow_sumsliceentryoutputnegative. dst_negative_code_fubini_rowsrowsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_rowsrowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_fubini_rowsrowsrowrow_sumslice)) * dst_negative_scale_fubini_rowsrowsrowrow_sumsliceentryoutput) + (dst_negative_fubini_rowsrowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_fubini_rowsrowsrowrow_sumsliceentryoutputvalue ge_balance_negative_fubini_rowsrowsrowrow_sumsliceentryoutputvalue. (((((srs_value_fubini_rowsrowsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_rowsrowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_fubini_rowsrowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_fubini_rowsrowsrowrow_sumslice) = 2 * ge_signed_half_fubini_rowsrowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_fubini_rowsrowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_fubini_rowsrowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_fubini_rowsrowsrowrow_sumsliceentryoutput) + ge_balance_negative_fubini_rowsrowsrowrow_sumsliceentryoutputvalue = (dst_negative_fubini_rowsrowsrowrow_sumsliceentryoutput) + ge_balance_positive_fubini_rowsrowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_fubini_rowsrowsrowrow_sumsum dst_positive_scale_fubini_rowsrowsrowrow_sumsum dst_negative_code_fubini_rowsrowsrowrow_sumsum dst_negative_scale_fubini_rowsrowsrowrow_sumsum dst_positive_sum_fubini_rowsrowsrowrow_sumsum dst_negative_sum_fubini_rowsrowsrowrow_sumsum. (((srs_slice_fubini_rowsrowsrowrow_sum) = (((((dst_positive_code_fubini_rowsrowsrowrow_sumsum) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsum)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumsum) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsum)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumsum) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsum))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)))) * S ((((dst_positive_code_fubini_rowsrowsrowrow_sumsum) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsum)) * S ((dst_positive_code_fubini_rowsrowsrowrow_sumsum) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsum)) + ((dst_positive_scale_fubini_rowsrowsrowrow_sumsum) + (dst_positive_scale_fubini_rowsrowsrowrow_sumsum))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)))) + ((((dst_negative_code_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum))) + (((dst_negative_code_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_rowsrowsrowrow_sumsum) + (dst_negative_scale_fubini_rowsrowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_fubini_rowsrowsrowrow_sumsumpositive fs_v_dst_fubini_rowsrowsrowrow_sumsumpositive. ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_start. fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_start. fs_u_dst_fubini_rowsrowsrowrow_sumsumpositive = fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_terminal. fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_fubini_rowsrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_terminal. fs_u_dst_fubini_rowsrowsrowrow_sumsumpositive = fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumpositive) + (dst_positive_sum_fubini_rowsrowsrowrow_sumsum))) /\ forall fs_i_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps fs_r_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps fs_s_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_rowsrowsrowrow_sumsum)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_fubini_rowsrowsrowrow_sumsum = fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_rowsrowsrowrow_sumsum) + (fs_a_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_fubini_rowsrowsrowrow_sumsumpositive = fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumpositive) + (fs_r_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_fubini_rowsrowsrowrow_sumsumpositive = fs_q_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumpositive) + (fs_s_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps = fs_r_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps + fs_a_dst_fubini_rowsrowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_rowsrowsrowrow_sumsumnegative fs_v_dst_fubini_rowsrowsrowrow_sumsumnegative. ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_start. fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_start. fs_u_dst_fubini_rowsrowsrowrow_sumsumnegative = fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_terminal. fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_fubini_rowsrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_terminal. fs_u_dst_fubini_rowsrowsrowrow_sumsumnegative = fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumnegative) + (dst_negative_sum_fubini_rowsrowsrowrow_sumsum))) /\ forall fs_i_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps fs_r_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps fs_s_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_rowsrowsrowrow_sumsum)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_fubini_rowsrowsrowrow_sumsum = fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_rowsrowsrowrow_sumsum) + (fs_a_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_fubini_rowsrowsrowrow_sumsumnegative = fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumnegative) + (fs_r_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_fubini_rowsrowsrowrow_sumsumnegative = fs_q_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_rowsrowsrowrow_sumsumnegative) + (fs_s_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps = fs_r_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps + fs_a_dst_fubini_rowsrowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_rowsrowsrowrow_sumsumresult ge_balance_negative_fubini_rowsrowsrowrow_sumsumresult. (((((srt_value_fubini_rowsrows) = 2 * (ge_balance_positive_fubini_rowsrowsrowrow_sumsumresult) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_fubini_rowsrowsrowrow_sumsumresultdecode. (((srt_value_fubini_rowsrows) = 2 * ge_signed_half_fubini_rowsrowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_fubini_rowsrowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_fubini_rowsrowsrowrow_sumsumresult) = S ge_signed_half_fubini_rowsrowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_fubini_rowsrowsrowrow_sumsum) + ge_balance_negative_fubini_rowsrowsrowrow_sumsumresult = (dst_negative_sum_fubini_rowsrowsrowrow_sumsum) + ge_balance_positive_fubini_rowsrowsrowrow_sumsumresult)))))))))))))))))) /\ (exists dst_positive_code_fubini_rowstotal dst_positive_scale_fubini_rowstotal dst_negative_code_fubini_rowstotal dst_negative_scale_fubini_rowstotal dst_positive_sum_fubini_rowstotal dst_negative_sum_fubini_rowstotal. (((srt_rows_fubini_rows) = (((((dst_positive_code_fubini_rowstotal) + (dst_positive_scale_fubini_rowstotal)) * S ((dst_positive_code_fubini_rowstotal) + (dst_positive_scale_fubini_rowstotal)) + ((dst_positive_scale_fubini_rowstotal) + (dst_positive_scale_fubini_rowstotal))) + (((dst_negative_code_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)) * S ((dst_negative_code_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)) + ((dst_negative_scale_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)))) * S ((((dst_positive_code_fubini_rowstotal) + (dst_positive_scale_fubini_rowstotal)) * S ((dst_positive_code_fubini_rowstotal) + (dst_positive_scale_fubini_rowstotal)) + ((dst_positive_scale_fubini_rowstotal) + (dst_positive_scale_fubini_rowstotal))) + (((dst_negative_code_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)) * S ((dst_negative_code_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)) + ((dst_negative_scale_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)))) + ((((dst_negative_code_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)) * S ((dst_negative_code_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)) + ((dst_negative_scale_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal))) + (((dst_negative_code_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)) * S ((dst_negative_code_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)) + ((dst_negative_scale_fubini_rowstotal) + (dst_negative_scale_fubini_rowstotal)))))) /\ (((exists fs_u_dst_fubini_rowstotalpositive fs_v_dst_fubini_rowstotalpositive. ((((exists fs_h_dst_fubini_rowstotalpositive_body_start. fs_h_dst_fubini_rowstotalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_rowstotalpositive)) /\ exists fs_q_dst_fubini_rowstotalpositive_body_start. fs_u_dst_fubini_rowstotalpositive = fs_q_dst_fubini_rowstotalpositive_body_start * S ((S (0)) * fs_v_dst_fubini_rowstotalpositive) + (0))) /\ ((((exists fs_h_dst_fubini_rowstotalpositive_body_terminal. fs_h_dst_fubini_rowstotalpositive_body_terminal + S (dst_positive_sum_fubini_rowstotal) = S ((S (m)) * fs_v_dst_fubini_rowstotalpositive)) /\ exists fs_q_dst_fubini_rowstotalpositive_body_terminal. fs_u_dst_fubini_rowstotalpositive = fs_q_dst_fubini_rowstotalpositive_body_terminal * S ((S (m)) * fs_v_dst_fubini_rowstotalpositive) + (dst_positive_sum_fubini_rowstotal))) /\ forall fs_i_dst_fubini_rowstotalpositive_body_steps. (exists fs_lt_dst_fubini_rowstotalpositive_body_steps_bound. fs_lt_dst_fubini_rowstotalpositive_body_steps_bound + S fs_i_dst_fubini_rowstotalpositive_body_steps = m) -> exists fs_a_dst_fubini_rowstotalpositive_body_steps fs_r_dst_fubini_rowstotalpositive_body_steps fs_s_dst_fubini_rowstotalpositive_body_steps. ((((exists fs_h_dst_fubini_rowstotalpositive_body_steps_summand. fs_h_dst_fubini_rowstotalpositive_body_steps_summand + S (fs_a_dst_fubini_rowstotalpositive_body_steps) = S ((S (fs_i_dst_fubini_rowstotalpositive_body_steps)) * dst_positive_scale_fubini_rowstotal)) /\ exists fs_q_dst_fubini_rowstotalpositive_body_steps_summand. dst_positive_code_fubini_rowstotal = fs_q_dst_fubini_rowstotalpositive_body_steps_summand * S ((S (fs_i_dst_fubini_rowstotalpositive_body_steps)) * dst_positive_scale_fubini_rowstotal) + (fs_a_dst_fubini_rowstotalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_rowstotalpositive_body_steps_partial. fs_h_dst_fubini_rowstotalpositive_body_steps_partial + S (fs_r_dst_fubini_rowstotalpositive_body_steps) = S ((S (fs_i_dst_fubini_rowstotalpositive_body_steps)) * fs_v_dst_fubini_rowstotalpositive)) /\ exists fs_q_dst_fubini_rowstotalpositive_body_steps_partial. fs_u_dst_fubini_rowstotalpositive = fs_q_dst_fubini_rowstotalpositive_body_steps_partial * S ((S (fs_i_dst_fubini_rowstotalpositive_body_steps)) * fs_v_dst_fubini_rowstotalpositive) + (fs_r_dst_fubini_rowstotalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_rowstotalpositive_body_steps_successor. fs_h_dst_fubini_rowstotalpositive_body_steps_successor + S (fs_s_dst_fubini_rowstotalpositive_body_steps) = S ((S (S fs_i_dst_fubini_rowstotalpositive_body_steps)) * fs_v_dst_fubini_rowstotalpositive)) /\ exists fs_q_dst_fubini_rowstotalpositive_body_steps_successor. fs_u_dst_fubini_rowstotalpositive = fs_q_dst_fubini_rowstotalpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_rowstotalpositive_body_steps)) * fs_v_dst_fubini_rowstotalpositive) + (fs_s_dst_fubini_rowstotalpositive_body_steps))) /\ fs_s_dst_fubini_rowstotalpositive_body_steps = fs_r_dst_fubini_rowstotalpositive_body_steps + fs_a_dst_fubini_rowstotalpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_rowstotalnegative fs_v_dst_fubini_rowstotalnegative. ((((exists fs_h_dst_fubini_rowstotalnegative_body_start. fs_h_dst_fubini_rowstotalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_rowstotalnegative)) /\ exists fs_q_dst_fubini_rowstotalnegative_body_start. fs_u_dst_fubini_rowstotalnegative = fs_q_dst_fubini_rowstotalnegative_body_start * S ((S (0)) * fs_v_dst_fubini_rowstotalnegative) + (0))) /\ ((((exists fs_h_dst_fubini_rowstotalnegative_body_terminal. fs_h_dst_fubini_rowstotalnegative_body_terminal + S (dst_negative_sum_fubini_rowstotal) = S ((S (m)) * fs_v_dst_fubini_rowstotalnegative)) /\ exists fs_q_dst_fubini_rowstotalnegative_body_terminal. fs_u_dst_fubini_rowstotalnegative = fs_q_dst_fubini_rowstotalnegative_body_terminal * S ((S (m)) * fs_v_dst_fubini_rowstotalnegative) + (dst_negative_sum_fubini_rowstotal))) /\ forall fs_i_dst_fubini_rowstotalnegative_body_steps. (exists fs_lt_dst_fubini_rowstotalnegative_body_steps_bound. fs_lt_dst_fubini_rowstotalnegative_body_steps_bound + S fs_i_dst_fubini_rowstotalnegative_body_steps = m) -> exists fs_a_dst_fubini_rowstotalnegative_body_steps fs_r_dst_fubini_rowstotalnegative_body_steps fs_s_dst_fubini_rowstotalnegative_body_steps. ((((exists fs_h_dst_fubini_rowstotalnegative_body_steps_summand. fs_h_dst_fubini_rowstotalnegative_body_steps_summand + S (fs_a_dst_fubini_rowstotalnegative_body_steps) = S ((S (fs_i_dst_fubini_rowstotalnegative_body_steps)) * dst_negative_scale_fubini_rowstotal)) /\ exists fs_q_dst_fubini_rowstotalnegative_body_steps_summand. dst_negative_code_fubini_rowstotal = fs_q_dst_fubini_rowstotalnegative_body_steps_summand * S ((S (fs_i_dst_fubini_rowstotalnegative_body_steps)) * dst_negative_scale_fubini_rowstotal) + (fs_a_dst_fubini_rowstotalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_rowstotalnegative_body_steps_partial. fs_h_dst_fubini_rowstotalnegative_body_steps_partial + S (fs_r_dst_fubini_rowstotalnegative_body_steps) = S ((S (fs_i_dst_fubini_rowstotalnegative_body_steps)) * fs_v_dst_fubini_rowstotalnegative)) /\ exists fs_q_dst_fubini_rowstotalnegative_body_steps_partial. fs_u_dst_fubini_rowstotalnegative = fs_q_dst_fubini_rowstotalnegative_body_steps_partial * S ((S (fs_i_dst_fubini_rowstotalnegative_body_steps)) * fs_v_dst_fubini_rowstotalnegative) + (fs_r_dst_fubini_rowstotalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_rowstotalnegative_body_steps_successor. fs_h_dst_fubini_rowstotalnegative_body_steps_successor + S (fs_s_dst_fubini_rowstotalnegative_body_steps) = S ((S (S fs_i_dst_fubini_rowstotalnegative_body_steps)) * fs_v_dst_fubini_rowstotalnegative)) /\ exists fs_q_dst_fubini_rowstotalnegative_body_steps_successor. fs_u_dst_fubini_rowstotalnegative = fs_q_dst_fubini_rowstotalnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_rowstotalnegative_body_steps)) * fs_v_dst_fubini_rowstotalnegative) + (fs_s_dst_fubini_rowstotalnegative_body_steps))) /\ fs_s_dst_fubini_rowstotalnegative_body_steps = fs_r_dst_fubini_rowstotalnegative_body_steps + fs_a_dst_fubini_rowstotalnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_rowstotalresult ge_balance_negative_fubini_rowstotalresult. (((((a) = 2 * (ge_balance_positive_fubini_rowstotalresult) /\ (ge_balance_negative_fubini_rowstotalresult) = 0) \/ exists ge_signed_half_fubini_rowstotalresultdecode. (((a) = 2 * ge_signed_half_fubini_rowstotalresultdecode + 1 /\ (ge_balance_positive_fubini_rowstotalresult) = 0) /\ (ge_balance_negative_fubini_rowstotalresult) = S ge_signed_half_fubini_rowstotalresultdecode))) /\ ((dst_positive_sum_fubini_rowstotal) + ge_balance_negative_fubini_rowstotalresult = (dst_negative_sum_fubini_rowstotal) + ge_balance_positive_fubini_rowstotalresult))))))))))) -> (exists srt_rows_fubini_columns. ((((exists dst_positive_code_fubini_columnsrowssource_table dst_positive_scale_fubini_columnsrowssource_table dst_negative_code_fubini_columnsrowssource_table dst_negative_scale_fubini_columnsrowssource_table. (((F) = (((((dst_positive_code_fubini_columnsrowssource_table) + (dst_positive_scale_fubini_columnsrowssource_table)) * S ((dst_positive_code_fubini_columnsrowssource_table) + (dst_positive_scale_fubini_columnsrowssource_table)) + ((dst_positive_scale_fubini_columnsrowssource_table) + (dst_positive_scale_fubini_columnsrowssource_table))) + (((dst_negative_code_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)) * S ((dst_negative_code_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)) + ((dst_negative_scale_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)))) * S ((((dst_positive_code_fubini_columnsrowssource_table) + (dst_positive_scale_fubini_columnsrowssource_table)) * S ((dst_positive_code_fubini_columnsrowssource_table) + (dst_positive_scale_fubini_columnsrowssource_table)) + ((dst_positive_scale_fubini_columnsrowssource_table) + (dst_positive_scale_fubini_columnsrowssource_table))) + (((dst_negative_code_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)) * S ((dst_negative_code_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)) + ((dst_negative_scale_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)))) + ((((dst_negative_code_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)) * S ((dst_negative_code_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)) + ((dst_negative_scale_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table))) + (((dst_negative_code_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)) * S ((dst_negative_code_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)) + ((dst_negative_scale_fubini_columnsrowssource_table) + (dst_negative_scale_fubini_columnsrowssource_table)))))) /\ (forall dst_index_fubini_columnsrowssource_table. (exists pvs_le_gap_fubini_columnsrowssource_tabledomain. pvs_le_gap_fubini_columnsrowssource_tabledomain + (dst_index_fubini_columnsrowssource_table) = (0)) -> exists dst_positive_fubini_columnsrowssource_table dst_negative_fubini_columnsrowssource_table dst_value_fubini_columnsrowssource_table. ((((exists ff_h_pvs_fubini_columnsrowssource_tableentrypositive. ff_h_pvs_fubini_columnsrowssource_tableentrypositive + S (dst_positive_fubini_columnsrowssource_table) = S ((S (dst_index_fubini_columnsrowssource_table)) * dst_positive_scale_fubini_columnsrowssource_table)) /\ exists ff_q_pvs_fubini_columnsrowssource_tableentrypositive. dst_positive_code_fubini_columnsrowssource_table = ff_q_pvs_fubini_columnsrowssource_tableentrypositive * S ((S (dst_index_fubini_columnsrowssource_table)) * dst_positive_scale_fubini_columnsrowssource_table) + (dst_positive_fubini_columnsrowssource_table))) /\ (((((exists ff_h_pvs_fubini_columnsrowssource_tableentrynegative. ff_h_pvs_fubini_columnsrowssource_tableentrynegative + S (dst_negative_fubini_columnsrowssource_table) = S ((S (dst_index_fubini_columnsrowssource_table)) * dst_negative_scale_fubini_columnsrowssource_table)) /\ exists ff_q_pvs_fubini_columnsrowssource_tableentrynegative. dst_negative_code_fubini_columnsrowssource_table = ff_q_pvs_fubini_columnsrowssource_tableentrynegative * S ((S (dst_index_fubini_columnsrowssource_table)) * dst_negative_scale_fubini_columnsrowssource_table) + (dst_negative_fubini_columnsrowssource_table))) /\ (exists ge_balance_positive_fubini_columnsrowssource_tableentryvalue ge_balance_negative_fubini_columnsrowssource_tableentryvalue. (((((dst_value_fubini_columnsrowssource_table) = 2 * (ge_balance_positive_fubini_columnsrowssource_tableentryvalue) /\ (ge_balance_negative_fubini_columnsrowssource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_columnsrowssource_tableentryvaluedecode. (((dst_value_fubini_columnsrowssource_table) = 2 * ge_signed_half_fubini_columnsrowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_columnsrowssource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_columnsrowssource_tableentryvalue) = S ge_signed_half_fubini_columnsrowssource_tableentryvaluedecode))) /\ ((dst_positive_fubini_columnsrowssource_table) + ge_balance_negative_fubini_columnsrowssource_tableentryvalue = (dst_negative_fubini_columnsrowssource_table) + ge_balance_positive_fubini_columnsrowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_columnsrowsrow_table dst_positive_scale_fubini_columnsrowsrow_table dst_negative_code_fubini_columnsrowsrow_table dst_negative_scale_fubini_columnsrowsrow_table. (((srt_rows_fubini_columns) = (((((dst_positive_code_fubini_columnsrowsrow_table) + (dst_positive_scale_fubini_columnsrowsrow_table)) * S ((dst_positive_code_fubini_columnsrowsrow_table) + (dst_positive_scale_fubini_columnsrowsrow_table)) + ((dst_positive_scale_fubini_columnsrowsrow_table) + (dst_positive_scale_fubini_columnsrowsrow_table))) + (((dst_negative_code_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)) * S ((dst_negative_code_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)) + ((dst_negative_scale_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)))) * S ((((dst_positive_code_fubini_columnsrowsrow_table) + (dst_positive_scale_fubini_columnsrowsrow_table)) * S ((dst_positive_code_fubini_columnsrowsrow_table) + (dst_positive_scale_fubini_columnsrowsrow_table)) + ((dst_positive_scale_fubini_columnsrowsrow_table) + (dst_positive_scale_fubini_columnsrowsrow_table))) + (((dst_negative_code_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)) * S ((dst_negative_code_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)) + ((dst_negative_scale_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)))) + ((((dst_negative_code_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)) * S ((dst_negative_code_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)) + ((dst_negative_scale_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table))) + (((dst_negative_code_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)) * S ((dst_negative_code_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)) + ((dst_negative_scale_fubini_columnsrowsrow_table) + (dst_negative_scale_fubini_columnsrowsrow_table)))))) /\ (forall dst_index_fubini_columnsrowsrow_table. (exists pvs_le_gap_fubini_columnsrowsrow_tabledomain. pvs_le_gap_fubini_columnsrowsrow_tabledomain + (dst_index_fubini_columnsrowsrow_table) = (n)) -> exists dst_positive_fubini_columnsrowsrow_table dst_negative_fubini_columnsrowsrow_table dst_value_fubini_columnsrowsrow_table. ((((exists ff_h_pvs_fubini_columnsrowsrow_tableentrypositive. ff_h_pvs_fubini_columnsrowsrow_tableentrypositive + S (dst_positive_fubini_columnsrowsrow_table) = S ((S (dst_index_fubini_columnsrowsrow_table)) * dst_positive_scale_fubini_columnsrowsrow_table)) /\ exists ff_q_pvs_fubini_columnsrowsrow_tableentrypositive. dst_positive_code_fubini_columnsrowsrow_table = ff_q_pvs_fubini_columnsrowsrow_tableentrypositive * S ((S (dst_index_fubini_columnsrowsrow_table)) * dst_positive_scale_fubini_columnsrowsrow_table) + (dst_positive_fubini_columnsrowsrow_table))) /\ (((((exists ff_h_pvs_fubini_columnsrowsrow_tableentrynegative. ff_h_pvs_fubini_columnsrowsrow_tableentrynegative + S (dst_negative_fubini_columnsrowsrow_table) = S ((S (dst_index_fubini_columnsrowsrow_table)) * dst_negative_scale_fubini_columnsrowsrow_table)) /\ exists ff_q_pvs_fubini_columnsrowsrow_tableentrynegative. dst_negative_code_fubini_columnsrowsrow_table = ff_q_pvs_fubini_columnsrowsrow_tableentrynegative * S ((S (dst_index_fubini_columnsrowsrow_table)) * dst_negative_scale_fubini_columnsrowsrow_table) + (dst_negative_fubini_columnsrowsrow_table))) /\ (exists ge_balance_positive_fubini_columnsrowsrow_tableentryvalue ge_balance_negative_fubini_columnsrowsrow_tableentryvalue. (((((dst_value_fubini_columnsrowsrow_table) = 2 * (ge_balance_positive_fubini_columnsrowsrow_tableentryvalue) /\ (ge_balance_negative_fubini_columnsrowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_columnsrowsrow_tableentryvaluedecode. (((dst_value_fubini_columnsrowsrow_table) = 2 * ge_signed_half_fubini_columnsrowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_columnsrowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_columnsrowsrow_tableentryvalue) = S ge_signed_half_fubini_columnsrowsrow_tableentryvaluedecode))) /\ ((dst_positive_fubini_columnsrowsrow_table) + ge_balance_negative_fubini_columnsrowsrow_tableentryvalue = (dst_negative_fubini_columnsrowsrow_table) + ge_balance_positive_fubini_columnsrowsrow_tableentryvalue))))))))) /\ (forall srt_index_fubini_columnsrows. (exists pvs_gap_fubini_columnsrowsbound. pvs_gap_fubini_columnsrowsbound + S (srt_index_fubini_columnsrows) = (n)) -> exists srt_value_fubini_columnsrows. (((exists dst_positive_code_fubini_columnsrowsrowentry dst_positive_scale_fubini_columnsrowsrowentry dst_negative_code_fubini_columnsrowsrowentry dst_negative_scale_fubini_columnsrowsrowentry dst_positive_fubini_columnsrowsrowentry dst_negative_fubini_columnsrowsrowentry. (((srt_rows_fubini_columns) = (((((dst_positive_code_fubini_columnsrowsrowentry) + (dst_positive_scale_fubini_columnsrowsrowentry)) * S ((dst_positive_code_fubini_columnsrowsrowentry) + (dst_positive_scale_fubini_columnsrowsrowentry)) + ((dst_positive_scale_fubini_columnsrowsrowentry) + (dst_positive_scale_fubini_columnsrowsrowentry))) + (((dst_negative_code_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)) * S ((dst_negative_code_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)) + ((dst_negative_scale_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)))) * S ((((dst_positive_code_fubini_columnsrowsrowentry) + (dst_positive_scale_fubini_columnsrowsrowentry)) * S ((dst_positive_code_fubini_columnsrowsrowentry) + (dst_positive_scale_fubini_columnsrowsrowentry)) + ((dst_positive_scale_fubini_columnsrowsrowentry) + (dst_positive_scale_fubini_columnsrowsrowentry))) + (((dst_negative_code_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)) * S ((dst_negative_code_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)) + ((dst_negative_scale_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)))) + ((((dst_negative_code_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)) * S ((dst_negative_code_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)) + ((dst_negative_scale_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry))) + (((dst_negative_code_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)) * S ((dst_negative_code_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)) + ((dst_negative_scale_fubini_columnsrowsrowentry) + (dst_negative_scale_fubini_columnsrowsrowentry)))))) /\ (((((exists ff_h_pvs_fubini_columnsrowsrowentrypositive. ff_h_pvs_fubini_columnsrowsrowentrypositive + S (dst_positive_fubini_columnsrowsrowentry) = S ((S (srt_index_fubini_columnsrows)) * dst_positive_scale_fubini_columnsrowsrowentry)) /\ exists ff_q_pvs_fubini_columnsrowsrowentrypositive. dst_positive_code_fubini_columnsrowsrowentry = ff_q_pvs_fubini_columnsrowsrowentrypositive * S ((S (srt_index_fubini_columnsrows)) * dst_positive_scale_fubini_columnsrowsrowentry) + (dst_positive_fubini_columnsrowsrowentry))) /\ (((((exists ff_h_pvs_fubini_columnsrowsrowentrynegative. ff_h_pvs_fubini_columnsrowsrowentrynegative + S (dst_negative_fubini_columnsrowsrowentry) = S ((S (srt_index_fubini_columnsrows)) * dst_negative_scale_fubini_columnsrowsrowentry)) /\ exists ff_q_pvs_fubini_columnsrowsrowentrynegative. dst_negative_code_fubini_columnsrowsrowentry = ff_q_pvs_fubini_columnsrowsrowentrynegative * S ((S (srt_index_fubini_columnsrows)) * dst_negative_scale_fubini_columnsrowsrowentry) + (dst_negative_fubini_columnsrowsrowentry))) /\ (exists ge_balance_positive_fubini_columnsrowsrowentryvalue ge_balance_negative_fubini_columnsrowsrowentryvalue. (((((srt_value_fubini_columnsrows) = 2 * (ge_balance_positive_fubini_columnsrowsrowentryvalue) /\ (ge_balance_negative_fubini_columnsrowsrowentryvalue) = 0) \/ exists ge_signed_half_fubini_columnsrowsrowentryvaluedecode. (((srt_value_fubini_columnsrows) = 2 * ge_signed_half_fubini_columnsrowsrowentryvaluedecode + 1 /\ (ge_balance_positive_fubini_columnsrowsrowentryvalue) = 0) /\ (ge_balance_negative_fubini_columnsrowsrowentryvalue) = S ge_signed_half_fubini_columnsrowsrowentryvaluedecode))) /\ ((dst_positive_fubini_columnsrowsrowentry) + ge_balance_negative_fubini_columnsrowsrowentryvalue = (dst_negative_fubini_columnsrowsrowentry) + ge_balance_positive_fubini_columnsrowsrowentryvalue))))))))) /\ (exists srs_slice_fubini_columnsrowsrowrow_sum. ((((exists dst_positive_code_fubini_columnsrowsrowrow_sumslicesource_table dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_fubini_columnsrowsrowrow_sumslicesource_table. (exists pvs_le_gap_fubini_columnsrowsrowrow_sumslicesource_tabledomain. pvs_le_gap_fubini_columnsrowsrowrow_sumslicesource_tabledomain + (dst_index_fubini_columnsrowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_fubini_columnsrowsrowrow_sumslicesource_table dst_negative_fubini_columnsrowsrowrow_sumslicesource_table dst_value_fubini_columnsrowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_fubini_columnsrowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_fubini_columnsrowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_fubini_columnsrowsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_columnsrowsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_columnsrowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_fubini_columnsrowsrowrow_sumslicesource_table = ff_q_pvs_fubini_columnsrowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_fubini_columnsrowsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_positive_fubini_columnsrowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_fubini_columnsrowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_fubini_columnsrowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_fubini_columnsrowsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_columnsrowsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_columnsrowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_fubini_columnsrowsrowrow_sumslicesource_table = ff_q_pvs_fubini_columnsrowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_fubini_columnsrowsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_columnsrowsrowrow_sumslicesource_table) + (dst_negative_fubini_columnsrowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_fubini_columnsrowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_fubini_columnsrowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_fubini_columnsrowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_fubini_columnsrowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_columnsrowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_fubini_columnsrowsrowrow_sumslicesource_table) = 2 * ge_signed_half_fubini_columnsrowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_columnsrowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_fubini_columnsrowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_fubini_columnsrowsrowrow_sumslicesource_table) + ge_balance_negative_fubini_columnsrowsrowrow_sumslicesource_tableentryvalue = (dst_negative_fubini_columnsrowsrowrow_sumslicesource_table) + ge_balance_positive_fubini_columnsrowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_columnsrowsrowrow_sumsliceoutput_table dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table. (((srs_slice_fubini_columnsrowsrowrow_sum) = (((((dst_positive_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_fubini_columnsrowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_fubini_columnsrowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_fubini_columnsrowsrowrow_sumsliceoutput_tabledomain + (dst_index_fubini_columnsrowsrowrow_sumsliceoutput_table) = (m)) -> exists dst_positive_fubini_columnsrowsrowrow_sumsliceoutput_table dst_negative_fubini_columnsrowsrowrow_sumsliceoutput_table dst_value_fubini_columnsrowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_fubini_columnsrowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_fubini_columnsrowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_fubini_columnsrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_columnsrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_columnsrowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_fubini_columnsrowsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_columnsrowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_fubini_columnsrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_positive_fubini_columnsrowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_fubini_columnsrowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_fubini_columnsrowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_fubini_columnsrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_columnsrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_columnsrowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_fubini_columnsrowsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_columnsrowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_fubini_columnsrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_columnsrowsrowrow_sumsliceoutput_table) + (dst_negative_fubini_columnsrowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_fubini_columnsrowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_fubini_columnsrowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_fubini_columnsrowsrowrow_sumsliceoutput_table) + ge_balance_negative_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_fubini_columnsrowsrowrow_sumsliceoutput_table) + ge_balance_positive_fubini_columnsrowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_fubini_columnsrowsrowrow_sumslice. (exists pvs_gap_fubini_columnsrowsrowrow_sumslicebound. pvs_gap_fubini_columnsrowsrowrow_sumslicebound + S (srs_index_fubini_columnsrowsrowrow_sumslice) = (m)) -> exists srs_value_fubini_columnsrowsrowrow_sumslice. (((exists dst_positive_code_fubini_columnsrowsrowrow_sumsliceentrysource dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource dst_positive_fubini_columnsrowsrowrow_sumsliceentrysource dst_negative_fubini_columnsrowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_fubini_columnsrowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_fubini_columnsrowsrowrow_sumsliceentrysourcepositive + S (dst_positive_fubini_columnsrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((t) * (srt_index_fubini_columnsrows)))) + ((s) * (srs_index_fubini_columnsrowsrowrow_sumslice))))) * dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_columnsrowsrowrow_sumsliceentrysourcepositive. dst_positive_code_fubini_columnsrowsrowrow_sumsliceentrysource = ff_q_pvs_fubini_columnsrowsrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((t) * (srt_index_fubini_columnsrows)))) + ((s) * (srs_index_fubini_columnsrowsrowrow_sumslice))))) * dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_positive_fubini_columnsrowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_fubini_columnsrowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_fubini_columnsrowsrowrow_sumsliceentrysourcenegative + S (dst_negative_fubini_columnsrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((t) * (srt_index_fubini_columnsrows)))) + ((s) * (srs_index_fubini_columnsrowsrowrow_sumslice))))) * dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_columnsrowsrowrow_sumsliceentrysourcenegative. dst_negative_code_fubini_columnsrowsrowrow_sumsliceentrysource = ff_q_pvs_fubini_columnsrowsrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((t) * (srt_index_fubini_columnsrows)))) + ((s) * (srs_index_fubini_columnsrowsrowrow_sumslice))))) * dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentrysource) + (dst_negative_fubini_columnsrowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_fubini_columnsrowsrowrow_sumsliceentrysourcevalue ge_balance_negative_fubini_columnsrowsrowrow_sumsliceentrysourcevalue. (((((srs_value_fubini_columnsrowsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_columnsrowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_fubini_columnsrowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_fubini_columnsrowsrowrow_sumslice) = 2 * ge_signed_half_fubini_columnsrowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_fubini_columnsrowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_fubini_columnsrowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_fubini_columnsrowsrowrow_sumsliceentrysource) + ge_balance_negative_fubini_columnsrowsrowrow_sumsliceentrysourcevalue = (dst_negative_fubini_columnsrowsrowrow_sumsliceentrysource) + ge_balance_positive_fubini_columnsrowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_fubini_columnsrowsrowrow_sumsliceentryoutput dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput dst_positive_fubini_columnsrowsrowrow_sumsliceentryoutput dst_negative_fubini_columnsrowsrowrow_sumsliceentryoutput. (((srs_slice_fubini_columnsrowsrowrow_sum) = (((((dst_positive_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_fubini_columnsrowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_fubini_columnsrowsrowrow_sumsliceentryoutputpositive + S (dst_positive_fubini_columnsrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_columnsrowsrowrow_sumslice)) * dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_columnsrowsrowrow_sumsliceentryoutputpositive. dst_positive_code_fubini_columnsrowsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_columnsrowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_fubini_columnsrowsrowrow_sumslice)) * dst_positive_scale_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_positive_fubini_columnsrowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_fubini_columnsrowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_fubini_columnsrowsrowrow_sumsliceentryoutputnegative + S (dst_negative_fubini_columnsrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_columnsrowsrowrow_sumslice)) * dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_columnsrowsrowrow_sumsliceentryoutputnegative. dst_negative_code_fubini_columnsrowsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_columnsrowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_fubini_columnsrowsrowrow_sumslice)) * dst_negative_scale_fubini_columnsrowsrowrow_sumsliceentryoutput) + (dst_negative_fubini_columnsrowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_fubini_columnsrowsrowrow_sumsliceentryoutputvalue ge_balance_negative_fubini_columnsrowsrowrow_sumsliceentryoutputvalue. (((((srs_value_fubini_columnsrowsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_columnsrowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_fubini_columnsrowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_fubini_columnsrowsrowrow_sumslice) = 2 * ge_signed_half_fubini_columnsrowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_fubini_columnsrowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_fubini_columnsrowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_fubini_columnsrowsrowrow_sumsliceentryoutput) + ge_balance_negative_fubini_columnsrowsrowrow_sumsliceentryoutputvalue = (dst_negative_fubini_columnsrowsrowrow_sumsliceentryoutput) + ge_balance_positive_fubini_columnsrowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_fubini_columnsrowsrowrow_sumsum dst_positive_scale_fubini_columnsrowsrowrow_sumsum dst_negative_code_fubini_columnsrowsrowrow_sumsum dst_negative_scale_fubini_columnsrowsrowrow_sumsum dst_positive_sum_fubini_columnsrowsrowrow_sumsum dst_negative_sum_fubini_columnsrowsrowrow_sumsum. (((srs_slice_fubini_columnsrowsrowrow_sum) = (((((dst_positive_code_fubini_columnsrowsrowrow_sumsum) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsum)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumsum) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsum)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumsum) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsum))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)))) * S ((((dst_positive_code_fubini_columnsrowsrowrow_sumsum) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsum)) * S ((dst_positive_code_fubini_columnsrowsrowrow_sumsum) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsum)) + ((dst_positive_scale_fubini_columnsrowsrowrow_sumsum) + (dst_positive_scale_fubini_columnsrowsrowrow_sumsum))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)))) + ((((dst_negative_code_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum))) + (((dst_negative_code_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_columnsrowsrowrow_sumsum) + (dst_negative_scale_fubini_columnsrowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_fubini_columnsrowsrowrow_sumsumpositive fs_v_dst_fubini_columnsrowsrowrow_sumsumpositive. ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_start. fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_start. fs_u_dst_fubini_columnsrowsrowrow_sumsumpositive = fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_terminal. fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_fubini_columnsrowsrowrow_sumsum) = S ((S (m)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_terminal. fs_u_dst_fubini_columnsrowsrowrow_sumsumpositive = fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_terminal * S ((S (m)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumpositive) + (dst_positive_sum_fubini_columnsrowsrowrow_sumsum))) /\ forall fs_i_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps = m) -> exists fs_a_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps fs_r_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps fs_s_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_columnsrowsrowrow_sumsum)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_fubini_columnsrowsrowrow_sumsum = fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_columnsrowsrowrow_sumsum) + (fs_a_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_fubini_columnsrowsrowrow_sumsumpositive = fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumpositive) + (fs_r_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_fubini_columnsrowsrowrow_sumsumpositive = fs_q_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumpositive) + (fs_s_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps = fs_r_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps + fs_a_dst_fubini_columnsrowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_columnsrowsrowrow_sumsumnegative fs_v_dst_fubini_columnsrowsrowrow_sumsumnegative. ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_start. fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_start. fs_u_dst_fubini_columnsrowsrowrow_sumsumnegative = fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_terminal. fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_fubini_columnsrowsrowrow_sumsum) = S ((S (m)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_terminal. fs_u_dst_fubini_columnsrowsrowrow_sumsumnegative = fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_terminal * S ((S (m)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumnegative) + (dst_negative_sum_fubini_columnsrowsrowrow_sumsum))) /\ forall fs_i_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps = m) -> exists fs_a_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps fs_r_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps fs_s_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_columnsrowsrowrow_sumsum)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_fubini_columnsrowsrowrow_sumsum = fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_columnsrowsrowrow_sumsum) + (fs_a_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_fubini_columnsrowsrowrow_sumsumnegative = fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumnegative) + (fs_r_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_fubini_columnsrowsrowrow_sumsumnegative = fs_q_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_columnsrowsrowrow_sumsumnegative) + (fs_s_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps = fs_r_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps + fs_a_dst_fubini_columnsrowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_columnsrowsrowrow_sumsumresult ge_balance_negative_fubini_columnsrowsrowrow_sumsumresult. (((((srt_value_fubini_columnsrows) = 2 * (ge_balance_positive_fubini_columnsrowsrowrow_sumsumresult) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_fubini_columnsrowsrowrow_sumsumresultdecode. (((srt_value_fubini_columnsrows) = 2 * ge_signed_half_fubini_columnsrowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_fubini_columnsrowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_fubini_columnsrowsrowrow_sumsumresult) = S ge_signed_half_fubini_columnsrowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_fubini_columnsrowsrowrow_sumsum) + ge_balance_negative_fubini_columnsrowsrowrow_sumsumresult = (dst_negative_sum_fubini_columnsrowsrowrow_sumsum) + ge_balance_positive_fubini_columnsrowsrowrow_sumsumresult)))))))))))))))))) /\ (exists dst_positive_code_fubini_columnstotal dst_positive_scale_fubini_columnstotal dst_negative_code_fubini_columnstotal dst_negative_scale_fubini_columnstotal dst_positive_sum_fubini_columnstotal dst_negative_sum_fubini_columnstotal. (((srt_rows_fubini_columns) = (((((dst_positive_code_fubini_columnstotal) + (dst_positive_scale_fubini_columnstotal)) * S ((dst_positive_code_fubini_columnstotal) + (dst_positive_scale_fubini_columnstotal)) + ((dst_positive_scale_fubini_columnstotal) + (dst_positive_scale_fubini_columnstotal))) + (((dst_negative_code_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)) * S ((dst_negative_code_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)) + ((dst_negative_scale_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)))) * S ((((dst_positive_code_fubini_columnstotal) + (dst_positive_scale_fubini_columnstotal)) * S ((dst_positive_code_fubini_columnstotal) + (dst_positive_scale_fubini_columnstotal)) + ((dst_positive_scale_fubini_columnstotal) + (dst_positive_scale_fubini_columnstotal))) + (((dst_negative_code_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)) * S ((dst_negative_code_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)) + ((dst_negative_scale_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)))) + ((((dst_negative_code_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)) * S ((dst_negative_code_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)) + ((dst_negative_scale_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal))) + (((dst_negative_code_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)) * S ((dst_negative_code_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)) + ((dst_negative_scale_fubini_columnstotal) + (dst_negative_scale_fubini_columnstotal)))))) /\ (((exists fs_u_dst_fubini_columnstotalpositive fs_v_dst_fubini_columnstotalpositive. ((((exists fs_h_dst_fubini_columnstotalpositive_body_start. fs_h_dst_fubini_columnstotalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_columnstotalpositive)) /\ exists fs_q_dst_fubini_columnstotalpositive_body_start. fs_u_dst_fubini_columnstotalpositive = fs_q_dst_fubini_columnstotalpositive_body_start * S ((S (0)) * fs_v_dst_fubini_columnstotalpositive) + (0))) /\ ((((exists fs_h_dst_fubini_columnstotalpositive_body_terminal. fs_h_dst_fubini_columnstotalpositive_body_terminal + S (dst_positive_sum_fubini_columnstotal) = S ((S (n)) * fs_v_dst_fubini_columnstotalpositive)) /\ exists fs_q_dst_fubini_columnstotalpositive_body_terminal. fs_u_dst_fubini_columnstotalpositive = fs_q_dst_fubini_columnstotalpositive_body_terminal * S ((S (n)) * fs_v_dst_fubini_columnstotalpositive) + (dst_positive_sum_fubini_columnstotal))) /\ forall fs_i_dst_fubini_columnstotalpositive_body_steps. (exists fs_lt_dst_fubini_columnstotalpositive_body_steps_bound. fs_lt_dst_fubini_columnstotalpositive_body_steps_bound + S fs_i_dst_fubini_columnstotalpositive_body_steps = n) -> exists fs_a_dst_fubini_columnstotalpositive_body_steps fs_r_dst_fubini_columnstotalpositive_body_steps fs_s_dst_fubini_columnstotalpositive_body_steps. ((((exists fs_h_dst_fubini_columnstotalpositive_body_steps_summand. fs_h_dst_fubini_columnstotalpositive_body_steps_summand + S (fs_a_dst_fubini_columnstotalpositive_body_steps) = S ((S (fs_i_dst_fubini_columnstotalpositive_body_steps)) * dst_positive_scale_fubini_columnstotal)) /\ exists fs_q_dst_fubini_columnstotalpositive_body_steps_summand. dst_positive_code_fubini_columnstotal = fs_q_dst_fubini_columnstotalpositive_body_steps_summand * S ((S (fs_i_dst_fubini_columnstotalpositive_body_steps)) * dst_positive_scale_fubini_columnstotal) + (fs_a_dst_fubini_columnstotalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_columnstotalpositive_body_steps_partial. fs_h_dst_fubini_columnstotalpositive_body_steps_partial + S (fs_r_dst_fubini_columnstotalpositive_body_steps) = S ((S (fs_i_dst_fubini_columnstotalpositive_body_steps)) * fs_v_dst_fubini_columnstotalpositive)) /\ exists fs_q_dst_fubini_columnstotalpositive_body_steps_partial. fs_u_dst_fubini_columnstotalpositive = fs_q_dst_fubini_columnstotalpositive_body_steps_partial * S ((S (fs_i_dst_fubini_columnstotalpositive_body_steps)) * fs_v_dst_fubini_columnstotalpositive) + (fs_r_dst_fubini_columnstotalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_columnstotalpositive_body_steps_successor. fs_h_dst_fubini_columnstotalpositive_body_steps_successor + S (fs_s_dst_fubini_columnstotalpositive_body_steps) = S ((S (S fs_i_dst_fubini_columnstotalpositive_body_steps)) * fs_v_dst_fubini_columnstotalpositive)) /\ exists fs_q_dst_fubini_columnstotalpositive_body_steps_successor. fs_u_dst_fubini_columnstotalpositive = fs_q_dst_fubini_columnstotalpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_columnstotalpositive_body_steps)) * fs_v_dst_fubini_columnstotalpositive) + (fs_s_dst_fubini_columnstotalpositive_body_steps))) /\ fs_s_dst_fubini_columnstotalpositive_body_steps = fs_r_dst_fubini_columnstotalpositive_body_steps + fs_a_dst_fubini_columnstotalpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_columnstotalnegative fs_v_dst_fubini_columnstotalnegative. ((((exists fs_h_dst_fubini_columnstotalnegative_body_start. fs_h_dst_fubini_columnstotalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_columnstotalnegative)) /\ exists fs_q_dst_fubini_columnstotalnegative_body_start. fs_u_dst_fubini_columnstotalnegative = fs_q_dst_fubini_columnstotalnegative_body_start * S ((S (0)) * fs_v_dst_fubini_columnstotalnegative) + (0))) /\ ((((exists fs_h_dst_fubini_columnstotalnegative_body_terminal. fs_h_dst_fubini_columnstotalnegative_body_terminal + S (dst_negative_sum_fubini_columnstotal) = S ((S (n)) * fs_v_dst_fubini_columnstotalnegative)) /\ exists fs_q_dst_fubini_columnstotalnegative_body_terminal. fs_u_dst_fubini_columnstotalnegative = fs_q_dst_fubini_columnstotalnegative_body_terminal * S ((S (n)) * fs_v_dst_fubini_columnstotalnegative) + (dst_negative_sum_fubini_columnstotal))) /\ forall fs_i_dst_fubini_columnstotalnegative_body_steps. (exists fs_lt_dst_fubini_columnstotalnegative_body_steps_bound. fs_lt_dst_fubini_columnstotalnegative_body_steps_bound + S fs_i_dst_fubini_columnstotalnegative_body_steps = n) -> exists fs_a_dst_fubini_columnstotalnegative_body_steps fs_r_dst_fubini_columnstotalnegative_body_steps fs_s_dst_fubini_columnstotalnegative_body_steps. ((((exists fs_h_dst_fubini_columnstotalnegative_body_steps_summand. fs_h_dst_fubini_columnstotalnegative_body_steps_summand + S (fs_a_dst_fubini_columnstotalnegative_body_steps) = S ((S (fs_i_dst_fubini_columnstotalnegative_body_steps)) * dst_negative_scale_fubini_columnstotal)) /\ exists fs_q_dst_fubini_columnstotalnegative_body_steps_summand. dst_negative_code_fubini_columnstotal = fs_q_dst_fubini_columnstotalnegative_body_steps_summand * S ((S (fs_i_dst_fubini_columnstotalnegative_body_steps)) * dst_negative_scale_fubini_columnstotal) + (fs_a_dst_fubini_columnstotalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_columnstotalnegative_body_steps_partial. fs_h_dst_fubini_columnstotalnegative_body_steps_partial + S (fs_r_dst_fubini_columnstotalnegative_body_steps) = S ((S (fs_i_dst_fubini_columnstotalnegative_body_steps)) * fs_v_dst_fubini_columnstotalnegative)) /\ exists fs_q_dst_fubini_columnstotalnegative_body_steps_partial. fs_u_dst_fubini_columnstotalnegative = fs_q_dst_fubini_columnstotalnegative_body_steps_partial * S ((S (fs_i_dst_fubini_columnstotalnegative_body_steps)) * fs_v_dst_fubini_columnstotalnegative) + (fs_r_dst_fubini_columnstotalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_columnstotalnegative_body_steps_successor. fs_h_dst_fubini_columnstotalnegative_body_steps_successor + S (fs_s_dst_fubini_columnstotalnegative_body_steps) = S ((S (S fs_i_dst_fubini_columnstotalnegative_body_steps)) * fs_v_dst_fubini_columnstotalnegative)) /\ exists fs_q_dst_fubini_columnstotalnegative_body_steps_successor. fs_u_dst_fubini_columnstotalnegative = fs_q_dst_fubini_columnstotalnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_columnstotalnegative_body_steps)) * fs_v_dst_fubini_columnstotalnegative) + (fs_s_dst_fubini_columnstotalnegative_body_steps))) /\ fs_s_dst_fubini_columnstotalnegative_body_steps = fs_r_dst_fubini_columnstotalnegative_body_steps + fs_a_dst_fubini_columnstotalnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_columnstotalresult ge_balance_negative_fubini_columnstotalresult. (((((b) = 2 * (ge_balance_positive_fubini_columnstotalresult) /\ (ge_balance_negative_fubini_columnstotalresult) = 0) \/ exists ge_signed_half_fubini_columnstotalresultdecode. (((b) = 2 * ge_signed_half_fubini_columnstotalresultdecode + 1 /\ (ge_balance_positive_fubini_columnstotalresult) = 0) /\ (ge_balance_negative_fubini_columnstotalresult) = S ge_signed_half_fubini_columnstotalresultdecode))) /\ ((dst_positive_sum_fubini_columnstotal) + ge_balance_negative_fubini_columnstotalresult = (dst_negative_sum_fubini_columnstotal) + ge_balance_positive_fubini_columnstotalresult))))))))))) -> a=b