Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Every slice, row table, column table and signed sum is an actual beta-coded witness. Entries are F((o+s*i)+t*j), for i<m and j<n. Zero dimensions and zero strides are allowed; separately certified endpoints are unused. Table uniqueness concerns values, not codes. No infinite-sum assertion is made.
Exact theorem in conservative defined notation
∀ m. ∀ F. ∀ o. ∀ s. ∀ t. ∀ n. ∀ a. ∀ b. SignedRectangularSum(F,o,s,t,m,n,a) → SignedRectangularSum(F,o,t,s,n,m,b) → a = bEvery linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
signed_rectangular_sum_zero_outersigned_rectangular_sum_zero_innerdivisor_signed_sum_successor_decompose · checked external prerequisitesigned_rectangular_row_sums_existsarithmetic_signed_sum_exists · checked external prerequisitesigned_rectangular_row_sums_restrict_outersigned_rectangular_row_sums_lookuple_refl · checked external prerequisitesigned_rectangular_columns_successor_addsigned_prefix_sum_pointwise_add · checked external prerequisitesigned_add_functional · checked external prerequisite
Original expanded first-order 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=bComplete tactic proof in conservative notation
All 150 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
150 script commands · 33 reading checkpoints · 7 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (6)
01Induction on mL1–10
02Calculate and transport equalitiesL11–11
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L11
trans 0
03Use earlier factsL12–19
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L12
specialize signed_rectangular_sum_zero_outer (F) - L13
specialize signed_rectangular_sum_zero_outer (o) - L14
specialize signed_rectangular_sum_zero_outer (s) - L15
specialize signed_rectangular_sum_zero_outer (t) - L16
specialize signed_rectangular_sum_zero_outer (n) - L17
specialize signed_rectangular_sum_zero_outer (a) - L18
apply signed_rectangular_sum_zero_outer - L19
exact ha
04Calculate and transport equalitiesL20–20
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L20
symm
05Use earlier factsL21–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L21
specialize signed_rectangular_sum_zero_inner (F) - L22
specialize signed_rectangular_sum_zero_inner (o) - L23
specialize signed_rectangular_sum_zero_inner (t) - L24
specialize signed_rectangular_sum_zero_inner (s) - L25
specialize signed_rectangular_sum_zero_inner (n) - L26
specialize signed_rectangular_sum_zero_inner (b) - L27
apply signed_rectangular_sum_zero_inner - L28
exact hb
06Fix variables and assumptionsL29–37
07Separate the logical casesL38–41
08Establish hdL42–47
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed sum successor decompose.
- L42
have hd : ∃ u. ∃ v. SignedPrefixSum(x,m,u) ∧ (ArithAt(x,m,v) ∧ SignedAdd(u,v,a))Definitions: SignedPrefixSum(x,m,u)ArithAt(x,m,v)SignedAdd(u,v,a)Original native command in the exact edition - L43
specialize divisor_signed_sum_successor_decompose (x) - L44
specialize divisor_signed_sum_successor_decompose (m) - L45
specialize divisor_signed_sum_successor_decompose (a) - L46
apply divisor_signed_sum_successor_decompose - L47
exact ha_witness_right
09Separate the logical casesL48–51
10Establish hCL52–59
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed rectangular row sums exists.
- L52
have hC : ∃ C. ArithRowSums(F,C,o,t,s,n,m)Definitions: ArithRowSums(F,C,o,t,s,n,m)Original native command in the exact edition - L53
specialize signed_rectangular_row_sums_exists (n) - L54
specialize signed_rectangular_row_sums_exists (F) - L55
specialize signed_rectangular_row_sums_exists (o) - L56
specialize signed_rectangular_row_sums_exists (t) - L57
specialize signed_rectangular_row_sums_exists (s) - L58
specialize signed_rectangular_row_sums_exists (m) - L59
apply signed_rectangular_row_sums_exists
11Separate the logical casesL60–61
12Use earlier factsL62–62
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L62
exact ha_witness_left_left
13Separate the logical casesL63–63
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L63
cases hC
14Establish hsumCL64–68
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed sum exists.
- L64
have hsumC : ∃ z. SignedPrefixSum(x4,n,z)Definitions: SignedPrefixSum(x4,n,z)Original native command in the exact edition - L65
specialize arithmetic_signed_sum_exists (n) - L66
specialize arithmetic_signed_sum_exists (x4) - L67
specialize arithmetic_signed_sum_exists (n) - L68
apply arithmetic_signed_sum_exists
15Separate the logical casesL69–70
16Use earlier factsL71–71
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L71
exact hC_witness_right_left
17Separate the logical casesL72–72
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L72
cases hsumC
18Establish heqL73–81
19Construct an explicit witnessL82–82
Supply the displayed value, then prove that it has the required property.
- L82
exists x
20Separate the logical casesL83–83
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L83
split
21Use earlier factsL84–93
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L84
specialize signed_rectangular_row_sums_restrict_outer (F) - L85
specialize signed_rectangular_row_sums_restrict_outer (x) - L86
specialize signed_rectangular_row_sums_restrict_outer (o) - L87
specialize signed_rectangular_row_sums_restrict_outer (s) - L88
specialize signed_rectangular_row_sums_restrict_outer (t) - L89
specialize signed_rectangular_row_sums_restrict_outer (m) - L90
specialize signed_rectangular_row_sums_restrict_outer (n) - L91
apply signed_rectangular_row_sums_restrict_outer - L92
exact ha_witness_left - L93
exact hd_witness_witness_left
22Construct an explicit witnessL94–94
Supply the displayed value, then prove that it has the required property.
- L94
exists x4
23Separate the logical casesL95–95
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L95
split
24Use earlier factsL96–97
25Establish hlastL98–107
Establish this local claim before using it. It is not an additional assumption.
- L98
have hlast : SignedSliceSum(F,o + s · m,t,n,x3)Definitions: SignedSliceSum(F,o + s · m,t,n,x3)Original native command in the exact edition - L99
specialize signed_rectangular_row_sums_lookup (F) - L100
specialize signed_rectangular_row_sums_lookup (x) - L101
specialize signed_rectangular_row_sums_lookup (o) - L102
specialize signed_rectangular_row_sums_lookup (s) - L103
specialize signed_rectangular_row_sums_lookup (t) - L104
specialize signed_rectangular_row_sums_lookup (S m) - L105
specialize signed_rectangular_row_sums_lookup (n) - L106
specialize signed_rectangular_row_sums_lookup (m) - L107
specialize signed_rectangular_row_sums_lookup (x3)
26Use earlier factsL108–112
27Separate the logical casesL113–114
28Establish hpointL115–124
Establish this local claim before using it. It is not an additional assumption.
- L115
have hpoint : ArithAdd(x4,x6,x1,n)Definitions: ArithAdd(x4,x6,x1,n)Original native command in the exact edition - L116
specialize signed_rectangular_columns_successor_add (F) - L117
specialize signed_rectangular_columns_successor_add (x4) - L118
specialize signed_rectangular_columns_successor_add (x6) - L119
specialize signed_rectangular_columns_successor_add (x1) - L120
specialize signed_rectangular_columns_successor_add (o) - L121
specialize signed_rectangular_columns_successor_add (s) - L122
specialize signed_rectangular_columns_successor_add (t) - L123
specialize signed_rectangular_columns_successor_add (m) - L124
specialize signed_rectangular_columns_successor_add (n)
29Use earlier factsL125–128
30Establish haddL129–138
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed prefix sum pointwise add.
- L129
have hadd : SignedAdd(x5,x3,b)Definitions: SignedAdd(x5,x3,b)Original native command in the exact edition - L130
specialize signed_prefix_sum_pointwise_add (n) - L131
specialize signed_prefix_sum_pointwise_add (x4) - L132
specialize signed_prefix_sum_pointwise_add (x6) - L133
specialize signed_prefix_sum_pointwise_add (x1) - L134
specialize signed_prefix_sum_pointwise_add (x5) - L135
specialize signed_prefix_sum_pointwise_add (x3) - L136
specialize signed_prefix_sum_pointwise_add (b) - L137
apply signed_prefix_sum_pointwise_add - L138
exact hpoint
31Use earlier factsL139–141
32Calculate and transport equalitiesL142–143
33Use earlier factsL144–150
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 150 lines
- 0001
induction m - 0002
intro F - 0003
intro o - 0004
intro s - 0005
intro t - 0006
intro n - 0007
intro a - 0008
intro b - 0009
intro ha - 0010
intro hb - 0011
trans 0 - 0012
specialize signed_rectangular_sum_zero_outer (F) - 0013
specialize signed_rectangular_sum_zero_outer (o) - 0014
specialize signed_rectangular_sum_zero_outer (s) - 0015
specialize signed_rectangular_sum_zero_outer (t) - 0016
specialize signed_rectangular_sum_zero_outer (n) - 0017
specialize signed_rectangular_sum_zero_outer (a) - 0018
apply signed_rectangular_sum_zero_outer - 0019
exact ha - 0020
symm - 0021
specialize signed_rectangular_sum_zero_inner (F) - 0022
specialize signed_rectangular_sum_zero_inner (o) - 0023
specialize signed_rectangular_sum_zero_inner (t) - 0024
specialize signed_rectangular_sum_zero_inner (s) - 0025
specialize signed_rectangular_sum_zero_inner (n) - 0026
specialize signed_rectangular_sum_zero_inner (b) - 0027
apply signed_rectangular_sum_zero_inner - 0028
exact hb - 0029
intro F - 0030
intro o - 0031
intro s - 0032
intro t - 0033
intro n - 0034
intro a - 0035
intro b - 0036
intro ha - 0037
intro hb - 0038
cases ha - 0039
cases ha_witness - 0040
cases hb - 0041
cases hb_witness - 0042
have hd : ∃ u. ∃ v. SignedPrefixSum(x,m,u) ∧ (ArithAt(x,m,v) ∧ SignedAdd(u,v,a)) - 0043
specialize divisor_signed_sum_successor_decompose (x) - 0044
specialize divisor_signed_sum_successor_decompose (m) - 0045
specialize divisor_signed_sum_successor_decompose (a) - 0046
apply divisor_signed_sum_successor_decompose - 0047
exact ha_witness_right - 0048
cases hd - 0049
cases hd_witness - 0050
cases hd_witness_witness - 0051
cases hd_witness_witness_right - 0052
have hC : ∃ C. ArithRowSums(F,C,o,t,s,n,m) - 0053
specialize signed_rectangular_row_sums_exists (n) - 0054
specialize signed_rectangular_row_sums_exists (F) - 0055
specialize signed_rectangular_row_sums_exists (o) - 0056
specialize signed_rectangular_row_sums_exists (t) - 0057
specialize signed_rectangular_row_sums_exists (s) - 0058
specialize signed_rectangular_row_sums_exists (m) - 0059
apply signed_rectangular_row_sums_exists - 0060
cases ha_witness_left - 0061
cases ha_witness_left_right - 0062
exact ha_witness_left_left - 0063
cases hC - 0064
have hsumC : ∃ z. SignedPrefixSum(x4,n,z) - 0065
specialize arithmetic_signed_sum_exists (n) - 0066
specialize arithmetic_signed_sum_exists (x4) - 0067
specialize arithmetic_signed_sum_exists (n) - 0068
apply arithmetic_signed_sum_exists - 0069
cases hC_witness - 0070
cases hC_witness_right - 0071
exact hC_witness_right_left - 0072
cases hsumC - 0073
have heq : x2 = x5 - 0074
specialize IH (F) - 0075
specialize IH (o) - 0076
specialize IH (s) - 0077
specialize IH (t) - 0078
specialize IH (n) - 0079
specialize IH (x2) - 0080
specialize IH (x5) - 0081
apply IH - 0082
exists x - 0083
split - 0084
specialize signed_rectangular_row_sums_restrict_outer (F) - 0085
specialize signed_rectangular_row_sums_restrict_outer (x) - 0086
specialize signed_rectangular_row_sums_restrict_outer (o) - 0087
specialize signed_rectangular_row_sums_restrict_outer (s) - 0088
specialize signed_rectangular_row_sums_restrict_outer (t) - 0089
specialize signed_rectangular_row_sums_restrict_outer (m) - 0090
specialize signed_rectangular_row_sums_restrict_outer (n) - 0091
apply signed_rectangular_row_sums_restrict_outer - 0092
exact ha_witness_left - 0093
exact hd_witness_witness_left - 0094
exists x4 - 0095
split - 0096
exact hC_witness - 0097
exact hsumC_witness - 0098
have hlast : SignedSliceSum(F,o + s · m,t,n,x3) - 0099
specialize signed_rectangular_row_sums_lookup (F) - 0100
specialize signed_rectangular_row_sums_lookup (x) - 0101
specialize signed_rectangular_row_sums_lookup (o) - 0102
specialize signed_rectangular_row_sums_lookup (s) - 0103
specialize signed_rectangular_row_sums_lookup (t) - 0104
specialize signed_rectangular_row_sums_lookup (S m) - 0105
specialize signed_rectangular_row_sums_lookup (n) - 0106
specialize signed_rectangular_row_sums_lookup (m) - 0107
specialize signed_rectangular_row_sums_lookup (x3) - 0108
apply signed_rectangular_row_sums_lookup - 0109
exact ha_witness_left - 0110
specialize le_refl (S m) - 0111
apply le_refl - 0112
exact hd_witness_witness_right_left - 0113
cases hlast - 0114
cases hlast_witness - 0115
have hpoint : ArithAdd(x4,x6,x1,n) - 0116
specialize signed_rectangular_columns_successor_add (F) - 0117
specialize signed_rectangular_columns_successor_add (x4) - 0118
specialize signed_rectangular_columns_successor_add (x6) - 0119
specialize signed_rectangular_columns_successor_add (x1) - 0120
specialize signed_rectangular_columns_successor_add (o) - 0121
specialize signed_rectangular_columns_successor_add (s) - 0122
specialize signed_rectangular_columns_successor_add (t) - 0123
specialize signed_rectangular_columns_successor_add (m) - 0124
specialize signed_rectangular_columns_successor_add (n) - 0125
apply signed_rectangular_columns_successor_add - 0126
exact hC_witness - 0127
exact hlast_witness_left - 0128
exact hb_witness_left - 0129
have hadd : SignedAdd(x5,x3,b) - 0130
specialize signed_prefix_sum_pointwise_add (n) - 0131
specialize signed_prefix_sum_pointwise_add (x4) - 0132
specialize signed_prefix_sum_pointwise_add (x6) - 0133
specialize signed_prefix_sum_pointwise_add (x1) - 0134
specialize signed_prefix_sum_pointwise_add (x5) - 0135
specialize signed_prefix_sum_pointwise_add (x3) - 0136
specialize signed_prefix_sum_pointwise_add (b) - 0137
apply signed_prefix_sum_pointwise_add - 0138
exact hpoint - 0139
exact hsumC_witness - 0140
exact hlast_witness_right - 0141
exact hb_witness_right - 0142
rewrite heq at hd_witness_witness_right_right - 0143
rewrite heq at hd_witness_witness_right_right - 0144
specialize signed_add_functional (x5) - 0145
specialize signed_add_functional (x3) - 0146
specialize signed_add_functional (a) - 0147
specialize signed_add_functional (b) - 0148
apply signed_add_functional - 0149
exact hd_witness_witness_right_right - 0150
exact hadd